:: deftheorem Def4 defines clique# DILWORTH:def 4 :
for R being with_finite_clique# RelStr
for b₂ being Nat holds
( b₂ = clique# R iff ( ex C being finite Clique of R st card C = b₂ & ( for T being finite Clique of R holds card T <= b₂ ) ) );