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;