let seq be ExtREAL_sequence; :: thesis: ( ( seq is increasing implies for n, m being Element of NAT st m < n holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds
seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds
seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) implies seq is non-increasing ) )
A1: dom seq = NAT by FUNCT_2:def 1;
X: ( ( seq is increasing implies for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m < seq . n ) & ( seq is decreasing implies for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . n < seq . m ) & ( seq is non-decreasing implies for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m <= seq . n ) & ( seq is non-increasing implies for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . n <= seq . m ) ) by VALUED_0:def 13, VALUED_0:def 14, VALUED_0:def 15, VALUED_0:def 16;
X1: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m < seq . n ) implies seq is increasing )

proof

assume Z: for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m < seq . n ; :: thesis: seq is increasing
let e1 be ext-real number ; :: according to VALUED_0:def 13 :: thesis: for b₁ being set holds
( not e1 in K1(seq) or not b₁ in K1(seq) or b₁ <= e1 or not K13(seq,b₁) <= K13(seq,e1) )
let e2 be ext-real number ; :: thesis: ( not e1 in K1(seq) or not e2 in K1(seq) or e2 <= e1 or not K13(seq,e2) <= K13(seq,e1) )
thus ( not e1 in K1(seq) or not e2 in K1(seq) or e2 <= e1 or not K13(seq,e2) <= K13(seq,e1) ) by Z; :: thesis: verum

end;

X2: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m > seq . n ) implies seq is decreasing )

proof

assume Z: for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds
seq . m > seq . n ; :: thesis: seq is decreasing
let e1 be ext-real number ; :: according to VALUED_0:def 14 :: thesis: for b₁ being set holds
( not e1 in K1(seq) or not b₁ in K1(seq) or b₁ <= e1 or not K13(seq,e1) <= K13(seq,b₁) )
let e2 be ext-real number ; :: thesis: ( not e1 in K1(seq) or not e2 in K1(seq) or e2 <= e1 or not K13(seq,e1) <= K13(seq,e2) )
thus ( not e1 in K1(seq) or not e2 in K1(seq) or e2 <= e1 or not K13(seq,e1) <= K13(seq,e2) ) by Z; :: thesis: verum

end;

X3: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m >= seq . n ) implies seq is non-increasing )

proof

assume Z: for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m >= seq . n ; :: thesis: seq is non-increasing
let e1 be ext-real number ; :: according to VALUED_0:def 16 :: thesis: for b₁ being set holds
( not e1 in K1(seq) or not b₁ in K1(seq) or not e1 <= b₁ or K13(seq,b₁) <= K13(seq,e1) )
let e2 be ext-real number ; :: thesis: ( not e1 in K1(seq) or not e2 in K1(seq) or not e1 <= e2 or K13(seq,e2) <= K13(seq,e1) )
thus ( not e1 in K1(seq) or not e2 in K1(seq) or not e1 <= e2 or K13(seq,e2) <= K13(seq,e1) ) by Z; :: thesis: verum

end;

( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing )

proof

assume Z: for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds
seq . m <= seq . n ; :: thesis: seq is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def 15 :: thesis: for b₁ being set holds
( not e1 in K1(seq) or not b₁ in K1(seq) or not e1 <= b₁ or K13(seq,e1) <= K13(seq,b₁) )
let e2 be ext-real number ; :: thesis: ( not e1 in K1(seq) or not e2 in K1(seq) or not e1 <= e2 or K13(seq,e1) <= K13(seq,e2) )
thus ( not e1 in K1(seq) or not e2 in K1(seq) or not e1 <= e2 or K13(seq,e1) <= K13(seq,e2) ) by Z; :: thesis: verum

end;

hence ( ( seq is increasing implies for n, m being Element of NAT st m < n holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds
seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds
seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) implies seq is non-increasing ) ) by A1, X, X1, X2, X3; :: thesis: verum