FDL > PVS > Graphs > subgraphs > subgraph smaller > pf:subgraph_smaller : proof (4 nodes)

Conclusion

1. FORALL G:graph[T], SS:graph[T] : subgraph?(SS, G) IMPLIES (size(SS) < = size(G))

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

-1. subgraph?(SS!1, G!1)

1. size(SS!1) < = size(G!1)