let R, S be non empty RelStr ; :: thesis: for x, y being Element of R
for a, b being Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds
( x <= y iff a <= b )
let x, y be Element of R; :: thesis: for a, b being Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds
( x <= y iff a <= b )
let a, b be Element of (R [*] S); :: thesis: ( x = a & y = b & R tolerates S & R is transitive implies ( x <= y iff a <= b ) )
assume A1: ( x = a & y = b ) ; :: thesis: ( not R tolerates S or not R is transitive or ( x <= y iff a <= b ) )
assume A2: ( R tolerates S & R is transitive ) ; :: thesis: ( x <= y iff a <= b )

hereby :: thesis: ( a <= b implies x <= y )

assume x <= y ; :: thesis: a <= b
then [x,y] in the InternalRel of R by ORDERS_2:def 5;
then [a,b] in the InternalRel of (R [*] S) by A1, Th6;
hence a <= b by ORDERS_2:def 5; :: thesis: verum

end;

assume a <= b ; :: thesis: x <= y
then [a,b] in the InternalRel of (R [*] S) by ORDERS_2:def 5;
then [x,y] in the InternalRel of R by A1, A2, Th4;
hence x <= y by ORDERS_2:def 5; :: thesis: verum