FDL > PVS > Graphs > ramsey new > r1 : const-decl


r1(G): finite set[T] = LET v0 = choose(vert(G)) IN {(n:T) | vert(G)(n) AND (n /= v0) AND edge?(G)(v0, n)};