theorem Th1: :: REAL_3:1

for r being Real st 0 < r & r < 1 holds
1 < 1 / r