let X be set ; 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; 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; 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)); ( 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
; 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
;
Degree (v9,X) = (Degree (v,X)) + 1then
(
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
;
verum end; suppose A6:
v = v2
;
Degree (v9,X) = (Degree (v,X)) + 1then
(
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
;
verum end;