let U be Universe; :: thesis: ( U is uncountable iff omega in U )
thus ( U is uncountable implies omega in U ) :: thesis: ( omega in U implies U is uncountable )
proof
assume card U c/= omega ; :: according to CARD_3:def 14 :: thesis: omega in U
then omega in card U by Th4;
then omega in On U by CLASSES2:9;
hence omega in U by ORDINAL1:def 9; :: thesis: verum
end;
assume omega in U ; :: thesis: U is uncountable
then card omega in card U by CLASSES2:1;
hence card U c/= omega ; :: according to CARD_3:def 14 :: thesis: verum