let f be UnOp of [.0,1.]; :: thesis: ( 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 ) ; :: thesis: ( ( 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 ; :: thesis: f is non-increasing
let e1, e2 be ExtReal; :: according to VALUED_0:def 16 :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum