let H be DGraphComplement of G; :: thesis: H is Dregular
consider n being Nat such that
A1: G is n -Dregular by Def10;
H is (G .order()) -' (n + 1) -Dregular by A1, Th49;
hence H is Dregular ; :: thesis: verum