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
A3: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A2);
A4: union (rng F) = RAT

proof

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
A5: ( x in Y & Y in rng F ) by TARSKI:def 4;
dom F = NAT by FUNCT_2:def 1;
then consider n being set such that
A6: ( n in NAT & F . n = Y ) by A5, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A6;
Y = RAT_with_denominator (n + 1) by A3, A6;
hence x in RAT by A5; :: thesis: verum

end;

then A7: 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 ;
A8: dom F = NAT by FUNCT_2:def 1;
denominator x <> 0 by RAT_1:def 3;
then consider m being Nat such that
A9: denominator x = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
denominator x = m + 1 by A9;
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 ( x in F . n & F . n in rng F ) by A3, A8, FUNCT_1:def 5;
hence x in union (rng F) by TARSKI:def 4; :: thesis: verum

end;

then RAT c= union (rng F) by TARSKI:def 3;
hence union (rng F) = RAT by A7, XBOOLE_0:def 10; :: thesis: verum

end;

dom F = NAT by FUNCT_2:def 1;
then A10: 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
A11: ( n in dom F & F . n = Y ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A11, FUNCT_2:def 1;
Y = RAT_with_denominator (n + 1) by A3, A11;
then INT ,Y are_equipotent by Th4;
then NAT ,Y are_equipotent by Th3, WELLORD2:22;
then A12: 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 A12, CARD_3:def 15; :: thesis: verum

end;

then RAT is countable by A4, A10, 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 A13: card RAT in omega by A1, CARD_1:14, CARD_1:21, CARD_1:84;
thus contradiction by A13; :: thesis: verum