let G1 be _finite _Graph; :: thesis: for G2 being spanning Subgraph of G1 st G1 .size() = G2 .size() holds
G1 == G2
let G2 be spanning Subgraph of G1; :: thesis: ( G1 .size() = G2 .size() implies G1 == G2 )
assume A1: G1 .size() = G2 .size() ; :: thesis: G1 == G2
card (the_Edges_of G1) = card (the_Edges_of G2) by A1;
then the_Edges_of G1 = the_Edges_of G2 by CARD_2:102;
hence G1 == G2 by Th118; :: thesis: verum