let R be RelStr ; :: thesis: ( R is finite implies R is with_finite_clique# )
assume R is finite ; :: thesis: R is with_finite_clique#
then reconsider R9 = R as finite RelStr ;
defpred S₁[ Nat] means ex c being finite Clique of R st card c = c₁;
A1: for k being Nat st S₁[k] holds
k <= card R9 by NAT_1:43;
card ({} R) = 0 ;
then A2: ex k being Nat st S₁[k] ;
consider k being Nat such that
A3: S₁[k] and
A4: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A1, A2);
consider c being finite Clique of R such that
A5: card c = k by A3;
for D being finite Clique of R holds card D <= card c by A5, A4;
hence R is with_finite_clique# ; :: thesis: verum