:: deftheorem defines maximal_clique COMBGRAS:def 3 :
for S being IncProjStr
for K being Subset of the Points of S holds
( K is maximal_clique iff ( K is clique & ( for U being Subset of the Points of S st U is clique & K c= U holds
U = K ) ) );