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 )

( 0 < x & x ^2 < a ) )

assume A1: 0 < a ; :: thesis: ex x being Real st

( 0 < x & x ^2 < a )