theorem Th4: :: FIELD_3:3

for n being Nat st 1 < n holds
0. (Z/ n) = 0