ind A >= - 1 by Th5;
then ( ind A > - 1 or ind A = - 1 ) by XXREAL_0:1;
then ind A >= (- 1) + 1 by Th6, INT_1:7;
then ind A in NAT by INT_1:3;
hence ind A is natural ; :: thesis: verum