let G1 be _finite connected _Graph; :: thesis: for G2 being Subgraph of G1 st G1 .size() = G2 .size() holds
G1 == G2
let G2 be Subgraph of G1; :: thesis: ( G1 .size() = G2 .size() implies G1 == G2 )
assume A1: G1 .size() = G2 .size() ; :: thesis: G1 == G2
card (the_Edges_of G2) = G2 .size() by GLIB_000:def 25
.= card (the_Edges_of G1) by A1, GLIB_000:def 25 ;
then the_Edges_of G1 = the_Edges_of G2 by CARD_2:102;
hence G1 == G2 by Th19; :: thesis: verum