let n be Nat; :: thesis: for G1 being Dsimple vertex-finite n -Dregular _Graph
for G2 being DGraphComplement of G1 holds G2 is (G1 .order()) -' (n + 1) -Dregular
let G1 be Dsimple vertex-finite n -Dregular _Graph; :: thesis: for G2 being DGraphComplement of G1 holds G2 is (G1 .order()) -' (n + 1) -Dregular
let G2 be DGraphComplement of G1; :: thesis: G2 is (G1 .order()) -' (n + 1) -Dregular
let v2 be Vertex of G2; :: according to GLIB_016:def 8 :: thesis: ( v2 .inDegree() = (G1 .order()) -' (n + 1) & v2 .outDegree() = (G1 .order()) -' (n + 1) )
reconsider v1 = v2 as Vertex of G1 by GLIB_012:80;
v1 .inDegree() < G1 .order() by GLIBPRE1:113;
then n < G1 .order() by Def8;
then A1: n + 1 <= G1 .order() by NAT_1:13;
thus v2 .inDegree() = (G1 .order()) - ((v1 .inDegree()) + 1) by GLIBPRE1:111
.= ((G1 .order()) + 0) - (n + 1) by Def8
.= (G1 .order()) -' (n + 1) by A1, NAT_D:37 ; :: thesis: v2 .outDegree() = (G1 .order()) -' (n + 1)
thus v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) by GLIBPRE1:111
.= ((G1 .order()) + 0) - (n + 1) by Def8
.= (G1 .order()) -' (n + 1) by A1, NAT_D:37 ; :: thesis: verum