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 & y in NAT & a = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x as integer number by A2;
reconsider y = y as natural number by A2;
x / y = x / y ;
hence ex b being set st S₁[a,b] by A2; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = [:INT ,NAT :] & ( for a being set st a in [:INT ,NAT :] holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A1);
A4: 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
A5: a = i / j by RAT_1:def 1;
consider n being Element of NAT such that
A6: ( 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 A5, A6, XCMPLX_1:188;
then consider k being Integer such that
A7: a = k / n ;
( k in INT & n in NAT ) by INT_1:def 2;
then A8: [k,n] in [:INT ,NAT :] by ZFMISC_1:def 2;
then consider i1 being integer number , n1 being natural number such that
A9: ( [k,n] = [i1,n1] & f . [k,n] = i1 / n1 ) by A3;
( i1 = k & n = n1 ) by A9, ZFMISC_1:33;
hence a in rng f by A3, A7, A8, A9, 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 A3, A4, 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