theorem Th23: :: NEWTON02:121

for b being Nat holds
( b > 1 iff b ! > 1 )