thus ( f is monotone implies for x, y being Element of L1 st x <= y holds
f . x <= f . y ) by ORDERS_3:def 5; :: thesis: ( ( for x, y being Element of L1 st x <= y holds
f . x <= f . y ) implies f is monotone )
assume for x, y being Element of L1 st x <= y holds
f . x <= f . y ; :: thesis: f is monotone
hence for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b ; :: according to ORDERS_3:def 5 :: thesis: verum