let G2 be _Graph; :: thesis: for G1 being Supergraph of G2
for e, v1, v2 being object holds
( not e Joins v1,v2,G1 or e Joins v1,v2,G2 or not e in the_Edges_of G2 )
let G1 be Supergraph of G2; :: thesis: for e, v1, v2 being object holds
( not e Joins v1,v2,G1 or e Joins v1,v2,G2 or not e in the_Edges_of G2 )
let e, v1, v2 be object ; :: thesis: ( not e Joins v1,v2,G1 or e Joins v1,v2,G2 or not e in the_Edges_of G2 )
assume e Joins v1,v2,G1 ; :: thesis: ( e Joins v1,v2,G2 or not e in the_Edges_of G2 )

per cases then ( e DJoins v1,v2,G1 or e DJoins v2,v1,G1 ) by GLIB_000:16;

suppose e DJoins v1,v2,G1 ; :: thesis: ( e Joins v1,v2,G2 or not e in the_Edges_of G2 )

per cases then ( e DJoins v1,v2,G2 or not e in the_Edges_of G2 ) by Th75;

suppose e DJoins v1,v2,G2 ; :: thesis: ( e Joins v1,v2,G2 or not e in the_Edges_of G2 )

hence ( e Joins v1,v2,G2 or not e in the_Edges_of G2 ) by GLIB_000:16; :: thesis: verum

end;

suppose not e in the_Edges_of G2 ; :: thesis: ( e Joins v1,v2,G2 or not e in the_Edges_of G2 )

hence ( e Joins v1,v2,G2 or not e in the_Edges_of G2 ) ; :: thesis: verum

end;

end;

end;

suppose e DJoins v2,v1,G1 ; :: thesis: ( e Joins v1,v2,G2 or not e in the_Edges_of G2 )

per cases then ( e DJoins v2,v1,G2 or not e in the_Edges_of G2 ) by Th75;

suppose e DJoins v2,v1,G2 ; :: thesis: ( e Joins v1,v2,G2 or not e in the_Edges_of G2 )

hence ( e Joins v1,v2,G2 or not e in the_Edges_of G2 ) by GLIB_000:16; :: thesis: verum

end;

suppose not e in the_Edges_of G2 ; :: thesis: ( e Joins v1,v2,G2 or not e in the_Edges_of G2 )

hence ( e Joins v1,v2,G2 or not e in the_Edges_of G2 ) ; :: thesis: verum

end;

end;

end;

end;