consider N being Num of D;
set S = Ser D,N;
reconsider SER = rng (Ser D,N) as non empty Subset of ExtREAL ;
take SER ; :: thesis: ex N being Num of D st SER = rng (Ser D,N)
thus ex N being Num of D st SER = rng (Ser D,N) ; :: thesis: verum