set G1 = the LGraphComplement of G;
take the removeLoops of the LGraphComplement of G ; :: thesis: ex G9 being LGraphComplement of G st the removeLoops of the LGraphComplement of G is removeLoops of G9
thus ex G9 being LGraphComplement of G st the removeLoops of the LGraphComplement of G is removeLoops of G9 ; :: thesis: verum