let a be Real; :: thesis: ( 0 < a implies ex x being Real st
( 0 < x & x ^2 < a ) )
assume A1: 0 < a ; :: thesis: ex x being Real st
( 0 < x & x ^2 < a )

per cases ( 1 <= a or a < 1 ) ;

suppose A2: 1 <= a ; :: thesis: ex x being Real st
( 0 < x & x ^2 < a )

reconsider x = 2 " as Real ;
take x ; :: thesis: ( 0 < x & x ^2 < a )
thus 0 < x ; :: thesis: x ^2 < a
thus x ^2 < a by A2, XXREAL_0:2; :: thesis: verum

end;

suppose A3: a < 1 ; :: thesis: ex x being Real st
( 0 < x & x ^2 < a )

take x = a; :: thesis: ( 0 < x & x ^2 < a )
thus 0 < x by A1; :: thesis: x ^2 < a
thus x ^2 < a by A1, A3, Th13; :: thesis: verum

end;

end;