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

Conclusion

-1. D!1(i!1)
-2. D!1(j!1)
-3. edges(g!1)(dbl[T](i!1, j!1))
-4. vert(g!1)(i!1) AND V!1(i!1)
-5. card(D!1) > = p!1
-6. ((NOT (i!1 = j!1)) AND D!1(i!1) AND D!1(j!1)) IMPLIES (NOT ((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. i!1 = j!1

Tactic
 ASSERT
Premise 1.   (has proof of 8 steps)

-1. D!1(i!1)
-2. D!1(j!1)
-3. edges(g!1)(dbl[T](i!1, j!1))
-4. vert(g!1)(i!1) AND V!1(i!1)
-5. card(D!1) > = p!1

1. i!1 = j!1
2. i!1 = j!1
3. FORALL x:T : ((x = i!1) OR (x = j!1)) IMPLIES V!1(x)