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
A4: ( IT1 in C & IT1 is_minimal_wrt C,the InternalRel of R ) and
A5: ( IT2 in C & IT2 is_minimal_wrt C,the InternalRel of R ) ; :: thesis: IT1 = IT2
set IR = the InternalRel of R;

now

assume A6: 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 A6, WELLORD1:def 1;
then IT1 in (the InternalRel of R -Seg IT2) /\ C by A4, XBOOLE_0:def 4;
then the InternalRel of R -Seg IT2 meets C by XBOOLE_0:def 7;
hence contradiction by A5, 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 A6, WELLORD1:def 1;
then IT2 in (the InternalRel of R -Seg IT1) /\ C by A5, XBOOLE_0:def 4;
then the InternalRel of R -Seg IT1 meets C by XBOOLE_0:def 7;
hence contradiction by A4, DICKSON:7; :: thesis: verum

end;

end;

end;

hence IT1 = IT2 ; :: thesis: verum