theorem Th18: :: BASEL_1:18

for r being Real st 0 <= r & r < PI / 2 holds
r <= tan . r