theorem Th25: :: SQUARE_1:25

for a being Real st 0 < a holds
0 < sqrt a