theorem Th1: :: NAT_4:1

for r, s being Real st 0 <= r & s * s < r * r holds
s < r