deffunc H₁( Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,0 ]|;
consider f being Function such that
A1: dom f = REAL and
A2: for r being Real holds f . r = H₁(r) from FUNCT_1:sch 4();
REAL , y=0-line are_equipotent

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = REAL & proj2 f = y=0-line )
thus f is one-to-one :: thesis: ( proj1 f = REAL & proj2 f = y=0-line )

proof

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )
then reconsider x = x, y = y as Real by A1;
( f . x = |[x,0 ]| & f . y = |[y,0 ]| ) by A2;
hence ( not f . x = f . y or x = y ) by SPPOL_2:1; :: thesis: verum

end;

thus dom f = REAL by A1; :: thesis: proj2 f = y=0-line
thus rng f c= y=0-line :: according to XBOOLE_0:def 10 :: thesis: y=0-line c= proj2 f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in y=0-line )
assume a in rng f ; :: thesis: a in y=0-line
then consider b being set such that
A3: ( b in dom f & a = f . b ) by FUNCT_1:def 5;
reconsider b = b as Real by A1, A3;
a = |[b,0 ]| by A2, A3;
hence a in y=0-line ; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in y=0-line or a in proj2 f )
assume A4: a in y=0-line ; :: thesis: a in proj2 f
then reconsider a = a as Point of (TOP-REAL 2) ;
A5: a = |[(a `1 ),(a `2 )]| by EUCLID:57;
then a `2 = 0 by A4, Th19;
then a = f . (a `1 ) by A2, A5;
hence a in proj2 f by A1, FUNCT_1:def 5; :: thesis: verum

end;

hence card y=0-line = continuum by CARD_1:21, TOPGEN_3:def 4; :: thesis: verum