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

A11: IT1 in X and

A12: IT1 is_maximal_wrt X, the InternalRel of R and

A13: IT2 in X and

A14: IT2 is_maximal_wrt X, the InternalRel of R ; :: thesis: IT1 = IT2

set IR = the InternalRel of R;

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

assume that

A11: IT1 in X and

A12: IT1 is_maximal_wrt X, the InternalRel of R and

A13: IT2 in X and

A14: IT2 is_maximal_wrt X, the InternalRel of R ; :: thesis: IT1 = IT2

set IR = the InternalRel of R;

A15: ( 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 A15, ORDERS_2:def 5;

end;