FDL > PVS > Graphs > ramsey new > subgraph clique > pf:subgraph clique > 1 > 1 > 1 > 1 (9 nodes)

Conclusion

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

1. (FORALL x:T : C!1(x) = > vert(g!1)(x)) AND (card(C!1) > = p!1) AND (FORALL i, j : ((NOT (i = j)) AND C!1(i) AND C!1(j)) IMPLIES ((NOT (i = j)) AND edges(g!1)(dbl[T](i, j))))

Tactic
 PROP
Premise 1.   (has proof of 3 steps)

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

1. FORALL x:T : C!1(x) = > vert(g!1)(x)
Premise 2.   (has proof of 5 steps)

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

1. FORALL i, j : ((NOT (i = j)) AND C!1(i) AND C!1(j)) IMPLIES ((NOT (i = j)) AND edges(g!1)(dbl[T](i, j)))