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