let H be GraphComplement of G; :: thesis: H is regular
consider n being Nat such that
A1: G is n -regular by Def7;
H is (G .order()) -' (n + 1) -regular by A1, Th26;
hence H is regular ; :: thesis: verum