consider c being Element of T;
take f = S --> c; :: thesis: f is antitone
let x, y be Element of S; :: according to WAYBEL_0: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₁ )
A1: f = the carrier of S --> c ;
let a, b be Element of T; :: thesis: ( not a = f . x or not b = f . y or b <= a )
assume ( a = f . x & b = f . y ) ; :: thesis: b <= a
then ( a = c & b = c ) by A1, FUNCOP_1:13;
hence b <= a ; :: thesis: verum