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