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₁;
P1: for k being Nat st S₁[k] holds
k <= card R9 by NAT_1:44;
card ({} R) = 0 ;
then P2: ex k being Nat st S₁[k] ;
consider k being Nat such that
B: S₁[k] and
C: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(P1, P2);
consider c being finite Clique of R such that
D: card c = k by B;
for D being finite Clique of R holds card D <= card c by D, C;
hence R is with_finite_clique# by Lfheight; :: thesis: verum