set cP = the carrier of R;
set iP = the InternalRel of R;
consider CL being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card CL by Def3;
card { the Element of R} <= card CL by A1;
then CL <> {} ;
then consider y being Element of R such that
y in CL and
A2: y is_maximal_wrt CL, the InternalRel of R by BAGORDER:6;
A3: y is_maximal_in CL by A2, WAYBEL_4:def 24;
A4: the carrier of R = [#] R ;

now :: thesis: y is_maximal_in the carrier of R

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
A5: y < z by WAYBEL_4:55;
A6: y <= z by A5;
set C = CL \/ {z};
reconsider C = CL \/ {z} as finite Clique of R by A6, A3, Th11;
not z in CL by A3, A5, WAYBEL_4:55;
then card C = (card CL) + 1 by CARD_2:41;
then (card CL) + 1 <= (card CL) + 0 by A1;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

hence not maximals R is empty by A4, Def10; :: thesis: verum