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]
A3: for x being set st x in RAT_with_denominator (n + 1) holds
x in REAL by NUMBERS:12, TARSKI:def 3;
reconsider X = RAT_with_denominator (n + 1) as Subset of REAL by A3, 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);
A5: 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 A6: x in union (rng F) ; :: thesis: x in RAT
consider Y being set such that
A7: x in Y and
A8: Y in rng F by A6, TARSKI:def 4;
A9: dom F = NAT by FUNCT_2:def 1;
consider n being set such that
A10: n in NAT and
A11: F . n = Y by A8, A9, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A10;
A12: Y = RAT_with_denominator (n + 1) by A4, A11;
thus x in RAT by A7, A12; :: thesis: verum

end;

A13: union (rng F) c= RAT by A5, TARSKI:def 3;
A14: 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 A15: x in RAT ; :: thesis: x in union (rng F)
reconsider x = x as Rational by A15;
A16: dom F = NAT by FUNCT_2:def 1;
A17: denominator x <> 0 by RAT_1:def 3;
consider m being Nat such that
A18: denominator x = m + 1 by A17, NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A19: denominator x = m + 1 by A18;
reconsider n = (denominator x) - 1 as Element of NAT by A19;
A20: x = (numerator x) / (n + 1) by RAT_1:37;
A21: x in RAT_with_denominator (n + 1) by A20, Def2;
A22: x in F . n by A4, A21;
A23: F . n in rng F by A16, FUNCT_1:def 5;
thus x in union (rng F) by A22, A23, TARSKI:def 4; :: thesis: verum

end;

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

end;

A37: RAT is countable by A25, A27, A28, CARD_4:62;
A38: card RAT c= omega by A37, CARD_3:def 15;
A39: not omega in card RAT by A38;
A40: ( not omega c= card RAT or not omega <> card RAT ) by A39, CARD_1:13;
A41: card RAT in omega by A1, A40, CARD_1:14, CARD_1:21, CARD_1:84;
thus contradiction by A41; :: thesis: verum