thus ( h is non-decreasing implies for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 ) ; :: thesis: ( ( for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 ) implies h is non-decreasing )
assume A1: for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 ; :: thesis: h is non-decreasing
let e1 be ExtReal; :: according to VALUED_0:def 15 :: thesis: for b₁ being object holds
( not e1 in dom h or not b₁ in dom h or not e1 <= b₁ or h . e1 <= h . b₁ )
let e2 be ExtReal; :: thesis: ( not e1 in dom h or not e2 in dom h or not e1 <= e2 or h . e1 <= h . e2 )
assume A2: ( e1 in dom h & e2 in dom h ) ; :: thesis: ( not e1 <= e2 or h . e1 <= h . e2 )
assume e1 <= e2 ; :: thesis: h . e1 <= h . e2
then ( e1 < e2 or e1 = e2 ) by XXREAL_0:1;
hence h . e1 <= h . e2 by A1, A2; :: thesis: verum