let X be set ; for G being Graph
for v1, v, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge v1,v2) st v9 = v & v <> v2 holds
Edges_In v9,X = Edges_In v,X
let G be Graph; for v1, v, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge v1,v2) st v9 = v & v <> v2 holds
Edges_In v9,X = Edges_In v,X
let v1, v, v2 be Vertex of G; for v9 being Vertex of (AddNewEdge v1,v2) st v9 = v & v <> v2 holds
Edges_In v9,X = Edges_In v,X
let v9 be Vertex of (AddNewEdge v1,v2); ( v9 = v & v <> v2 implies Edges_In v9,X = Edges_In v,X )
assume that
A1:
v9 = v
and
A2:
v <> v2
; Edges_In v9,X = Edges_In v,X
set G9 = AddNewEdge v1,v2;
set E = the carrier' of G;
set T = the Target of G;
set E9 = the carrier' of (AddNewEdge v1,v2);
set T9 = the Target 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 ;
( ( x in Edges_In v9,X implies x in Edges_In v,X ) & ( x in Edges_In v,X implies x in Edges_In v9,X ) )hereby ( x in Edges_In v,X implies x in Edges_In v9,X )
assume A4:
x in Edges_In v9,
X
;
x in Edges_In v,Xthen A5:
x in X
by Def1;
A6:
the
Target of
(AddNewEdge v1,v2) . x = v9
by A4, Def1;
the
Target of
(AddNewEdge v1,v2) . the
carrier' of
G = v2
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
Target of
G . x = v
by A1, A6, Th40;
hence
x in Edges_In v,
X
by A5, A7, Def1;
verum
end; assume A8:
x in Edges_In v,
X
;
x in Edges_In v9,Xthen
the
Target of
G . x = v
by Def1;
then A9:
the
Target of
(AddNewEdge v1,v2) . x = v9
by A1, A8, Th40;
(
x in X &
x in the
carrier' of
(AddNewEdge v1,v2) )
by A3, A8, Def1, XBOOLE_0:def 3;
hence
x in Edges_In v9,
X
by A9, Def1;
verum end;
hence
Edges_In v9,X = Edges_In v,X
by TARSKI:2; verum