let R, S be non empty RelStr ; 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; 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; ( 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
; ( 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 ( c <= d implies a <= b )
end;
assume
c <= d
; a <= b
then
a9 <= b9
by A1, A2, A4, Th9;
hence
a <= b
by A2, A3, Th8; verum