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

Conclusion

-1. EXISTS D:finite set[T] : (FORALL x:T : D(x) = > (vert(g!1)(x) AND V!1(x))) AND (card(D) > = p!1) AND (FORALL i_2016:T, j : ((NOT (i_2016 = j)) AND D(i_2016) AND D(j)) IMPLIES (NOT ((NOT (i_2016 = j)) AND edges(g!1)(dbl[T](i_2016, j)) AND (FORALL x:T : ((x = i_2016) OR (x = j)) IMPLIES V!1(x)))))

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

Tactic
 SKOSIMP*
Premise 1.   (has proof of 18 steps)

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

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