theorem :: GLIB_002:23

for G1 being _Graph
for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected by Lm10;