let G2 be _Graph; :: thesis: for G1 being Supergraph of G2
for e, v1, v2 being object holds
( not e DJoins v1,v2,G1 or e DJoins 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 DJoins v1,v2,G1 or e DJoins v1,v2,G2 or not e in the_Edges_of G2 )
let e, v1, v2 be object ; :: thesis: ( not e DJoins v1,v2,G1 or e DJoins v1,v2,G2 or not e in the_Edges_of G2 )
assume A1: e DJoins v1,v2,G1 ; :: thesis: ( e DJoins v1,v2,G2 or not e in the_Edges_of G2 )
per cases ( not e in the_Edges_of G2 or e in the_Edges_of G2 ) ;
suppose not e in the_Edges_of G2 ; :: thesis: ( e DJoins v1,v2,G2 or not e in the_Edges_of G2 )
hence ( e DJoins v1,v2,G2 or not e in the_Edges_of G2 ) ; :: thesis: verum
end;
suppose A2: e in the_Edges_of G2 ; :: thesis: ( e DJoins v1,v2,G2 or not e in the_Edges_of G2 )
A3: ( e in the_Edges_of G1 & (the_Source_of G1) . e = v1 & (the_Target_of G1) . e = v2 ) by A1, GLIB_000:def 14;
reconsider e1 = e as set by TARSKI:1;
( (the_Source_of G2) . e = v1 & (the_Target_of G2) . e = v2 ) by A2, A3, Def9;
hence ( e DJoins v1,v2,G2 or not e in the_Edges_of G2 ) by GLIB_000:def 14; :: thesis: verum
end;
end;