let R, S be non empty RelStr ; 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; 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); ( x = a & y = b & R tolerates S & R is transitive implies ( x <= y iff a <= b ) )
assume A1:
( x = a & y = b )
; ( not R tolerates S or not R is transitive or ( x <= y iff a <= b ) )
assume A2:
( R tolerates S & R is transitive )
; ( x <= y iff a <= b )
hereby ( a <= b implies x <= y )
end;
assume
a <= b
; 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; verum