FDL > PVS > Graphs > subgraphs > subgraph smaller > pf:subgraph smaller > 1 (3 nodes)

Conclusion

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

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

Tactic
 EXPAND "size"
Premise 1.   (has proof of 2 steps)

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

1. card[T](vert(SS!1)) < = card[T](vert(G!1))