let f be ext-real-valued Function; :: thesis: ( f is increasing implies f is non-decreasing )
assume A1: f is increasing ; :: thesis: f is non-decreasing
let e1 be ExtReal; :: according to VALUED_0:def 15 :: thesis: for e2 being ExtReal st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2
let e2 be ExtReal; :: thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 <= f . e2 )
assume that
A2: ( e1 in dom f & e2 in dom f ) and
A3: e1 <= e2 ; :: thesis: f . e1 <= f . e2
per cases ( e1 = e2 or e1 < e2 ) by A3, 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 A1, A2; :: thesis: verum
end;
end;