theorem Th25: :: NUMBER19:25

for n, k being Nat st 0 < n & n < k holds
n ! < k !