:: deftheorem defines Complement SCMYCIEL:def 11 :
for G being SimpleGraph holds Complement G = (CompleteSGraph (Vertices G)) \ (Edges G);