let x, y be Element of R; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of T holds
( not b₁ = (f | R) . x or not b₂ = (f | R) . y or b₁ <= b₂ ) )
A1: the carrier of R c= the carrier of S by YELLOW_0:def 13;
assume A2: x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of T holds
( not b₁ = (f | R) . x or not b₂ = (f | R) . y or b₁ <= b₂ )
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 b₁, b₂ being Element of the carrier of T holds
( not b₁ = (f | R) . x or not b₂ = (f | R) . y or b₁ <= b₂ ) by A5, A6, WAYBEL_1:def 2; :: thesis: verum