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