let x be real number ; :: thesis: ( 0 < x & x <= 1 implies 1 - (x ^2 ) >= 0 )
assume A1: ( 0 < x & x <= 1 ) ; :: thesis: 1 - (x ^2 ) >= 0
then A2: x - 1 <= 1 - 1 by XREAL_1:11;

per cases ( x - 1 < 0 or x - 1 = 0 ) by A2;

suppose x - 1 < 0 ; :: thesis: 1 - (x ^2 ) >= 0

then (x - 1) + 1 < 0 + 1 by XREAL_1:10;
hence 1 - (x ^2 ) >= 0 by A1, Lm7; :: thesis: verum

end;

suppose x - 1 = 0 ; :: thesis: 1 - (x ^2 ) >= 0

hence 1 - (x ^2 ) >= 0 ; :: thesis: verum

end;

end;