let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
e DJoins v1,v2,G1
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
e DJoins v1,v2,G1
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
e DJoins v1,v2,G1
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 implies e DJoins v1,v2,G1 )
assume A1: not e in the_Edges_of G2 ; :: thesis: e DJoins v1,v2,G1
e in {e} by TARSKI:def 1;
then e in (the_Edges_of G2) \/ {e} by XBOOLE_0:def 3;
then A2: e in the_Edges_of G1 by A1, Def11;
A3: e in dom (e .--> v1) by FUNCOP_1:74;
A4: (the_Source_of G1) . e = ((the_Source_of G2) +* (e .--> v1)) . e by A1, Def11
.= (e .--> v1) . e by A3, FUNCT_4:13
.= v1 by FUNCOP_1:72 ;
A5: e in dom (e .--> v2) by FUNCOP_1:74;
(the_Target_of G1) . e = ((the_Target_of G2) +* (e .--> v2)) . e by A1, Def11
.= (e .--> v2) . e by A5, FUNCT_4:13
.= v2 by FUNCOP_1:72 ;
hence e DJoins v1,v2,G1 by A2, A4, GLIB_000:def 14; :: thesis: verum