assume A1: not NAT , RAT are_equipotent ; :: thesis: contradiction
defpred S₁[ Element of NAT , Subset of REAL] means $2 = RAT_with_denominator ($1 + 1);
A2: for n being Element of NAT ex X being Subset of REAL st S₁[n,X]

proof

let n be Element of NAT ; :: thesis: ex X being Subset of REAL st S₁[n,X]
for x being object st x in RAT_with_denominator (n + 1) holds
x in REAL by NUMBERS:12;
then reconsider X = RAT_with_denominator (n + 1) as Subset of REAL by TARSKI:def 3;
take X ; :: thesis: S₁[n,X]
thus S₁[n,X] ; :: thesis: verum

end;

consider F being sequence of (bool REAL) such that
A3: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A2);
for x being object st x in union (rng F) holds
x in RAT

proof

let x be object ; :: thesis: ( x in union (rng F) implies x in RAT )
assume x in union (rng F) ; :: thesis: x in RAT
then consider Y being set such that
A4: x in Y and
A5: Y in rng F by TARSKI:def 4;
dom F = NAT by FUNCT_2:def 1;
then consider n being object such that
A6: n in NAT and
A7: F . n = Y by A5, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A6;
Y = RAT_with_denominator (n + 1) by A3, A7;
hence x in RAT by A4; :: thesis: verum

end;

then A8: union (rng F) c= RAT ;
for x being object st x in RAT holds
x in union (rng F)

proof

let x be object ; :: thesis: ( x in RAT implies x in union (rng F) )
assume x in RAT ; :: thesis: x in union (rng F)
then reconsider x = x as Rational ;
A9: dom F = NAT by FUNCT_2:def 1;
denominator x <> 0 by RAT_1:def 3;
then consider m being Nat such that
A10: denominator x = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
denominator x = m + 1 by A10;
then reconsider n = (denominator x) - 1 as Element of NAT ;
x = (numerator x) / (n + 1) by RAT_1:15;
then x in RAT_with_denominator (n + 1) by Def2;
then A11: x in F . n by A3;
F . n in rng F by A9, FUNCT_1:def 3;
hence x in union (rng F) by A11, TARSKI:def 4; :: thesis: verum

end;

then RAT c= union (rng F) ;
then A12: union (rng F) = RAT by A8, XBOOLE_0:def 10;
dom F = NAT by FUNCT_2:def 1;
then A13: rng F is countable by CARD_3:93;
for Y being set st Y in rng F holds
Y is countable

proof

let Y be set ; :: thesis: ( Y in rng F implies Y is countable )
assume Y in rng F ; :: thesis: Y is countable
then consider n being object such that
A14: n in dom F and
A15: F . n = Y by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A14, FUNCT_2:def 1;
Y = RAT_with_denominator (n + 1) by A3, A15;
then INT ,Y are_equipotent by Th4;
then NAT ,Y are_equipotent by Th3, WELLORD2:15;
then A16: card NAT = card Y by CARD_1:5;
thus Y is countable by A16, CARD_3:def 14; :: thesis: verum

end;

then RAT is countable by A12, A13, CARD_4:12;
then card RAT c= omega by CARD_3:def 14;
then not omega in card RAT ;
then ( not omega c= card RAT or not omega <> card RAT ) by CARD_1:3;
then card RAT in omega by A1, CARD_1:4, CARD_1:5, CARD_1:47;
hence contradiction ; :: thesis: verum