seq_id Zeroseq is bounded ;
hence not the_set_of_BoundedRealSequences is empty by Def1; :: thesis: verum