theorem :: GLIB_000:117

for G1 being _finite _Graph
for G2 being Subgraph of G1 holds
( G2 is spanning iff G1 .order() = G2 .order() ) by CARD_2:102;