let G1 be _finite edgeless _Graph; :: thesis: for G2 being Subgraph of G1 st G1 .order() = G2 .order() holds
G1 == G2
let G2 be Subgraph of G1; :: thesis: ( G1 .order() = G2 .order() implies G1 == G2 )
assume A1: G1 .order() = G2 .order() ; :: thesis: G1 == G2
A2: card (the_Vertices_of G1) = G1 .order() by GLIB_000:def 24
.= card (the_Vertices_of G2) by A1, GLIB_000:def 24 ;
A3: the_Vertices_of G2 = the_Vertices_of G1 by A2, CARD_2:102;
A4: the_Edges_of G1 = the_Edges_of G2 ;
G1 is Subgraph of G1 by GLIB_000:40;
hence G1 == G2 by A3, A4, GLIB_000:86; :: thesis: verum