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