let x be Real; :: thesis: ( 0 < x & x < 1 implies 0 < 1 - (x ^2) )
assume that
A1: 0 < x and
A2: x < 1 ; :: thesis: 0 < 1 - (x ^2)
x ^2 < x by A1, A2, SQUARE_1:13;
then x ^2 < 1 by A2, XXREAL_0:2;
then (x ^2) - (x ^2) < 1 - (x ^2) by XREAL_1:9;
hence 0 < 1 - (x ^2) ; :: thesis: verum