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: ( ( 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 A2: 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 K53(seq) or not b₁ in K53(seq) or b₁ <= e1 or not K65(seq,b₁) <= K65(seq,e1) )
let e2 be ext-real number ; :: thesis: ( not e1 in K53(seq) or not e2 in K53(seq) or e2 <= e1 or not K65(seq,e2) <= K65(seq,e1) )
thus ( not e1 in K53(seq) or not e2 in K53(seq) or e2 <= e1 or not K65(seq,e2) <= K65(seq,e1) ) by A2; :: thesis: verum

end;

A3: ( ( 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 A4: 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 K53(seq) or not b₁ in K53(seq) or b₁ <= e1 or not K65(seq,e1) <= K65(seq,b₁) )
let e2 be ext-real number ; :: thesis: ( not e1 in K53(seq) or not e2 in K53(seq) or e2 <= e1 or not K65(seq,e1) <= K65(seq,e2) )
thus ( not e1 in K53(seq) or not e2 in K53(seq) or e2 <= e1 or not K65(seq,e1) <= K65(seq,e2) ) by A4; :: thesis: verum

end;

A5: ( ( 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 A6: 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 K53(seq) or not b₁ in K53(seq) or not e1 <= b₁ or K65(seq,e1) <= K65(seq,b₁) )
let e2 be ext-real number ; :: thesis: ( not e1 in K53(seq) or not e2 in K53(seq) or not e1 <= e2 or K65(seq,e1) <= K65(seq,e2) )
thus ( not e1 in K53(seq) or not e2 in K53(seq) or not e1 <= e2 or K65(seq,e1) <= K65(seq,e2) ) by A6; :: thesis: verum

end;

A7: ( ( 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 A8: 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 K53(seq) or not b₁ in K53(seq) or not e1 <= b₁ or K65(seq,b₁) <= K65(seq,e1) )
let e2 be ext-real number ; :: thesis: ( not e1 in K53(seq) or not e2 in K53(seq) or not e1 <= e2 or K65(seq,e2) <= K65(seq,e1) )
thus ( not e1 in K53(seq) or not e2 in K53(seq) or not e1 <= e2 or K65(seq,e2) <= K65(seq,e1) ) by A8; :: thesis: verum

end;

dom seq = NAT by FUNCT_2:def 1;
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, A3, A7, A5, VALUED_0:def 13, VALUED_0:def 14, VALUED_0:def 15, VALUED_0:def 16; :: thesis: verum