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