let G1, G2 be _Graph; :: thesis: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 & the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 implies G1 == G2 )
assume that
A1: the_Vertices_of G2 = the_Vertices_of G1 and
A2: the_Edges_of G2 = the_Edges_of G1 and
A3: the_Source_of G2 c= the_Source_of G1 and
A4: the_Target_of G2 c= the_Target_of G1 ; :: thesis: G1 == G2
G1 is Supergraph of G2 by A1, A3, A4, Th67;
hence G1 == G2 by A1, A2, Th69; :: thesis: verum