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 by ORDERS_2:def 9;
then A4: x in the carrier of R by ZFMISC_1:106;
y in the carrier of R by A3, ZFMISC_1:106;
then reconsider a = x, b = y as Element of S by A4, A1;
A5: a <= b by A2, YELLOW_0:60;
A6: f . b = (f | R) . y by A4, Th7;
f . a = (f | R) . x by A4, Th7;
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