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, Th48
.= Degree v,X by A1, A2, Th49 ; :: thesis: verum