let IT1, IT2 be Element of R; :: thesis: ( IT1 in X & IT1 is_maximal_wrt X,the InternalRel of R & IT2 in X & IT2 is_maximal_wrt X,the InternalRel of R implies IT1 = IT2 )
assume that
A7: ( IT1 in X & IT1 is_maximal_wrt X,the InternalRel of R ) and
A8: ( IT2 in X & IT2 is_maximal_wrt X,the InternalRel of R ) ; :: thesis: IT1 = IT2
set IR = the InternalRel of R;
A9: ( IT1 <= IT2 or IT2 <= IT1 ) by WAYBEL_0:def 29;

per cases ( [IT1,IT2] in the InternalRel of R or [IT2,IT1] in the InternalRel of R ) by A9, ORDERS_2:def 9;

suppose [IT1,IT2] in the InternalRel of R ; :: thesis: IT1 = IT2

hence IT1 = IT2 by A7, A8, WAYBEL_4:def 24; :: thesis: verum

end;

suppose [IT2,IT1] in the InternalRel of R ; :: thesis: IT1 = IT2

hence IT1 = IT2 by A7, A8, WAYBEL_4:def 24; :: thesis: verum

end;

end;