let R, S be non empty RelStr ; :: thesis: for a, b being Element of R
for c, d being Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds
( a <= b iff c <= d )
let a, b be Element of R; :: thesis: for c, d being Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds
( a <= b iff c <= d )
let c, d be Element of S; :: thesis: ( a = c & b = d & R tolerates S & R is transitive & S is transitive implies ( a <= b iff c <= d ) )
assume that
A1: ( a = c & b = d ) and
A2: R tolerates S and
A3: R is transitive and
A4: S is transitive ; :: thesis: ( a <= b iff c <= d )
( a in the carrier of R \/ the carrier of S & b in the carrier of R \/ the carrier of S ) by XBOOLE_0:def 3;
then reconsider a9 = a, b9 = b as Element of (R [*] S) by Def2;

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

assume a <= b ; :: thesis: c <= d
then a9 <= b9 by A2, A3, Th8;
hence c <= d by A1, A2, A4, Th9; :: thesis: verum

end;

assume c <= d ; :: thesis: a <= b
then a9 <= b9 by A1, A2, A4, Th9;
hence a <= b by A2, A3, Th8; :: thesis: verum