theorem :: PRIMRECI:3

for x, y being Real st x ^2 < y holds
x < sqrt y