theorem Lm1: :: DIOPHAN1:27

for t being 1 _greater Nat holds
( t > 0 & t > 1 & t " > 0 & t * (t ") = 1 )