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, Th39, Th41;
hence Degree (v9,X) = (card (Edges_In (v,X))) + ((card (Edges_Out (v,X))) + (card { the carrier' of G})) by A1, A4, A5, Th41, CARD_2:40
.= ((card (Edges_In (v,X))) + (card (Edges_Out (v,X)))) + (card { the carrier' of G})
.= (Degree (v,X)) + 1 by CARD_1:30 ;
:: 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, Th40, Th42;
hence Degree (v9,X) = ((card (Edges_In (v,X))) + (card { the carrier' of G})) + (card (Edges_Out (v,X))) by A1, A4, A6, Th42, CARD_2:40
.= ((card (Edges_In (v,X))) + (card (Edges_Out (v,X)))) + (card { the carrier' of G})
.= (Degree (v,X)) + 1 by CARD_1:30 ;
:: thesis: verum

end;

end;