let UN be Universe; :: thesis: ( not UN is denumerable iff omega in UN )

hereby :: thesis: ( omega in UN implies not UN is denumerable )

assume not UN is denumerable ; :: thesis: omega in UN
then UN is uncountable ;
hence omega in UN by ORDINAL6:57; :: thesis: verum

end;

assume omega in UN ; :: thesis: not UN is denumerable
hence not UN is denumerable by ORDINAL6:57; :: thesis: verum