defpred S₁[ set , set ] means $2 in $1;
let A be set ; :: thesis: ( A is mutually-disjoint & ( for a being set st a in A holds
ex x, y being real number 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 number 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 number st
( x < y & ].x,y.[ c= a ) ; :: thesis: A is countable

A3: now

let a be set ; :: thesis: ( a in A implies ex q being set st
( q in RAT & S₁[a,q] ) )
assume a in A ; :: thesis: ex q being set st
( q in RAT & S₁[a,q] )
then consider x, y being real number such that
A4: x < y and
A5: ].x,y.[ c= a by A2;
consider q being rational number 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 set 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 set st a in A holds
S₁[a,f . a] from FUNCT_1:sch 5(A3);
f is one-to-one

proof

let a be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not a in proj1 f or not b₁ in proj1 f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in proj1 f or not b in proj1 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
A15: f . a in b by A12, A13, A9, A10;
A16: f . a in a by A11, A9, A10;
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, CARD_3:def 14; :: thesis: verum