:: deftheorem Def3 defines with_finite_clique# DILWORTH:def 3 :
for R being RelStr holds
( R is with_finite_clique# iff ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C );