thus ( h is decreasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 > h . r2 ) by VALUED_0:def 14; :: thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1 ) implies h is decreasing )
assume A2: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 > h . r2 ; :: thesis: h is decreasing
let e1 be ext-real number ; :: according to VALUED_0:def 14 :: thesis: for b₁ being set holds
( not e1 in proj1 h or not b₁ in proj1 h or b₁ <= e1 or not h . e1 <= h . b₁ )
let e2 be ext-real number ; :: thesis: ( not e1 in proj1 h or not e2 in proj1 h or e2 <= e1 or not h . e1 <= h . e2 )
thus ( not e1 in proj1 h or not e2 in proj1 h or e2 <= e1 or not h . e1 <= h . e2 ) by A2; :: thesis: verum