take
f
=
<*>
REAL
;
:: thesis:
f
is
non-decreasing
let
n
be
Nat
;
:: according to
INTEGRA2:def 1
:: thesis:
(
n
in
dom
f
&
n
+
1
in
dom
f
implies
f
.
n
<=
f
.
(
n
+
1
)
)
assume
that
A1
:
n
in
dom
f
and
n
+
1
in
dom
f
;
:: thesis:
f
.
n
<=
f
.
(
n
+
1
)
thus
f
.
n
<=
f
.
(
n
+
1
)
by
A1
;
:: thesis:
verum