defpred S_{1}[ 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

A9: ( dom f = A & rng f c= RAT ) and

A10: for a being object st a in A holds

S_{1}[a,f . a]
from FUNCT_1:sch 6(A3);

f is one-to-one

hence A is countable by Th17; :: thesis: verum

( 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_{1}[a,q] )

consider f being Function such that ex q being object st

( q in RAT & S

let a be object ; :: thesis: ( a in A implies ex q being object st

( q in RAT & S_{1}[a,q] ) )

reconsider aa = a as set by TARSKI:1;

assume a in A ; :: thesis: ex q being object st

( q in RAT & S_{1}[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_{1}[a,q] )
by A5, A8; :: thesis: verum

end;( q in RAT & S

reconsider aa = a as set by TARSKI:1;

assume a in A ; :: thesis: ex q being object st

( q in RAT & S

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

A9: ( dom f = A & rng f c= RAT ) and

A10: for a being object st a in A holds

S

f is one-to-one

proof

then
card A c= card RAT
by A9, CARD_1:10;
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_{1}[b,f . b]
by A12, A9, A10;

then A15: f . a in b by A13;

S_{1}[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;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

then A15: f . a in b by A13;

S

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

hence A is countable by Th17; :: thesis: verum