let A be Subset of S,N; :: thesis: not A is empty
ex i being Element of N st A = rng the mapping of (N | i) by Def2;
hence not A is empty ; :: thesis: verum