let x, y be Element of R; ORDERS_3:def 5 ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 ) )
A1:
the carrier of R c= the carrier of S
by YELLOW_0:def 13;
assume A2:
x <= y
; for b1, b2 being Element of the carrier of T holds
( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 )
then A3:
[x,y] in the InternalRel of R
;
then A4:
x in the carrier of R
by ZFMISC_1:87;
y in the carrier of R
by A3, ZFMISC_1:87;
then reconsider a = x, b = y as Element of S by A1;
A5:
a <= b
by A2, YELLOW_0:59;
A6:
f . b = (f | R) . y
by A4, Th6;
f . a = (f | R) . x
by A4, Th6;
hence
for b1, b2 being Element of the carrier of T holds
( not b1 = (f | R) . x or not b2 = (f | R) . y or b1 <= b2 )
by A5, A6, WAYBEL_1:def 2; verum