let X be set ; :: thesis: for G being finite Graph
for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v <> v1 & v <> v2 holds
Degree v',X = Degree v,X
let G be finite Graph; :: thesis: for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v <> v1 & v <> v2 holds
Degree v',X = Degree v,X
let v, v1, v2 be Vertex of G; :: thesis: for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v <> v1 & v <> v2 holds
Degree v',X = Degree v,X
let v' be Vertex of (AddNewEdge v1,v2); :: thesis: ( v' = v & v <> v1 & v <> v2 implies Degree v',X = Degree v,X )
assume that
A1: v' = v and
A2: v <> v1 and
A3: v <> v2 ; :: thesis: Degree v',X = Degree v,X
thus Degree v',X = (card (Edges_In v,X)) + (card (Edges_Out v',X)) by A1, A3, Th48
.= Degree v,X by A1, A2, Th49 ; :: thesis: verum