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 that
A1: x in the carrier of R and
A2: y in the carrier of S and
A3: 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 A4: [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 A5: 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 )
take a = y; :: thesis: ( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
y in the carrier of R by A4, ZFMISC_1:87;
hence a in the carrier of R /\ the carrier of S by A2, XBOOLE_0:def 4; :: thesis: ( x <= a & a <= y )
R [*] S is reflexive by Th3;
hence ( x <= a & a <= y ) by A5, ORDERS_2:1; :: thesis: verum
end;
[x,y] in the InternalRel of (R [*] S) by A4, 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 5; :: thesis: verum
end;
suppose A6: [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 A7: 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 )
take a = x; :: thesis: ( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
x in the carrier of S by A6, ZFMISC_1:87;
hence a in the carrier of R /\ the carrier of S by A1, XBOOLE_0:def 4; :: thesis: ( x <= a & a <= y )
R [*] S is reflexive by Th3;
hence ( x <= a & a <= y ) by A7, ORDERS_2:1; :: thesis: verum
end;
[x,y] in the InternalRel of (R [*] S) by A6, 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 5; :: thesis: verum
end;
suppose A8: ( not [x,y] in the InternalRel of R & 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 5;
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 object such that
A9: [x,z] in the InternalRel of R and
A10: [z,y] in the InternalRel of S by A8, RELAT_1:def 8, XBOOLE_0:def 3;
A11: z in the carrier of R by A9, ZFMISC_1:87;
A12: z in the carrier of S by A10, ZFMISC_1:87;
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 A9, Th6;
hence x <= z by ORDERS_2:def 5; :: thesis: z <= y
[z,y] in the InternalRel of (R [*] S) by A10, Th6;
hence z <= y by ORDERS_2:def 5; :: thesis: verum
end;
given a being Element of (R [*] S) such that A13: a in the carrier of R /\ the carrier of S and
A14: x <= a and
A15: a <= y ; :: thesis: x <= y
reconsider y9 = y, a1 = a as Element of S by A2, A13, Th13;
a1 <= y9 by A3, A15, Th9;
then A16: [a,y] in the InternalRel of S by ORDERS_2:def 5;
reconsider x9 = x, a9 = a as Element of R by A1, A13, Th12;
x9 <= a9 by A3, A14, Th8;
then [x,a] in the InternalRel of R by ORDERS_2:def 5;
then [x,y] in the InternalRel of R * the InternalRel of S by A16, 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 5; :: thesis: verum
end;
end;