let G1 be _finite _Graph; :: thesis: for G2 being Subgraph of G1 st G1 .size() = G2 .size() holds
G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
let G2 be Subgraph of G1; :: thesis: ( G1 .size() = G2 .size() implies G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2) )
assume A1: G1 .size() = G2 .size() ; :: thesis: G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of 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 A2: the_Edges_of G1 = the_Edges_of G2 by CARD_2:102;
G1 is Supergraph of G2 by GLIB_006:57;
hence G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2) by A2, Th33; :: thesis: verum