set cP = the carrier of R;
set iP = the InternalRel of R;
consider CL being finite Clique of R such that
AA: for D being finite Clique of R holds card D <= card CL by Lfheight;
card {the Element of R} <= card CL by AA;
then CL <> {} ;
then consider y being Element of R such that
y in CL and
D: y is_minimal_wrt CL,the InternalRel of R by BAGORDER:8;
E: y is_minimal_in CL by D, WAYBEL_4:def 27;
F: the carrier of R = [#] R ;

now

assume not y is_minimal_in the carrier of R ; :: thesis: contradiction
then consider z being Element of R such that
z in the carrier of R and
C1: z < y by WAYBEL_4:57;
D1: z <= y by C1, ORDERS_2:def 10;
set C = CL \/ {z};
reconsider C = CL \/ {z} as finite Clique of R by D1, E, ExtCliquemin;
not z in CL by E, C1, WAYBEL_4:57;
then card C = (card CL) + 1 by CARD_2:54;
then (card CL) + 1 <= (card CL) + 0 by AA;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

hence not minimals R is empty by F, Lmin; :: thesis: verum