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_maximal_wrt CL, the InternalRel of R by BAGORDER:7;
E: y is_maximal_in CL by D, WAYBEL_4:def 25;
F: the carrier of R = [#] R ;

now

assume not y is_maximal_in the carrier of R ; :: thesis: contradiction
then consider z being Element of R such that
z in the carrier of R and
C1: y < z by WAYBEL_4:56;
D1: y <= z by C1, ORDERS_2:def 10;
set C = CL \/ {z};
reconsider C = CL \/ {z} as finite Clique of R by D1, E, ExtClique;
not z in CL by E, C1, WAYBEL_4:56;
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 maximals R is empty by F, Lmax; :: thesis: verum