defpred S₁[ object , object ] means ex D1 being set st
( D1 = $1 & $2 in D1 );
let A be set ; :: thesis: ( A is mutually-disjoint & ( for a being set st a in A holds
ex x, y being Real st
( x < y & ].x,y.[ c= a ) ) implies A is countable )
assume A1: for a, b being set st a in A & b in A & a <> b holds
a misses b ; :: according to TAXONOM2:def 5 :: thesis: ( ex a being set st
( a in A & ( for x, y being Real holds
( not x < y or not ].x,y.[ c= a ) ) ) or A is countable )
assume A2: for a being set st a in A holds
ex x, y being Real st
( x < y & ].x,y.[ c= a ) ; :: thesis: A is countable

A3: now :: thesis: for a being object st a in A holds
ex q being object st
( q in RAT & S₁[a,q] )

let a be object ; :: thesis: ( a in A implies ex q being object st
( q in RAT & S₁[a,q] ) )
reconsider aa = a as set by TARSKI:1;
assume a in A ; :: thesis: ex q being object st
( q in RAT & S₁[a,q] )
then consider x, y being Real such that
A4: x < y and
A5: ].x,y.[ c= aa by A2;
consider q being Rational such that
A6: x < q and
A7: q < y by A4, RAT_1:7;
A8: q in RAT by RAT_1:def 2;
q in ].x,y.[ by A6, A7, XXREAL_1:4;
hence ex q being object st
( q in RAT & S₁[a,q] ) by A5, A8; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = A & rng f c= RAT ) and
A10: for a being object st a in A holds
S₁[a,f . a] from FUNCT_1:sch 6(A3);
f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A11: a in dom f and
A12: b in dom f and
A13: f . a = f . b and
A14: a <> b ; :: thesis: contradiction
reconsider a = a, b = b as set by TARSKI:1;
S₁[b,f . b] by A12, A9, A10;
then A15: f . a in b by A13;
S₁[a,f . a] by A11, A9, A10;
then A16: f . a in a ;
a misses b by A11, A12, A14, A1, A9;
hence contradiction by A16, A15, XBOOLE_0:3; :: thesis: verum

end;

then card A c= card RAT by A9, CARD_1:10;
hence A is countable by Th17; :: thesis: verum