let X be set ; :: thesis: for G being finite Graph
for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v1 <> v2 & ( v = v1 or v = v2 ) & the carrier' of G in X holds
Degree v',X = (Degree v,X) + 1
let G be finite Graph; :: thesis: for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v1 <> v2 & ( v = v1 or v = v2 ) & the carrier' of G in X holds
Degree v',X = (Degree v,X) + 1
let v, v1, v2 be Vertex of G; :: thesis: for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v1 <> v2 & ( v = v1 or v = v2 ) & the carrier' of G in X holds
Degree v',X = (Degree v,X) + 1
let v' be Vertex of (AddNewEdge v1,v2); :: thesis: ( v' = v & v1 <> v2 & ( v = v1 or v = v2 ) & the carrier' of G in X implies Degree v',X = (Degree v,X) + 1 )
assume that
A1: ( v' = v & v1 <> v2 ) and
A2: ( v = v1 or v = v2 ) and
A3: the carrier' of G in X ; :: thesis: Degree v',X = (Degree v,X) + 1
set E = the carrier' of G;

per cases ( v = v1 or v = v2 ) by A2;

suppose A4: v = v1 ; :: thesis: Degree v',X = (Degree v,X) + 1

then A5: Edges_In v',X = Edges_In v,X by A1, Th44;
( Edges_Out v',X = (Edges_Out v,X) \/ {the carrier' of G} & Edges_Out v,X misses {the carrier' of G} ) by A1, A3, A4, Th46;
hence Degree v',X = (card (Edges_In v,X)) + ((card (Edges_Out v,X)) + (card {the carrier' of G})) by A5, CARD_2:53
.= ((card (Edges_In v,X)) + (card (Edges_Out v,X))) + (card {the carrier' of G})
.= (Degree v,X) + 1 by CARD_1:50 ;
:: thesis: verum

end;

suppose A6: v = v2 ; :: thesis: Degree v',X = (Degree v,X) + 1

then A7: Edges_Out v',X = Edges_Out v,X by A1, Th45;
( Edges_In v',X = (Edges_In v,X) \/ {the carrier' of G} & Edges_In v,X misses {the carrier' of G} ) by A1, A3, A6, Th47;
hence Degree v',X = ((card (Edges_In v,X)) + (card {the carrier' of G})) + (card (Edges_Out v,X)) by A7, CARD_2:53
.= ((card (Edges_In v,X)) + (card (Edges_Out v,X))) + (card {the carrier' of G})
.= (Degree v,X) + 1 by CARD_1:50 ;
:: thesis: verum

end;

end;