let
n
be
Nat
;
:: thesis:
(
n
<=
1 implies
ind
(
TOP-REAL
n
)
=
n
)
assume
n
<=
1 ;
:: thesis:
ind
(
TOP-REAL
n
)
=
n
then
(
n
<
1 or
n
=
1 )
by
XXREAL_0:1
;
then
(
n
=
0
or
n
=
1 )
by
NAT_1:14
;
hence
ind
(
TOP-REAL
n
)
=
n
by
Lm7
,
Lm8
;
:: thesis:
verum