assume REAL is countable ; :: thesis: contradiction
then card REAL c= omega by CARD_3:def 15;
hence contradiction by TOPGEN_3:30, TOPGEN_3:def 4; :: thesis: verum