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

hereby :: thesis: ( c <= d implies a <= b )

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

end;

assume c <= d ; :: thesis: a <= b
then [c,d] in the InternalRel of S 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