not [0 ,0 ] in RAT+ by ARYTM_3:39;
then A1: RAT = RAT+ \/ ([:{0 },RAT+ :] \ {[0 ,0 ]}) by NUMBERS:def 3, XBOOLE_1:87, ZFMISC_1:56;
then bool RAT+ c= bool RAT by XBOOLE_1:7, ZFMISC_1:79;
then A2: DEDEKIND_CUTS c= bool RAT by XBOOLE_1:1;
RAT+ c= RAT by A1, XBOOLE_1:7;
then RAT+ \/ DEDEKIND_CUTS c= RAT \/ (bool RAT ) by A2, XBOOLE_1:13;
then REAL+ c= RAT \/ (bool RAT ) by ARYTM_2:def 2, XBOOLE_1:1;
then A3: card REAL+ c= card (RAT \/ (bool RAT )) by CARD_1:27;
set INFNAT = (bool NAT ) \ (Fin NAT );
A4: card RAT in card (bool RAT ) by CARD_1:30;
card (RAT \/ (bool RAT )) c= (card RAT ) +` (card (bool RAT )) by CARD_2:47;
then card REAL+ c= (card RAT ) +` (card (bool RAT )) by A3, XBOOLE_1:1;
then card REAL+ c= card (bool RAT ) by A4, CARD_3:118;
then card REAL+ c= exp 2,omega by Th17, CARD_2:44;
then (card REAL+ ) +` (card REAL+ ) c= (exp 2,omega ) +` (exp 2,omega ) by CARD_3:125;
then A5: (card REAL+ ) +` (card REAL+ ) c= exp 2,omega by CARD_3:118;
deffunc H<sub>1</sub>( set ) -> Element of REAL = Sum ($1 -powers (1 / 2));
A6: card [:{0 },REAL+ :] = card [:REAL+ ,{0 }:] by CARD_2:11
.= card REAL+ by CARD_2:13 ;
A7: continuum c= card (REAL+ \/ [:{0 },REAL+ :]) by CARD_1:27, NUMBERS:def 1;
card (REAL+ \/ [:{0 },REAL+ :]) c= (card REAL+ ) +` (card [:{0 },REAL+ :]) by CARD_2:47;
then continuum c= (card REAL+ ) +` (card REAL+ ) by A7, A6, XBOOLE_1:1;
hence continuum c= exp 2,omega by A5, XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: exp 2,omega c= continuum
Fin NAT is countable by Th28, CARD_4:44;
then A8: card (Fin NAT ) c= omega by CARD_3:def 15;
then card (Fin NAT ) in card (bool NAT ) by CARD_1:30, CARD_1:84, ORDINAL1:22;
then A9: (card (bool NAT )) +` (card (Fin NAT )) = card (bool NAT ) by CARD_3:118;
A10: omega in card (bool NAT ) by CARD_1:30, CARD_1:84;
then reconsider INFNAT = (bool NAT ) \ (Fin NAT ) as non empty set by A8, CARD_2:4, ORDINAL1:22;
consider f being Function of INFNAT,REAL such that
A11: for X being Element of INFNAT holds f . X = H₁(X) from FUNCT_2:sch 4();
A12: 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 proj1 f or not b₁ in proj1 f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A13: a in dom f and
A14: b in dom f ; :: thesis: ( not f . a = f . b or a = b )
A15: f . b = H₁(b) by A11, A14;
not b in Fin NAT by A14, XBOOLE_0:def 5;
then A16: b is infinite Subset of NAT by A14, XBOOLE_0:def 5, FINSUB_1:def 5;
not a in Fin NAT by A13, XBOOLE_0:def 5;
then A17: a is infinite Subset of NAT by A13, XBOOLE_0:def 5, FINSUB_1:def 5;
f . a = H₁(a) by A11, A13;
hence ( not f . a = f . b or a = b ) by A17, A16, A15, Th27; :: thesis: verum

end;

A18: rng f c= REAL by RELAT_1:def 19;
dom f = INFNAT by FUNCT_2:def 1;
then card INFNAT c= continuum by A12, A18, CARD_1:26;
then card (bool NAT ) c= continuum by A9, A8, A10, CARD_3:144, ORDINAL1:22;
hence exp 2,omega c= continuum by CARD_1:84, CARD_2:44; :: thesis: verum