A1: card INT c= card (NAT \/ [:{0},NAT:]) by NUMBERS:def 4, CARD_1:27;
A2: card [:NAT,{0}:] = card [:{0},NAT:] by CARD_2:11;
A3: card [:NAT,{0}:] = card NAT by CARD_2:13;
omega +` omega = omega by CARD_3:117;
then card (NAT \/ [:{0},NAT:]) c= omega by A3, A2, CARD_1:84, CARD_2:47;
hence card INT c= omega by A1, XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: omega c= card INT
thus omega c= card INT by CARD_1:27, CARD_1:84, NUMBERS:17; :: thesis: verum