thus ( f is antitone implies for x, y being Element of S st x <= y holds
f . x >= f . y ) by WAYBEL_0:def 5; :: thesis: ( ( for x, y being Element of S st x <= y holds
f . x >= f . y ) implies f is antitone )
assume for x, y being Element of S st x <= y holds
f . x >= f . y ; :: thesis: f is antitone
hence for x, y being Element of S st x <= y holds
for a, b being Element of T st a = f . x & b = f . y holds
a >= b ; :: according to WAYBEL_0:def 5 :: thesis: verum