theorem :: INT_3:14

for n being Nat st 1 < n holds
1. (INT.Ring n) = 1 by Lm7;