reconsider y = REAL as Point of REAL? by Th30;
assume REAL? is first-countable ; :: thesis: contradiction
then consider B being Basis of y such that
A1: B is countable by Def1;
consider h being Function of NAT ,B such that
A2: rng h = B by A1, CARD_3:146;
defpred S₁[ set , set ] means ex m being Element of NAT st
( m = $1 & $2 in (h . $1) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ );
A3: for n being set st n in NAT holds
ex x being set st
( x in REAL \ NAT & S₁[n,x] )

proof

let n be set ; :: thesis: ( n in NAT implies ex x being set st
( x in REAL \ NAT & S₁[n,x] ) )
assume A4: n in NAT ; :: thesis: ex x being set st
( x in REAL \ NAT & S₁[n,x] )
then reconsider m = n as Element of NAT ;
n in dom h by A4, FUNCT_2:def 1;
then A5: h . n in rng h by FUNCT_1:def 5;
then reconsider Bn = h . n as Subset of REAL? by A2;
reconsider m9 = m as Point of RealSpace by METRIC_1:def 14;
reconsider Kn = Ball m9,(1 / 4) as Subset of R^1 by TOPMETR:16;
reconsider Bn = Bn as Subset of REAL? ;
( Bn is open & y in Bn ) by A5, YELLOW_8:21;
then consider An being Subset of R^1 such that
A6: An is open and
A7: NAT c= An and
A8: Bn = (An \ NAT ) \/ {REAL } by Th31;
reconsider An9 = An as Subset of R^1 ;
Kn is open by TOPMETR:21;
then A9: An9 /\ Kn is open by A6, TOPS_1:38;
dist m9,m9 = 0 by METRIC_1:1;
then m9 in Ball m9,(1 / 4) by METRIC_1:12;
then n in An /\ (Ball m9,(1 / 4)) by A4, A7, XBOOLE_0:def 4;
then consider r being real number such that
A10: r > 0 and
A11: Ball m9,r c= An /\ Kn by A9, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
m < m + r by A10, XREAL_1:31;
then m - r < m by XREAL_1:21;
then consider x being real number such that
A12: m - r < x and
A13: x < m by XREAL_1:7;
reconsider x = x as Real by XREAL_0:def 1;
take x ; :: thesis: ( x in REAL \ NAT & S₁[n,x] )
A14: r < 1

proof

