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 set st x in RAT_with_denominator (n + 1) holds
x in REAL by NUMBERS:12, TARSKI:def 3;
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 Function of NAT,(bool REAL) such that
A4: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A2);
for x being set st x in union (rng F) holds
x in RAT

proof

let x be set ; :: 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
A7: x in Y and
A8: Y in rng F by TARSKI:def 4;
dom F = NAT by FUNCT_2:def 1;
then consider n being set such that
A10: n in NAT and
A11: F . n = Y by A8, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A10;
Y = RAT_with_denominator (n + 1) by A4, A11;
hence x in RAT by A7; :: thesis: verum

end;

then A13: union (rng F) c= RAT by TARSKI:def 3;
for x being set st x in RAT holds
x in union (rng F)

proof

let x be set ; :: 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 ;
A16: dom F = NAT by FUNCT_2:def 1;
denominator x <> 0 by RAT_1:def 3;
then consider m being Nat such that
A18: denominator x = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
denominator x = m + 1 by A18;
then reconsider n = (denominator x) - 1 as Element of NAT ;
x = (numerator x) / (n + 1) by RAT_1:37;
then x in RAT_with_denominator (n + 1) by Def2;
then A22: x in F . n by A4;
F . n in rng F by A16, FUNCT_1:def 5;
hence x in union (rng F) by A22, TARSKI:def 4; :: thesis: verum

end;

then RAT c= union (rng F) by TARSKI:def 3;
then A25: union (rng F) = RAT by A13, XBOOLE_0:def 10;
dom F = NAT by FUNCT_2:def 1;
then A27: rng F is countable by CARD_3:127;
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 set such that
A30: n in dom F and
A31: F . n = Y by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A30, FUNCT_2:def 1;
Y = RAT_with_denominator (n + 1) by A4, A31;
then INT ,Y are_equipotent by Th4;
then NAT ,Y are_equipotent by Th3, WELLORD2:22;
then A35: card NAT = card Y by CARD_1:21;
card NAT c= omega by CARD_3:def 15, CARD_4:44;
hence Y is countable by A35, CARD_3:def 15; :: thesis: verum

end;

then RAT is countable by A25, A27, CARD_4:62;
then card RAT c= omega by CARD_3:def 15;
then not omega in card RAT ;
then ( not omega c= card RAT or not omega <> card RAT ) by CARD_1:13;
then card RAT in omega by A1, CARD_1:14, CARD_1:21, CARD_1:84;
hence contradiction ; :: thesis: verum