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