theorem THTU: :: NTALGO_2:18
1 < tau