theorem :: SQUARE_1:12

for a being Real st 0 <> a holds
0 < a ^2 by XREAL_1:63;