for seq being ExtREAL_sequence holds ( ( seq is increasing implies for n, m being Nat st m < n holds seq . m < seq . n ) & ( ( for n, m being Nat st m < n holds seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Nat st m < n holds seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds seq . n <= seq . m ) implies seq is non-increasing ) )