let f be ext-real-valued Function; :: thesis: ( f is increasing implies f is non-decreasing )
assume Z: f is increasing ; :: thesis: f is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def 15 :: thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2
let e2 be ext-real number ; :: thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 <= f . e2 )
assume that
Z1: e1 in dom f and
Z2: e2 in dom f and
Z3: e1 <= e2 ; :: thesis: f . e1 <= f . e2

per cases ( e1 = e2 or e1 < e2 ) by Z3, XXREAL_0:1;

suppose e1 = e2 ; :: thesis: f . e1 <= f . e2

hence f . e1 <= f . e2 ; :: thesis: verum

end;

suppose e1 < e2 ; :: thesis: f . e1 <= f . e2

hence f . e1 <= f . e2 by Z1, Z2, Def13, Z; :: thesis: verum

end;

end;