defpred S₁[ set , set ] means ex i being integer number ex n being natural number st
( $1 = [i,n] & $2 = i / n );
A1: for a being set st a in [:INT ,NAT :] holds
ex b being set st S₁[a,b]

proof

let a be set ; :: thesis: ( a in [:INT ,NAT :] implies ex b being set st S₁[a,b] )
assume a in [:INT ,NAT :] ; :: thesis: ex b being set st S₁[a,b]
then consider x, y being set such that
A2: x in INT and
A3: y in NAT and
A4: a = [x,y] by ZFMISC_1:def 2;
reconsider y = y as natural number by A3;
reconsider x = x as integer number by A2;
x / y = x / y ;
hence ex b being set st S₁[a,b] by A4; :: thesis: verum

end;

consider f being Function such that
A5: ( dom f = [:INT ,NAT :] & ( for a being set st a in [:INT ,NAT :] holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A1);
A6: RAT c= rng f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in RAT or a in rng f )
assume a in RAT ; :: thesis: a in rng f
then consider i, j being Integer such that
A7: a = i / j by RAT_1:def 1;
consider n being Element of NAT such that
A8: ( j = n or j = - n ) by INT_1:8;
i / (- n) = - (i / n) by XCMPLX_1:189;
then ( a = i / n or a = (- i) / n ) by A7, A8, XCMPLX_1:188;
then consider k being Integer such that
A9: a = k / n ;
k in INT by INT_1:def 2;
then A10: [k,n] in [:INT ,NAT :] by ZFMISC_1:def 2;
then consider i1 being integer number , n1 being natural number such that
A11: [k,n] = [i1,n1] and
A12: f . [k,n] = i1 / n1 by A5;
A13: n = n1 by A11, ZFMISC_1:33;
i1 = k by A11, ZFMISC_1:33;
hence a in rng f by A13, A5, A9, A10, A12, FUNCT_1:def 5; :: thesis: verum

end;

card [:INT ,NAT :] = card [:omega ,omega :] by Th16, CARD_2:14
.= omega by CARD_2:def 2, CARD_4:54 ;
hence card RAT c= omega by A5, A6, CARD_1:28; :: according to XBOOLE_0:def 10 :: thesis: omega c= card RAT
thus omega c= card RAT by CARD_1:27, CARD_1:84, NUMBERS:18; :: thesis: verum