( 0 in omega & 1 in omega ) ;
hence not omega is trivial by ZFMISC_1:def 10; :: thesis: verum