let x be real number ; :: thesis: ( 0 < x & x < 1 implies 0 < 1 - (x ^2 ) )
assume A1: ( 0 < x & x < 1 ) ; :: thesis: 0 < 1 - (x ^2 )
then x ^2 < x by SQUARE_1:75;
then x ^2 < 1 by A1, XXREAL_0:2;
then (x ^2 ) - (x ^2 ) < 1 - (x ^2 ) by XREAL_1:11;
hence 0 < 1 - (x ^2 ) ; :: thesis: verum