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