let X be set ; for G being Graph
for v, v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v1 holds
Edges_Out (v9,X) = Edges_Out (v,X)
let G be Graph; for v, v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v1 holds
Edges_Out (v9,X) = Edges_Out (v,X)
let v, v1, v2 be Vertex of G; for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v1 holds
Edges_Out (v9,X) = Edges_Out (v,X)
let v9 be Vertex of (AddNewEdge (v1,v2)); ( v9 = v & v <> v1 implies Edges_Out (v9,X) = Edges_Out (v,X) )
assume that
A1:
v9 = v
and
A2:
v <> v1
; Edges_Out (v9,X) = Edges_Out (v,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 for x being object holds
( ( x in Edges_Out (v9,X) implies x in Edges_Out (v,X) ) & ( x in Edges_Out (v,X) implies x in Edges_Out (v9,X) ) )let x be
object ;
( ( x in Edges_Out (v9,X) implies x in Edges_Out (v,X) ) & ( x in Edges_Out (v,X) implies x in Edges_Out (v9,X) ) )hereby ( x in Edges_Out (v,X) implies x in Edges_Out (v9,X) )
assume A4:
x in Edges_Out (
v9,
X)
;
x in Edges_Out (v,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 Th34;
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 = v
by A1, A6, Th35;
hence
x in Edges_Out (
v,
X)
by A5, A7, Def2;
verum
end; assume A8:
x in Edges_Out (
v,
X)
;
x in Edges_Out (v9,X)then
the
Source of
G . x = v
by Def2;
then A9:
the
Source of
(AddNewEdge (v1,v2)) . x = v9
by A1, A8, Th35;
(
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;
verum end;
hence
Edges_Out (v9,X) = Edges_Out (v,X)
by TARSKI:2; verum