FDL > PVS > Graphs > ramsey new > subgraph clique > pf:subgraph clique > 1 > 1 > 1 > 1 > 2 > 1 > 1 > 1 > 1

Conclusion

-1. C!1(i!1)
-2. C!1(j!1)
-3. vert(g!1)(i!1) AND V!1(i!1)
-4. card(C!1) > = p!1
-5. ((NOT (i!1 = j!1)) AND C!1(i!1) AND C!1(j!1)) IMPLIES ((NOT (i!1 = j!1)) AND edges(g!1)(dbl[T](i!1, j!1)) AND (FORALL x:T : ((x = i!1) OR (x = j!1)) IMPLIES V!1(x)))

1. i!1 = j!1
2. edges(g!1)(dbl[T](i!1, j!1))