let IT1, IT2 be Element of R; :: thesis: ( IT1 in C & IT1 is_minimal_wrt C, the InternalRel of R & IT2 in C & IT2 is_minimal_wrt C, the InternalRel of R implies IT1 = IT2 )
assume that
A5: IT1 in C and
A6: IT1 is_minimal_wrt C, the InternalRel of R and
A7: IT2 in C and
A8: IT2 is_minimal_wrt C, the InternalRel of R ; :: thesis: IT1 = IT2
set IR = the InternalRel of R;

now

assume A9: IT1 <> IT2 ; :: thesis: contradiction

per cases ( IT1 <= IT2 or IT2 <= IT1 ) by WAYBEL_0:def 29;

suppose IT1 <= IT2 ; :: thesis: contradiction

then [IT1,IT2] in the InternalRel of R by ORDERS_2:def 9;
then IT1 in the InternalRel of R -Seg IT2 by A9, WELLORD1:def 1;
then IT1 in ( the InternalRel of R -Seg IT2) /\ C by A5, XBOOLE_0:def 4;
then the InternalRel of R -Seg IT2 meets C by XBOOLE_0:def 7;
hence contradiction by A8, DICKSON:7; :: thesis: verum

end;

suppose IT2 <= IT1 ; :: thesis: contradiction

then [IT2,IT1] in the InternalRel of R by ORDERS_2:def 9;
then IT2 in the InternalRel of R -Seg IT1 by A9, WELLORD1:def 1;
then IT2 in ( the InternalRel of R -Seg IT1) /\ C by A7, XBOOLE_0:def 4;
then the InternalRel of R -Seg IT1 meets C by XBOOLE_0:def 7;
hence contradiction by A6, DICKSON:7; :: thesis: verum

end;

end;

end;

hence IT1 = IT2 ; :: thesis: verum