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