let G1 be _finite _Graph; :: thesis: for G2 being Subgraph of G1 holds
( G2 is spanning iff G1 .order() = G2 .order() )
let G2 be Subgraph of G1; :: thesis: ( G2 is spanning iff G1 .order() = G2 .order() )
hereby :: thesis: ( G1 .order() = G2 .order() implies G2 is spanning )
assume A1: G2 is spanning ; :: thesis: G1 .order() = G2 .order()
thus G1 .order() = card (the_Vertices_of G1) by GLIB_000:def 24
.= card (the_Vertices_of G2) by A1, GLIB_000:def 33
.= G2 .order() by GLIB_000:def 24 ; :: thesis: verum
end;
assume A2: G1 .order() = G2 .order() ; :: thesis: G2 is spanning
card (the_Vertices_of G1) = G1 .order() by GLIB_000:def 24
.= card (the_Vertices_of G2) by A2, GLIB_000:def 24 ;
hence G2 is spanning by GLIB_000:def 33, CARD_2:102; :: thesis: verum