for n being Nat st n >= 2 holds
n ! > 1 by Lm50;