defpred S₁[ object , object ] means ex x, q being Element of REAL st
( $1 = x & $2 = [.x,q.[ & x < q & q is rational );
deffunc H₁( Element of [:REAL,RAT:]) -> Element of bool REAL = [.($1 `1),($1 `2).[;
set X = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ;
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 Real : ( x < q & q is rational ) } c= rng f

proof

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

end;

card omega c= card REAL by CARD_1:11, NUMBERS:19;
then A7: omega c= continuum ;
card [:REAL,RAT:] = card [:(card REAL),(card RAT):] by CARD_2:7
.= continuum *` omega by Th17, CARD_2:def 2
.= continuum by A7, CARD_4:16 ;
hence card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } c= continuum by A1, A3, CARD_1:12; :: according to XBOOLE_0:def 10 :: thesis: continuum c= card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) }
A8: for a being object st a in REAL holds
ex b being object st
( b in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } & S₁[a,b] )

proof

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

end;

consider f being Function such that
A10: ( dom f = REAL & rng f c= { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } & ( for a being object st a in REAL holds
S₁[a,f . a] ) ) from FUNCT_1:sch 6(A8);
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 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
A11: a = x and
A12: f . a = [.x,q.[ and
A13: x < q and
q is rational by A10;
assume b in dom f ; :: thesis: ( not f . a = f . b or a = b )
then consider y, r being Element of REAL such that
A14: b = y and
A15: f . b = [.y,r.[ and
A16: y < r and
r is rational by A10;
assume A17: f . a = f . b ; :: thesis: a = b
then y in [.x,q.[ by A12, A15, A16, XXREAL_1:3;
then A18: x <= y by XXREAL_1:3;
x in [.y,r.[ by A17, A12, A13, A15, XXREAL_1:3;
then y <= x by XXREAL_1:3;
hence a = b by A18, A11, A14, XXREAL_0:1; :: thesis: verum

end;

hence continuum c= card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } by A10, CARD_1:10; :: thesis: verum