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;

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

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;

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

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

end;

suppose
IT1 <= IT2
; :: thesis: contradiction

then
[IT1,IT2] in the InternalRel of R
by ORDERS_2:def 5;

then IT1 in the InternalRel of R -Seg IT2 by A9, WELLORD1: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:6; :: thesis: verum

end;then IT1 in the InternalRel of R -Seg IT2 by A9, WELLORD1: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:6; :: thesis: verum

suppose
IT2 <= IT1
; :: thesis: contradiction

then
[IT2,IT1] in the InternalRel of R
by ORDERS_2:def 5;

then IT2 in the InternalRel of R -Seg IT1 by A9, WELLORD1: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:6; :: thesis: verum

end;then IT2 in the InternalRel of R -Seg IT1 by A9, WELLORD1: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:6; :: thesis: verum