set c = the Element of T;
take f = S --> the Element of T; :: 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 5 :: 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 by ZFMISC_1:87;
let a, b be Element of T; :: thesis: ( not a = f . x or not b = f . y or a <= b )
assume that
A2: a = f . x and
A3: b = f . y ; :: thesis: a <= b
a = the Element of T by A1, A2, FUNCOP_1:7;
hence a <= b by A1, A3, FUNCOP_1:7; :: thesis: verum