assume r >= 1 ; :: thesis: contradiction
then 1 / 2 < r by XXREAL_0:2;
then - r < - (1 / 2) by XREAL_1:26;
then A15: (- r) + m < (- (1 / 2)) + m by XREAL_1:8;
(- (1 / 2)) + m < r + m by A10, XREAL_1:8;
then m - (1 / 2) in { a where a is Real : ( m - r < a & a < m + r ) } by A15;
then m - (1 / 2) in ].(m - r),(m + r).[ by RCOMP_1:def 2;
then m - (1 / 2) in Ball m9,r by Th7;
then m - (1 / 2) in Kn by A11, XBOOLE_0:def 4;
then m - (1 / 2) in ].(m - (1 / 4)),(m + (1 / 4)).[ by Th7;
then m - (1 / 2) in { a where a is Real : ( m - (1 / 4) < a & a < m + (1 / 4) ) } by RCOMP_1:def 2;
then ex a being Real st
( a = m - (1 / 2) & m - (1 / 4) < a & a < m + (1 / 4) ) ;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

A16: not x in NAT

proof

assume x in NAT ; :: thesis: contradiction
then reconsider x = x as Element of NAT ;

per cases ( x = m or x > m or x < m ) by XXREAL_0:1;

suppose x = m ; :: thesis: contradiction

hence contradiction by A13; :: thesis: verum

end;

suppose x > m ; :: thesis: contradiction

hence contradiction by A13; :: thesis: verum

end;

suppose A17: x < m ; :: thesis: contradiction

m < x + r by A12, XREAL_1:21;
then m - x < r by XREAL_1:21;
then A18: m - x < 1 by A14, XXREAL_0:2;
m >= x + 1 by A17, NAT_1:13;
hence contradiction by A18, XREAL_1:21; :: thesis: verum

end;

end;

end;

hence x in REAL \ NAT by XBOOLE_0:def 5; :: thesis: S₁[n,x]
x + 0 < m + r by A10, A13, XREAL_1:10;
then x in { a where a is Real : ( m - r < a & a < m + r ) } by A12;
then x in ].(m - r),(m + r).[ by RCOMP_1:def 2;
then A19: x in Ball m9,r by Th7;
then x in An by A11, XBOOLE_0:def 4;
then x in An \ NAT by A16, XBOOLE_0:def 5;
then A20: x in Bn by A8, XBOOLE_0:def 3;
take m ; :: thesis: ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ )
Ball m9,(1 / 4) = ].(m - (1 / 4)),(m + (1 / 4)).[ by Th7;
then x in ].(m - (1 / 4)),(m + (1 / 4)).[ by A11, A19, XBOOLE_0:def 4;
hence ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A20, XBOOLE_0:def 4; :: thesis: verum

end;

consider S being Function such that
A21: dom S = NAT and
A22: rng S c= REAL \ NAT and
A23: for n being set st n in NAT holds
S₁[n,S . n] from WELLORD2:sch 1(A3);
reconsider S = S as sequence of R^1 by A21, A22, FUNCT_2:4, TOPMETR:24, XBOOLE_1:1;
reconsider O = rng S as Subset of R^1 ;
for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[

proof

let n be Element of NAT ; :: thesis: S . n in ].(n - (1 / 4)),(n + (1 / 4)).[
ex m being Element of NAT st
( m = n & S . n in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A23;
hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by XBOOLE_0:def 4; :: thesis: verum

end;

then O is closed by Th9;
then A24: ([#] R^1 ) \ O is open by PRE_TOPC:def 6;
set A = ((O ` ) \ NAT ) \/ {REAL };
((O ` ) \ NAT ) \/ {REAL } c= (REAL \ NAT ) \/ {REAL }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((O ` ) \ NAT ) \/ {REAL } or x in (REAL \ NAT ) \/ {REAL } )
assume x in ((O ` ) \ NAT ) \/ {REAL } ; :: thesis: x in (REAL \ NAT ) \/ {REAL }
then ( x in (O ` ) \ NAT or x in {REAL } ) by XBOOLE_0:def 3;
then ( ( x in O ` & not x in NAT ) or x in {REAL } ) by XBOOLE_0:def 5;
then ( x in REAL \ NAT or x in {REAL } ) by TOPMETR:24, XBOOLE_0:def 5;
hence x in (REAL \ NAT ) \/ {REAL } by XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider A = ((O ` ) \ NAT ) \/ {REAL } as Subset of REAL? by Def7;
reconsider A = A as Subset of REAL? ;
NAT c= O `

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in O ` )
assume A25: x in NAT ; :: thesis: x in O `
then not x in rng S by A22, XBOOLE_0:def 5;
hence x in O ` by A25, TOPMETR:24, XBOOLE_0:def 5; :: thesis: verum

end;

then ( A is open & REAL in A ) by A24, Th31;
then consider V being Subset of REAL? such that
A26: V in B and
A27: V c= A by YELLOW_8:22;
consider n1 being set such that
A28: n1 in dom h and
A29: V = h . n1 by A2, A26, FUNCT_1:def 5;
reconsider n = n1 as Element of NAT by A28;
for n being Element of NAT ex x being set st
( x in h . n & not x in A )

proof

let n be Element of NAT ; :: thesis: ex x being set st
( x in h . n & not x in A )
consider xn being set such that
A30: xn = S . n ;
take xn ; :: thesis: ( xn in h . n & not xn in A )
A31: S . n in rng S by A21, FUNCT_1:def 5;
then not xn in ([#] R^1 ) \ O by A30, XBOOLE_0:def 5;
then A32: not xn in (O ` ) \ NAT by XBOOLE_0:def 5;
not xn = REAL

proof

assume xn = REAL ; :: thesis: contradiction
then REAL in REAL by A22, A30, A31, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum

end;

then A33: not xn in {REAL } by TARSKI:def 1;
ex m being Element of NAT st
( m = n & S . n in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by A23;
hence ( xn in h . n & not xn in A ) by A30, A32, A33, XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum

end;

then ex x being set st
( x in h . n & not x in A ) ;
hence contradiction by A27, A29; :: thesis: verum