let G2 be GraphComplement of G; :: thesis: G2 is connected
consider G9 being LGraphComplement of G such that
A1: G2 is removeLoops of G9 by Def9;
thus G2 is connected by A1; :: thesis: verum