let G2 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2
let v1, e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2

per cases ( ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( ( not v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) & ( v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ) ) ;

suppose A1: ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2

then ( the_Vertices_of G1 = (the_Vertices_of G2) \/ {v2} & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by Def12;
then A2: the_Edges_of G2 = (the_Edges_of G1) \ {e} by A1, ZFMISC_1:117;
for e1 being object holds
( e1 in G1 .edgesBetween (the_Vertices_of G2) iff e1 in (the_Edges_of G1) \ {e} )

proof

let e1 be object ; :: thesis: ( e1 in G1 .edgesBetween (the_Vertices_of G2) iff e1 in (the_Edges_of G1) \ {e} )

hereby :: thesis: ( e1 in (the_Edges_of G1) \ {e} implies e1 in G1 .edgesBetween (the_Vertices_of G2) )

assume e1 in G1 .edgesBetween (the_Vertices_of G2) ; :: thesis: e1 in (the_Edges_of G1) \ {e}
then A3: ( e1 in the_Edges_of G1 & (the_Source_of G1) . e1 in the_Vertices_of G2 & (the_Target_of G1) . e1 in the_Vertices_of G2 ) by GLIB_000:31;
e DJoins v1,v2,G1 by A1, Th135;
then e1 <> e by A1, A3, GLIB_000:def 14;
then not e1 in {e} by TARSKI:def 1;
hence e1 in (the_Edges_of G1) \ {e} by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume A4: e1 in (the_Edges_of G1) \ {e} ; :: thesis: e1 in G1 .edgesBetween (the_Vertices_of G2)
reconsider e2 = e1 as set by TARSKI:1;
A6: e2 in the_Edges_of G2 by A2, A4;
A7: ( (the_Source_of G2) . e2 in the_Vertices_of G2 & (the_Target_of G2) . e2 in the_Vertices_of G2 ) by A6, FUNCT_2:5;
e2 Joins (the_Source_of G2) . e2,(the_Target_of G2) . e2,G2 by A6, GLIB_000:def 13;
hence e1 in G1 .edgesBetween (the_Vertices_of G2) by A7, Th74, GLIB_000:32; :: thesis: verum

end;

hence G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2 by A2, TARSKI:2; :: thesis: verum

end;

suppose A8: ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2

then ( the_Vertices_of G1 = (the_Vertices_of G2) \/ {v1} & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by Def12;
then A9: the_Edges_of G2 = (the_Edges_of G1) \ {e} by A8, ZFMISC_1:117;
for e1 being object holds
( e1 in G1 .edgesBetween (the_Vertices_of G2) iff e1 in (the_Edges_of G1) \ {e} )

proof

let e1 be object ; :: thesis: ( e1 in G1 .edgesBetween (the_Vertices_of G2) iff e1 in (the_Edges_of G1) \ {e} )

hereby :: thesis: ( e1 in (the_Edges_of G1) \ {e} implies e1 in G1 .edgesBetween (the_Vertices_of G2) )

assume e1 in G1 .edgesBetween (the_Vertices_of G2) ; :: thesis: e1 in (the_Edges_of G1) \ {e}
then A10: ( e1 in the_Edges_of G1 & (the_Source_of G1) . e1 in the_Vertices_of G2 & (the_Target_of G1) . e1 in the_Vertices_of G2 ) by GLIB_000:31;
e DJoins v1,v2,G1 by A8, Th136;
then e1 <> e by A8, A10, GLIB_000:def 14;
then not e1 in {e} by TARSKI:def 1;
hence e1 in (the_Edges_of G1) \ {e} by A10, XBOOLE_0:def 5; :: thesis: verum

end;

assume A11: e1 in (the_Edges_of G1) \ {e} ; :: thesis: e1 in G1 .edgesBetween (the_Vertices_of G2)
reconsider e2 = e1 as set by TARSKI:1;
A13: e2 in the_Edges_of G2 by A9, A11;
A14: ( (the_Source_of G2) . e2 in the_Vertices_of G2 & (the_Target_of G2) . e2 in the_Vertices_of G2 ) by A13, FUNCT_2:5;
e2 Joins (the_Source_of G2) . e2,(the_Target_of G2) . e2,G2 by A13, GLIB_000:def 13;
hence e1 in G1 .edgesBetween (the_Vertices_of G2) by A14, Th74, GLIB_000:32; :: thesis: verum

end;

hence G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2 by A9, TARSKI:2; :: thesis: verum

end;

suppose ( ( not v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) & ( v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ) ; :: thesis: G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2

then G1 == G2 by Def12;
hence G1 .edgesBetween (the_Vertices_of G2) = G2 .edgesBetween (the_Vertices_of G2) by GLIB_000:90
.= the_Edges_of G2 by GLIB_000:34 ;
:: thesis: verum

end;

end;