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

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