0 < 1 ;
hence not NATPLUS is empty by Def9; :: thesis: verum