let X be set ; :: thesis: for G being Graph
for v2, v1 being Vertex of G
for v9 being Vertex of (AddNewEdge v1,v2) st v9 = v2 & v1 <> v2 holds
Edges_Out v9,X = Edges_Out v2,X
let G be Graph; :: thesis: for v2, v1 being Vertex of G
for v9 being Vertex of (AddNewEdge v1,v2) st v9 = v2 & v1 <> v2 holds
Edges_Out v9,X = Edges_Out v2,X
let v2, v1 be Vertex of G; :: thesis: for v9 being Vertex of (AddNewEdge v1,v2) st v9 = v2 & v1 <> v2 holds
Edges_Out v9,X = Edges_Out v2,X
let v9 be Vertex of (AddNewEdge v1,v2); :: thesis: ( v9 = v2 & v1 <> v2 implies Edges_Out v9,X = Edges_Out v2,X )
assume that
A1: v9 = v2 and
A2: v1 <> v2 ; :: thesis: Edges_Out v9,X = Edges_Out v2,X
set G9 = AddNewEdge v1,v2;
set E = the carrier' of G;
set S = the Source of G;
set E9 = the carrier' of (AddNewEdge v1,v2);
set S9 = the Source of (AddNewEdge v1,v2);
A3: the carrier' of (AddNewEdge v1,v2) = the carrier' of G \/ {the carrier' of G} by Def7;

now

let x be set ; :: thesis: ( ( x in Edges_Out v9,X implies x in Edges_Out v2,X ) & ( x in Edges_Out v2,X implies x in Edges_Out v9,X ) )

hereby :: thesis: ( x in Edges_Out v2,X implies x in Edges_Out v9,X )

assume A4: x in Edges_Out v9,X ; :: thesis: x in Edges_Out v2,X
then A5: x in X by Def2;
A6: the Source of (AddNewEdge v1,v2) . x = v9 by A4, Def2;
the Source of (AddNewEdge v1,v2) . the carrier' of G = v1 by Th39;
then not x in {the carrier' of G} by A1, A2, A6, TARSKI:def 1;
then A7: x in the carrier' of G by A3, A4, XBOOLE_0:def 3;
then the Source of G . x = v2 by A1, A6, Th40;
hence x in Edges_Out v2,X by A5, A7, Def2; :: thesis: verum

end;

assume A8: x in Edges_Out v2,X ; :: thesis: x in Edges_Out v9,X
then the Source of G . x = v2 by Def2;
then A9: the Source of (AddNewEdge v1,v2) . x = v9 by A1, A8, Th40;
( x in X & x in the carrier' of (AddNewEdge v1,v2) ) by A3, A8, Def2, XBOOLE_0:def 3;
hence x in Edges_Out v9,X by A9, Def2; :: thesis: verum

end;

hence Edges_Out v9,X = Edges_Out v2,X by TARSKI:2; :: thesis: verum