:: deftheorem Def15 defines clique# SCMYCIEL:def 15 :
for G being with_finite_clique# SimpleGraph
for b₂ being Nat holds
( b₂ = clique# G iff ( ex C being finite Clique of G st order C = b₂ & ( for T being finite Clique of G holds order T <= b₂ ) ) );