A1: omega +` omega = omega by CARD_3:117;
( INT c= NAT \/ [:{0 },NAT :] & card [:NAT ,{0 }:] = card NAT & card [:NAT ,{0 }:] = card [:{0 },NAT :] ) by CARD_2:11, CARD_2:13, NUMBERS:def 4;
then ( card INT c= card (NAT \/ [:{0 },NAT :]) & card (NAT \/ [:{0 },NAT :]) c= omega ) by A1, CARD_1:27, CARD_1:84, CARD_2:47;
hence card INT c= omega by 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