let U be Universe; :: thesis: ( not U is countable iff omega in U )
thus ( not U is countable implies omega in U ) :: thesis: ( omega in U implies not U is countable )

proof

assume card U c/= omega ; :: according to CARD_3:def 14 :: thesis: omega in U
then omega in card U by EXCH1;
then omega in On U by CLASSES2:9;
hence omega in U by ORDINAL1:def 9; :: thesis: verum

end;

assume omega in U ; :: thesis: not U is countable
then card omega in card U by CLASSES2:1;
hence card U c/= omega ; :: according to CARD_3:def 14 :: thesis: verum