thus
( IT is non-decreasing implies for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) ) by NAT_1:11, VALUED_0:def 15; :: thesis: ( ( for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) ) implies IT is non-decreasing )

assume for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) ; :: thesis: IT is non-decreasing

then for e1, e2 being ExtReal st e1 in dom IT & e2 in dom IT & e1 <= e2 holds

IT . e1 <= IT . e2 by LM;

hence IT is non-decreasing by VALUED_0:def 15; :: thesis: verum

IT . n <= IT . (n + 1) ) by NAT_1:11, VALUED_0:def 15; :: thesis: ( ( for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) ) implies IT is non-decreasing )

assume for n being Nat st n in dom IT & n + 1 in dom IT holds

IT . n <= IT . (n + 1) ; :: thesis: IT is non-decreasing

then for e1, e2 being ExtReal st e1 in dom IT & e2 in dom IT & e1 <= e2 holds

IT . e1 <= IT . e2 by LM;

hence IT is non-decreasing by VALUED_0:def 15; :: thesis: verum