let f be UnOp of [.0,1.]; ( f is non-increasing iff for a, b being Element of [.0,1.] st a <= b holds
f . a >= f . b )
dom f = [.0,1.]
by FUNCT_2:def 1;
hence
( f is non-increasing implies for a, b being Element of [.0,1.] st a <= b holds
f . a >= f . b )
; ( ( for a, b being Element of [.0,1.] st a <= b holds
f . a >= f . b ) implies f is non-increasing )
assume B1:
for a, b being Element of [.0,1.] st a <= b holds
f . a >= f . b
; f is non-increasing
let e1, e2 be ExtReal; VALUED_0:def 16 ( not e1 in dom f or not e2 in dom f or not e1 <= e2 or f . e2 <= f . e1 )
assume B2:
( e1 in dom f & e2 in dom f & e1 <= e2 )
; f . e2 <= f . e1
then reconsider ee1 = e1, ee2 = e2 as Element of [.0,1.] by FUNCT_2:def 1;
ee1 <= ee2
by B2;
hence
f . e2 <= f . e1
by B1; verum