let n be Nat; :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r ) )

assume A1: 0 < r ; :: thesis: ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )

per cases ( 0 = n or 0 <> n ) ;
suppose A2: 0 = n ; :: thesis: ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )

set s = r / 2;
take r / 2 ; :: thesis: ( 0 < r / 2 & r / 2 < r & sqrt (((r / 2) * (r / 2)) * n) < r )
thus ( 0 < r / 2 & r / 2 < r & sqrt (((r / 2) * (r / 2)) * n) < r ) by ; :: thesis: verum
end;
suppose A3: 0 <> n ; :: thesis: ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )

set s = r / (n + 1);
take r / (n + 1) ; :: thesis: ( 0 < r / (n + 1) & r / (n + 1) < r & sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r )
set s = r / (n + 1);
A4: n + 0 < n + 1 by XREAL_1:8;
thus 0 < r / (n + 1) by A1; :: thesis: ( r / (n + 1) < r & sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r )
0 + 1 <= n by ;
then 1 * n <= n * n by XREAL_1:66;
then A6: ((r / (n + 1)) * (r / (n + 1))) * n <= ((r / (n + 1)) * (r / (n + 1))) * (n * n) by XREAL_1:66;
( 0 < 1 & 0 + 1 < n + 1 ) by ;
then 1 / (n + 1) < 1 by XREAL_1:191;
then (1 / (n + 1)) * r < r * 1 by ;
hence r / (n + 1) < r ; :: thesis: sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r
sqrt (((r / (n + 1)) * (r / (n + 1))) * n) <= sqrt (((r / (n + 1)) * n) ^2) by ;
then A8: sqrt (((r / (n + 1)) * (r / (n + 1))) * n) <= (r / (n + 1)) * n by ;
n / (n + 1) < 1 by ;
then (n / (n + 1)) * r < r * 1 by ;
hence sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r by ; :: thesis: verum
end;
end;