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

Conclusion

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

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

Tactic
 EXPAND "subgraph?"
Premise 1.   (has proof of 1 step)

-1. subset?(vert(SS!1), vert(G!1)) AND subset?(edges(SS!1), edges(G!1))

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