( the_Edges_of G = {} & G .loops() = {} ) ;
hence for b₁ being GraphComplement of G holds b₁ is complete by Th113; :: thesis: verum