theorem Th54: :: SCMYCIEL:54

for G being with_finite_clique# SimpleGraph st clique# G = 0 holds
Vertices G = {}