theorem Th2: :: NAT_4:2

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