set U = Tarski-Class (a \/ omega);
( omega c= a \/ omega & a \/ omega in Tarski-Class (a \/ omega) ) by CLASSES1:2, XBOOLE_1:7;
then omega in Tarski-Class (a \/ omega) by CLASSES1:def 1;
hence not Tarski-Class (a \/ omega) is countable by Th57; :: thesis: verum