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