defpred S_{1}[ object , object ] means ex x, q being Element of REAL st

( $1 = x & $2 = [.x,q.[ & x < q & q is rational );

deffunc H_{1}( 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_{1}(z)
from FUNCT_1:sch 4();

A3: { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } c= rng f

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

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_{1}[a,f . a] ) )
from FUNCT_1:sch 6(A8);

f is one-to-one

( $1 = x & $2 = [.x,q.[ & x < q & q is rational );

deffunc H

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

A3: { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } c= rng f

proof

card omega c= card REAL
by CARD_1:11, NUMBERS:19;
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;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

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

proof

consider f being Function such that
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_{1}[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_{1}[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_{1}[a,b] )
by A9; :: thesis: verum

end;( b in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } & S

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

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

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

f is one-to-one

proof

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