let G1 be simple vertex-finite _Graph; :: thesis: for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .degree() = (G1 .order()) - ((v1 .degree()) + 1)
let G2 be GraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .degree() = (G1 .order()) - ((v1 .degree()) + 1)
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
v2 .degree() = (G1 .order()) - ((v1 .degree()) + 1)
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies v2 .degree() = (G1 .order()) - ((v1 .degree()) + 1) )
assume A1: v1 = v2 ; :: thesis: v2 .degree() = (G1 .order()) - ((v1 .degree()) + 1)
v1 .allNeighbors() c= the_Vertices_of G1 ;
then v1 .allNeighbors() c= the_Vertices_of G2 by GLIB_012:98;
then A2: (v1 .allNeighbors()) \/ {v2} c= the_Vertices_of G2 by XBOOLE_1:8;
A3: not v2 in v1 .allNeighbors() by A1, GLIB_000:112;
thus v2 .degree() = card (v2 .allNeighbors()) by GLIB_000:111
.= card ((the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2})) by A1, GLIB_012:118
.= (G2 .order()) - (card ((v1 .allNeighbors()) \/ {v2})) by A2, CARD_2:44
.= (G2 .order()) - ((card (v1 .allNeighbors())) + 1) by A3, CARD_2:41
.= (G1 .order()) - ((card (v1 .allNeighbors())) + 1) by GLIB_012:98
.= (G1 .order()) - ((v1 .degree()) + 1) by GLIB_000:111 ; :: thesis: verum