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 A1: ( v' = v & v <> v1 & v <> v2 ) ; :: thesis: Degree v',X = Degree v,X
hence Degree v',X = (card (Edges_In v,X)) + (card (Edges_Out v',X)) by Th48
.= Degree v,X by A1, Th49 ;
:: thesis: verum