theorem Th47: :: SCMYCIEL:47
for G being SimpleGraph st ( for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
{x,y} in Edges G ) holds
G is clique