set IR = the InternalRel of R;
X c= the carrier of R by FINSUB_1:def 5;
then consider x being Element of R such that
A8: x in X and
A9: x is_maximal_wrt X, the InternalRel of R by B1, Th6;
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 A8, A9; :: thesis: verum