let G1 be Dsimple vertex-finite _Graph; :: thesis: for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() = (G1 .order()) - ((v1 .inDegree()) + 1) & v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) & v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) )
let G2 be DGraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() = (G1 .order()) - ((v1 .inDegree()) + 1) & v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) & v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() = (G1 .order()) - ((v1 .inDegree()) + 1) & v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) & v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v2 .inDegree() = (G1 .order()) - ((v1 .inDegree()) + 1) & v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) & v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) ) )
assume A1: v1 = v2 ; :: thesis: ( v2 .inDegree() = (G1 .order()) - ((v1 .inDegree()) + 1) & v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) & v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) )
v1 .inNeighbors() c= the_Vertices_of G1 ;
then v1 .inNeighbors() c= the_Vertices_of G2 by GLIB_012:80;
then A2: (v1 .inNeighbors()) \/ {v2} c= the_Vertices_of G2 by XBOOLE_1:8;
v1 .outNeighbors() c= the_Vertices_of G1 ;
then v1 .outNeighbors() c= the_Vertices_of G2 by GLIB_012:80;
then A3: (v1 .outNeighbors()) \/ {v2} c= the_Vertices_of G2 by XBOOLE_1:8;
not v1 in v1 .allNeighbors() by GLIB_000:112;
then A4: ( not v2 in v1 .inNeighbors() & not v2 in v1 .outNeighbors() ) by A1, XBOOLE_0:def 3;
thus A5: v2 .inDegree() = card (v2 .inNeighbors()) by GLIB_000:109
.= card ((the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2})) by A1, GLIB_012:95
.= (G2 .order()) - (card ((v1 .inNeighbors()) \/ {v2})) by A2, CARD_2:44
.= (G2 .order()) - ((card (v1 .inNeighbors())) + 1) by A4, CARD_2:41
.= (G1 .order()) - ((card (v1 .inNeighbors())) + 1) by GLIB_012:80
.= (G1 .order()) - ((v1 .inDegree()) + 1) by GLIB_000:109 ; :: thesis: ( v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) & v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) )
thus v2 .outDegree() = card (v2 .outNeighbors()) by GLIB_000:110
.= card ((the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2})) by A1, GLIB_012:95
.= (G2 .order()) - (card ((v1 .outNeighbors()) \/ {v2})) by A3, CARD_2:44
.= (G2 .order()) - ((card (v1 .outNeighbors())) + 1) by A4, CARD_2:41
.= (G1 .order()) - ((card (v1 .outNeighbors())) + 1) by GLIB_012:80
.= (G1 .order()) - ((v1 .outDegree()) + 1) by GLIB_000:110 ; :: thesis: v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2)
hence v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) by A5; :: thesis: verum