for n being Nat st n > 1 holds
( not INT.Ring n is degenerated & INT.Ring n is commutative Ring )