set cP = the carrier of R;
set iP = the InternalRel of R;
consider CL being finite Clique of R such that
A7: for D being finite Clique of R holds card D <= card CL by Def3;
card { the Element of R} <= card CL by A7;
then CL <> {} ;
then consider y being Element of R such that
y in CL and
A8: y is_minimal_wrt CL, the InternalRel of R by BAGORDER:7;
A9: y is_minimal_in CL by A8, WAYBEL_4:def 26;
A10: the carrier of R = [#] R ;
now :: thesis: y is_minimal_in the carrier of R
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
A11: z < y by WAYBEL_4:56;
A12: z <= y by A11;
set C = CL \/ {z};
reconsider C = CL \/ {z} as finite Clique of R by A12, A9, Th12;
not z in CL by A9, A11, WAYBEL_4:56;
then card C = (card CL) + 1 by CARD_2:41;
then (card CL) + 1 <= (card CL) + 0 by A7;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
hence not minimals R is empty by A10, Def9; :: thesis: verum