consider c being Element of T;
take f = S --> c; :: thesis: f is monotone
let x, y be Element of S; :: 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 . x or not b₂ = f . y or b₁ <= b₂ ) )
assume [x,y] in the InternalRel of S ; :: according to ORDERS_2:def 9 :: thesis: for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ )
then A1: ( x in the carrier of S & y in the carrier of S ) by ZFMISC_1:106;
A2: f = the carrier of S --> c by BORSUK_1:def 2;
let a, b be Element of T; :: thesis: ( not a = f . x or not b = f . y or a <= b )
assume ( a = f . x & b = f . y ) ; :: thesis: a <= b
then ( a = c & b = c ) by A1, A2, FUNCOP_1:13;
hence a <= b ; :: thesis: verum