theorem Th49: :: SCMYCIEL:49

for X being set holds CompleteSGraph X is clique by Lm1;