let n be Nat; :: thesis: for G1 being simple vertex-finite n -regular _Graph
for G2 being GraphComplement of G1 holds G2 is (G1 .order()) -' (n + 1) -regular
let G1 be simple vertex-finite n -regular _Graph; :: thesis: for G2 being GraphComplement of G1 holds G2 is (G1 .order()) -' (n + 1) -regular
let G2 be GraphComplement of G1; :: thesis: G2 is (G1 .order()) -' (n + 1) -regular
let v2 be Vertex of G2; :: according to GLIB_016:def 4 :: thesis: v2 .degree() = (G1 .order()) -' (n + 1)
reconsider v1 = v2 as Vertex of G1 by GLIB_012:98;
v1 .degree() < G1 .order() by GLIBPRE1:114;
then n < G1 .order() by Def4;
then A1: n + 1 <= G1 .order() by NAT_1:13;
thus v2 .degree() = (G1 .order()) - ((v1 .degree()) + 1) by GLIBPRE1:112
.= ((G1 .order()) + 0) - (n + 1) by Def4
.= (G1 .order()) -' (n + 1) by A1, NAT_D:37 ; :: thesis: verum