let n be non zero Nat; :: thesis: RN_Base n <> {}
0 + 1 <= n by NAT_1:13;
then Base_FinSeq (n,1) in { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } ;
hence RN_Base n <> {} ; :: thesis: verum