let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
let V be set ; :: thesis: for G1 being addVertices of G2,V holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
let G1 be addVertices of G2,V; :: thesis: G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
set E1 = the_Edges_of G1;
set V2 = the_Vertices_of G2;
for e being object holds
( e in the_Edges_of G1 iff e in (G1 .edgesInto (the_Vertices_of G2)) /\ (G1 .edgesOutOf (the_Vertices_of G2)) )
proof
let e be object ; :: thesis: ( e in the_Edges_of G1 iff e in (G1 .edgesInto (the_Vertices_of G2)) /\ (G1 .edgesOutOf (the_Vertices_of G2)) )
hereby :: thesis: ( e in (G1 .edgesInto (the_Vertices_of G2)) /\ (G1 .edgesOutOf (the_Vertices_of G2)) implies e in the_Edges_of G1 )
assume A1: e in the_Edges_of G1 ; :: thesis: e in (G1 .edgesInto (the_Vertices_of G2)) /\ (G1 .edgesOutOf (the_Vertices_of G2))
then A2: e in the_Edges_of G2 by Def10;
then A3: ( (the_Source_of G2) . e in the_Vertices_of G2 & (the_Target_of G2) . e in the_Vertices_of G2 ) by FUNCT_2:5;
reconsider e1 = e as set by TARSKI:1;
( (the_Source_of G1) . e1 in the_Vertices_of G2 & (the_Target_of G1) . e1 in the_Vertices_of G2 ) by A2, A3, Def9;
then ( e1 in G1 .edgesInto (the_Vertices_of G2) & e1 in G1 .edgesOutOf (the_Vertices_of G2) ) by A1, GLIB_000:def 26, GLIB_000:def 27;
hence e in (G1 .edgesInto (the_Vertices_of G2)) /\ (G1 .edgesOutOf (the_Vertices_of G2)) by XBOOLE_0:def 4; :: thesis: verum
end;
thus ( e in (G1 .edgesInto (the_Vertices_of G2)) /\ (G1 .edgesOutOf (the_Vertices_of G2)) implies e in the_Edges_of G1 ) ; :: thesis: verum
end;
then the_Edges_of G1 = (G1 .edgesInto (the_Vertices_of G2)) /\ (G1 .edgesOutOf (the_Vertices_of G2)) by TARSKI:2;
hence G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1 by GLIB_000:def 29; :: thesis: verum