let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; :: thesis: for x, y being Element of (R [*] S) st x in the carrier of R & y in the carrier of S & R tolerates S holds
( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
let x, y be Element of (R [*] S); :: thesis: ( x in the carrier of R & y in the carrier of S & R tolerates S implies ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) ) )
assume A1: ( x in the carrier of R & y in the carrier of S & R tolerates S ) ; :: thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )

per cases ( [x,y] in the InternalRel of R or [x,y] in the InternalRel of S or ( not [x,y] in the InternalRel of R & not [x,y] in the InternalRel of S ) ) ;

suppose A2: [x,y] in the InternalRel of R ; :: thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )

hereby :: thesis: ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y )

assume A3: x <= y ; :: thesis: ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
A4: y in the carrier of R by A2, ZFMISC_1:106;
take a = y; :: thesis: ( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
thus a in the carrier of R /\ the carrier of S by A1, A4, XBOOLE_0:def 4; :: thesis: ( x <= a & a <= y )
R [*] S is reflexive by Th3;
hence ( x <= a & a <= y ) by A3, ORDERS_2:24; :: thesis: verum

end;

[x,y] in the InternalRel of (R [*] S) by A2, Th6;
hence ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y ) by ORDERS_2:def 9; :: thesis: verum

end;

suppose A5: [x,y] in the InternalRel of S ; :: thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )

hereby :: thesis: ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y )

assume A6: x <= y ; :: thesis: ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
A7: x in the carrier of S by A5, ZFMISC_1:106;
take a = x; :: thesis: ( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
thus a in the carrier of R /\ the carrier of S by A1, A7, XBOOLE_0:def 4; :: thesis: ( x <= a & a <= y )
R [*] S is reflexive by Th3;
hence ( x <= a & a <= y ) by A6, ORDERS_2:24; :: thesis: verum

end;

[x,y] in the InternalRel of (R [*] S) by A5, Th6;
hence ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y ) by ORDERS_2:def 9; :: thesis: verum

end;

suppose that A8: not [x,y] in the InternalRel of R and
A9: not [x,y] in the InternalRel of S ; :: thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )

hereby :: thesis: ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y )

assume x <= y ; :: thesis: ex z being Element of (R [*] S) st
( z in the carrier of R /\ the carrier of S & x <= z & z <= y )
then [x,y] in the InternalRel of (R [*] S) by ORDERS_2:def 9;
then [x,y] in (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by Def2;
then ( [x,y] in the InternalRel of R \/ the InternalRel of S or [x,y] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def 3;
then consider z being set such that
A10: ( [x,z] in the InternalRel of R & [z,y] in the InternalRel of S ) by A8, A9, RELAT_1:def 8, XBOOLE_0:def 3;
A11: z in the carrier of R by A10, ZFMISC_1:106;
A12: z in the carrier of S by A10, ZFMISC_1:106;
then z in the carrier of R \/ the carrier of S by XBOOLE_0:def 3;
then reconsider z = z as Element of (R [*] S) by Def2;
take z = z; :: thesis: ( z in the carrier of R /\ the carrier of S & x <= z & z <= y )
thus z in the carrier of R /\ the carrier of S by A11, A12, XBOOLE_0:def 4; :: thesis: ( x <= z & z <= y )
[x,z] in the InternalRel of (R [*] S) by A10, Th6;
hence x <= z by ORDERS_2:def 9; :: thesis: z <= y
[z,y] in the InternalRel of (R [*] S) by A10, Th6;
hence z <= y by ORDERS_2:def 9; :: thesis: verum

end;

given a being Element of (R [*] S) such that A13: ( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) ; :: thesis: x <= y
reconsider x' = x, a' = a as Element of R by A1, A13, Th12;
reconsider y' = y, a1 = a as Element of S by A1, A13, Th13;
x' <= a' by A1, A13, Th8;
then A14: [x,a] in the InternalRel of R by ORDERS_2:def 9;
a1 <= y' by A1, A13, Th9;
then [a,y] in the InternalRel of S by ORDERS_2:def 9;
then [x,y] in the InternalRel of R * the InternalRel of S by A14, RELAT_1:def 8;
then [x,y] in (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;
then [x,y] in the InternalRel of (R [*] S) by Def2;
hence x <= y by ORDERS_2:def 9; :: thesis: verum

end;

end;