let x be Real; :: thesis: ( 0 < x & x <= 1 implies 1 - (x ^2) >= 0 )
assume that
A1: 0 < x and
A2: x <= 1 ; :: thesis: 1 - (x ^2) >= 0
A3: x - 1 <= 1 - 1 by A2, XREAL_1:9;

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

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

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

end;

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

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

end;

end;