set X = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ;
deffunc H₁( Element of [:REAL ,RAT :]) -> Element of bool REAL = [.($1 `1 ),($1 `2 ).[;
consider f being Function such that
A1: dom f = [:REAL ,RAT :] and
A2: for z being Element of [:REAL ,RAT :] holds f . z = H₁(z) from FUNCT_1:sch 4();
A3: { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } c= rng f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } or a in rng f )
assume a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ; :: thesis: a in rng f
then consider x, q being Element of REAL such that
A4: ( a = [.x,q.[ & x < q & q is rational ) ;
q in RAT by A4, RAT_1:def 2;
then reconsider b = [x,q] as Element of [:REAL ,RAT :] by ZFMISC_1:def 2;
( b `1 = x & b `2 = q ) by MCART_1:7;
then f . b = [.x,q.[ by A2;
hence a in rng f by A1, A4, FUNCT_1:def 5; :: thesis: verum

end;

0 in omega ;
then B5: omega c= continuum by CARD_1:27, CARD_1:84;
card [:REAL ,RAT :] = card [:(card REAL ),(card RAT ):] by CARD_2:14
.= continuum *` omega by Th17, CARD_2:def 2
.= continuum by B5, CARD_4:78 ;
hence card { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } c= continuum by A1, A3, CARD_1:28; :: according to XBOOLE_0:def 10 :: thesis: continuum c= card { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) }
defpred S₁[ set , set ] means ex x, q being Element of REAL st
( $1 = x & $2 = [.x,q.[ & x < q & q is rational );
A6: for a being set st a in REAL holds
ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S₁[a,b] )

proof

let a be set ; :: thesis: ( a in REAL implies ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S₁[a,b] ) )
assume a in REAL ; :: thesis: ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S₁[a,b] )
then reconsider x = a as Element of REAL ;
x + 0 < x + 1 by XREAL_1:8;
then consider q being rational number such that
A7: ( x < q & q < x + 1 ) by RAT_1:22;
( q in RAT & RAT c= REAL ) by NUMBERS:12, RAT_1:def 2;
then reconsider q = q as Element of REAL ;
[.x,q.[ in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } by A7;
hence ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S₁[a,b] ) by A7; :: thesis: verum

end;

consider f being Function such that
A8: ( dom f = REAL & rng f c= { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & ( for a being set st a in REAL holds
S₁[a,f . a] ) ) from WELLORD2:sch 1(A6);
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 ; :: thesis: ( not b in dom f or not f . a = f . b or a = b )
then consider x, q being Element of REAL such that
A9: ( a = x & f . a = [.x,q.[ & x < q & q is rational ) by A8;
assume b in dom f ; :: thesis: ( not f . a = f . b or a = b )
then consider y, r being Element of REAL such that
A10: ( b = y & f . b = [.y,r.[ & y < r & r is rational ) by A8;
assume f . a = f . b ; :: thesis: a = b
then ( x in [.y,r.[ & y in [.x,q.[ ) by A9, A10, XXREAL_1:3;
then ( x <= y & y <= x ) by XXREAL_1:3;
hence a = b by A9, A10, XXREAL_0:1; :: thesis: verum

end;

hence continuum c= card { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } by A8, CARD_1:26; :: thesis: verum