let x be real number ; :: thesis: ( 0 < x & x < 1 implies 1 / (sqrt (1 - (x ^2 ))) > 1 )
assume A1: ( 0 < x & x < 1 ) ; :: thesis: 1 / (sqrt (1 - (x ^2 ))) > 1
then A2: 0 < 1 - (x ^2 ) by Lm7;
then A3: 0 < sqrt (1 - (x ^2 )) by SQUARE_1:93;
x * x > 0 * x by A1, XREAL_1:70;
then (x ^2 ) * (- 1) < 0 * (- 1) by XREAL_1:71;
then (- (x ^2 )) + 1 < 0 + 1 by XREAL_1:10;
then sqrt (1 - (x ^2 )) < 1 by A2, SQUARE_1:83, SQUARE_1:95;
hence 1 / (sqrt (1 - (x ^2 ))) > 1 by A3, XREAL_1:189; :: thesis: verum