set IR = the InternalRel of R;
( X c= the carrier of R & X is finite ) by FINSUB_1:def 5;
then consider x being Element of R such that
A6: ( x in X & x is_maximal_wrt X,the InternalRel of R ) by A1, Th7;
take x ; :: thesis: ( x in X & x is_maximal_wrt X,the InternalRel of R )
thus ( x in X & x is_maximal_wrt X,the InternalRel of R ) by A6; :: thesis: verum