theorem :: XREAL_1:63

for a being Real holds 0 <= a * a