let G2 be DGraphComplement of G; :: thesis: G2 is connected
consider G9 being DLGraphComplement of G such that
A1: G2 is removeLoops of G9 by Def8;
thus G2 is connected by A1; :: thesis: verum