let x be Real; :: thesis: ( 0 < x & x < 1 implies 1 / (sqrt (1 - (x ^2))) > 1 )
assume that
A1: 0 < x and
A2: x < 1 ; :: thesis: 1 / (sqrt (1 - (x ^2))) > 1
A3: 0 < 1 - (x ^2) by A1, A2, Lm5;
then A4: 0 < sqrt (1 - (x ^2)) by SQUARE_1:25;
x * x > 0 * x by A1;
then (x ^2) * (- 1) < 0 * (- 1) ;
then (- (x ^2)) + 1 < 0 + 1 by XREAL_1:8;
then sqrt (1 - (x ^2)) < 1 by A3, SQUARE_1:18, SQUARE_1:27;
hence 1 / (sqrt (1 - (x ^2))) > 1 by A4, XREAL_1:187; :: thesis: verum