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

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

suppose A5: v = v1 ; :: thesis: Degree v9,X = (Degree v,X) + 1

then ( Edges_In v9,X = Edges_In v,X & Edges_Out v9,X = (Edges_Out v,X) \/ {the carrier' of G} ) by A1, A2, A4, Th44, Th46;
hence Degree v9,X = (card (Edges_In v,X)) + ((card (Edges_Out v,X)) + (card {the carrier' of G})) by A1, A4, A5, Th46, 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 v9,X = (Degree v,X) + 1

then ( Edges_Out v9,X = Edges_Out v,X & Edges_In v9,X = (Edges_In v,X) \/ {the carrier' of G} ) by A1, A2, A4, Th45, Th47;
hence Degree v9,X = ((card (Edges_In v,X)) + (card {the carrier' of G})) + (card (Edges_Out v,X)) by A1, A4, A6, Th47, 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;