let X be set ; 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; 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; 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)); ( 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
; ( 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;
hence
Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G}
by TARSKI:2; Edges_Out (v1,X) misses { the carrier' of G}
assume
(Edges_Out (v1,X)) /\ { the carrier' of G} <> {}
; XBOOLE_0:def 7 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; verum