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

A2: x in X and

A3: x is_minimal_wrt X, the InternalRel of R by A1, Th6;

take x ; :: thesis: ( x in X & x is_minimal_wrt X, the InternalRel of R )

thus ( x in X & x is_minimal_wrt X, the InternalRel of R ) by A2, A3; :: thesis: verum

X c= the carrier of R by FINSUB_1:def 5;

then consider x being Element of R such that

A2: x in X and

A3: x is_minimal_wrt X, the InternalRel of R by A1, Th6;

take x ; :: thesis: ( x in X & x is_minimal_wrt X, the InternalRel of R )

thus ( x in X & x is_minimal_wrt X, the InternalRel of R ) by A2, A3; :: thesis: verum