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
defpred S₁[ set , set ] means $2 in $1;

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 & ].x,y.[ c= a ) by A2;
consider q being rational number such that
A5: ( x < q & q < y ) by A4, RAT_1:22;
q in ].x,y.[ by A5, XXREAL_1:4;
then ( q in a & q in RAT ) by A4, RAT_1:def 2;
hence ex q being set st
( q in RAT & S₁[a,q] ) ; :: thesis: verum

end;

consider f being Function such that
A6: ( dom f = A & rng f c= RAT ) and
A7: for a being set st a in A holds
S₁[a,f . a] from WELLORD2:sch 1(A3);
f is one-to-one

proof

let a be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not a in dom f or not b₁ in dom f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume ( a in dom f & b in dom f & f . a = f . b & a <> b ) ; :: thesis: contradiction
then ( f . a in a & f . a in b & a misses b ) by A1, A6, A7;
hence contradiction by XBOOLE_0:3; :: thesis: verum

end;

then card A c= card RAT by A6, CARD_1:26;
hence A is countable by Th17, CARD_3:def 15; :: thesis: verum