let X be set ; :: thesis: for G being Graph
for v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v1 & the carrier' of G in X holds
( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} & Edges_Out (v1,X) misses { the carrier' of G} )
let G be Graph; :: thesis: for v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v1 & the carrier' of G in X holds
( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} & Edges_Out (v1,X) misses { the carrier' of G} )
let v1, v2 be Vertex of G; :: thesis: for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v1 & the carrier' of G in X holds
( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} & Edges_Out (v1,X) misses { the carrier' of G} )
let v9 be Vertex of (AddNewEdge (v1,v2)); :: thesis: ( v9 = v1 & the carrier' of G in X implies ( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} & Edges_Out (v1,X) misses { the carrier' of G} ) )
assume that
A1: v9 = v1 and
A2: the carrier' of G in X ; :: thesis: ( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} & Edges_Out (v1,X) misses { the carrier' of G} )
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 :: thesis: for x being object holds
( ( x in Edges_Out (v9,X) implies x in (Edges_Out (v1,X)) \/ { the carrier' of G} ) & ( x in (Edges_Out (v1,X)) \/ { the carrier' of G} implies x in Edges_Out (v9,X) ) )

let x be object ; :: thesis: ( ( x in Edges_Out (v9,X) implies x in (Edges_Out (v1,X)) \/ { the carrier' of G} ) & ( x in (Edges_Out (v1,X)) \/ { the carrier' of G} implies b₁ in Edges_Out (v9,X) ) )

hereby :: thesis: ( x in (Edges_Out (v1,X)) \/ { the carrier' of G} implies b₁ in Edges_Out (v9,X) )

assume A4: x in Edges_Out (v9,X) ; :: thesis: x in (Edges_Out (v1,X)) \/ { the carrier' of G}
then A5: x in X by Def2;
A6: the Source of (AddNewEdge (v1,v2)) . x = v9 by A4, Def2;

per cases ( x in the carrier' of G or x in { the carrier' of G} ) by A3, A4, XBOOLE_0:def 3;

suppose A7: x in the carrier' of G ; :: thesis: x in (Edges_Out (v1,X)) \/ { the carrier' of G}

then the Source of G . x = v1 by A1, A6, Th35;
then x in Edges_Out (v1,X) by A5, A7, Def2;
hence x in (Edges_Out (v1,X)) \/ { the carrier' of G} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in { the carrier' of G} ; :: thesis: x in (Edges_Out (v1,X)) \/ { the carrier' of G}

hence x in (Edges_Out (v1,X)) \/ { the carrier' of G} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume A8: x in (Edges_Out (v1,X)) \/ { the carrier' of G} ; :: thesis: b₁ in Edges_Out (v9,X)

per cases ( x in Edges_Out (v1,X) or x in { the carrier' of G} ) by A8, XBOOLE_0:def 3;

suppose A9: x in Edges_Out (v1,X) ; :: thesis: b₁ in Edges_Out (v9,X)

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

end;

suppose A11: x in { the carrier' of G} ; :: thesis: b₁ in Edges_Out (v9,X)

A12: the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 by Th34;
( x = the carrier' of G & x in the carrier' of (AddNewEdge (v1,v2)) ) by A3, A11, TARSKI:def 1, XBOOLE_0:def 3;
hence x in Edges_Out (v9,X) by A1, A2, A12, Def2; :: thesis: verum

end;

end;

end;

hence Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} by TARSKI:2; :: thesis: Edges_Out (v1,X) misses { the carrier' of G}
assume (Edges_Out (v1,X)) /\ { the carrier' of G} <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being object such that
A13: x in (Edges_Out (v1,X)) /\ { the carrier' of G} by XBOOLE_0:def 1;
x in { the carrier' of G} by A13, XBOOLE_0:def 4;
then A14: x = the carrier' of G by TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
A: not xx in xx ;
x in the carrier' of G by A13;
hence contradiction by A14, A; :: thesis: verum