theorem Th31: :: EUCLID_7:32

for n being non zero Nat holds RN_Base n <> {}