let f be ext-real-valued Function; :: thesis: ( f is decreasing implies f is non-increasing )
assume A4: f is decreasing ; :: thesis: f is non-increasing
let e1 be ExtReal; :: according to VALUED_0:def 16 :: 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
A5: ( e1 in dom f & e2 in dom f ) and
A6: e1 <= e2 ; :: thesis: f . e1 >= f . e2

per cases ( e1 = e2 or e1 < e2 ) by A6, 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 A4, A5; :: thesis: verum

end;

end;