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

Conclusion

1. FORALL g:graph[T], p:nat, V:set[T] : contains indep(subgraph(g, V), p) IMPLIES contains indep(g, p)

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

-1. contains indep(subgraph(g!1, V!1), p!1)

1. contains indep(g!1, p!1)