let f be UnOp of [.0,1.]; :: thesis: ( f is 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 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 increasing )
assume B1: for a, b being Element of [.0,1.] st a < b holds
f . a < f . b ; :: thesis: f is increasing
let e1, e2 be ExtReal; :: according to VALUED_0:def 13 :: thesis: ( not e1 in dom f or not e2 in dom f or e2 <= e1 or not f . e2 <= f . e1 )
assume B2: ( e1 in dom f & e2 in dom f & e1 < e2 ) ; :: thesis: not 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 not f . e2 <= f . e1 by B1; :: thesis: verum