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 & v <> v1 & v <> v2 holds
Degree (v9,X) = Degree (v,X)
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 & v <> v1 & v <> v2 holds
Degree (v9,X) = Degree (v,X)
let v, v1, v2 be Vertex of G; :: thesis: for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v1 & v <> v2 holds
Degree (v9,X) = Degree (v,X)
let v9 be Vertex of (AddNewEdge (v1,v2)); :: thesis: ( v9 = v & v <> v1 & v <> v2 implies Degree (v9,X) = Degree (v,X) )
assume that
A1: v9 = v and
A2: v <> v1 and
A3: v <> v2 ; :: thesis: Degree (v9,X) = Degree (v,X)
thus Degree (v9,X) = (card (Edges_In (v,X))) + (card (Edges_Out (v9,X))) by A1, A3, Th43
.= Degree (v,X) by A1, A2, Th44 ; :: thesis: verum