reconsider y = REAL as Point of REAL? by Th27;
assume REAL? is first-countable ; :: thesis: contradiction
then consider B being Basis of y such that
A1: B is countable ;
consider h being sequence of B such that
A2: rng h = B by ;
defpred S1[ object , object ] means ex m being Element of NAT st
( m = \$1 & \$2 in (h . \$1) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ );
A3: for n being object st n in NAT holds
ex x being object st
( x in REAL \ NAT & S1[n,x] )
proof
let n be object ; :: thesis: ( n in NAT implies ex x being object st
( x in REAL \ NAT & S1[n,x] ) )

assume A4: n in NAT ; :: thesis: ex x being object st
( x in REAL \ NAT & S1[n,x] )

then reconsider m = n as Element of NAT ;
n in dom h by ;
then A5: h . n in rng h by FUNCT_1:def 3;
then reconsider Bn = h . n as Subset of REAL? by A2;
m in REAL by XREAL_0:def 1;
then reconsider m9 = m as Point of RealSpace by METRIC_1:def 13;
reconsider Kn = Ball (m9,(1 / 4)) as Subset of R^1 by TOPMETR:12;
reconsider Bn = Bn as Subset of REAL? ;
( Bn is open & y in Bn ) by ;
then consider An being Subset of R^1 such that
A6: An is open and
A7: NAT c= An and
A8: Bn = (An \ NAT) \/ by Th28;
reconsider An9 = An as Subset of R^1 ;
Kn is open by TOPMETR:14;
then A9: An9 /\ Kn is open by ;
dist (m9,m9) = 0 by METRIC_1:1;
then m9 in Ball (m9,(1 / 4)) by METRIC_1:11;
then n in An /\ (Ball (m9,(1 / 4))) by ;
then consider r being Real such that
A10: r > 0 and
A11: Ball (m9,r) c= An /\ Kn by ;
reconsider r = r as Real ;
m < m + r by ;
then m - r < m by XREAL_1:19;
then consider x being Real such that
A12: m - r < x and
A13: x < m by XREAL_1:5;
reconsider x = x as Element of REAL by XREAL_0:def 1;
take x ; :: thesis: ( x in REAL \ NAT & S1[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:24;
then A15: (- r) + m < (- (1 / 2)) + m by XREAL_1:6;
(- (1 / 2)) + m < r + m by ;
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 ;
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:6; :: 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;
end;
end;
hence x in REAL \ NAT by XBOOLE_0:def 5; :: thesis: S1[n,x]
x + 0 < m + r by ;
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 ;
then x in An \ NAT by ;
then A20: x in Bn by ;
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 ;
hence ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ ) by ; :: 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 object st n in NAT holds
S1[n,S . n] from reconsider S = S as sequence of R^1 by ;
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 3;
set A = ((O `) \ NAT) \/ ;
((O `) \ NAT) \/ c= () \/
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((O `) \ NAT) \/ or x in () \/ )
assume x in ((O `) \ NAT) \/ ; :: thesis: x in () \/
then ( x in (O `) \ NAT or x in ) by XBOOLE_0:def 3;
then ( ( x in O ` & not x in NAT ) or x in ) by XBOOLE_0:def 5;
then ( x in REAL \ NAT or x in ) by ;
hence x in () \/ by XBOOLE_0:def 3; :: thesis: verum
end;
then reconsider A = ((O `) \ NAT) \/ as Subset of REAL? by Def8;
reconsider A = A as Subset of REAL? ;
NAT c= O `
proof
let x be object ; :: 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 ;
hence x in O ` by ; :: thesis: verum
end;
then ( A is open & REAL in A ) by ;
then consider V being Subset of REAL? such that
A26: V in B and
A27: V c= A by YELLOW_8:13;
consider n1 being object such that
A28: n1 in dom h and
A29: V = h . n1 by ;
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 ;
then not xn in () \ O by ;
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 ;
hence contradiction ; :: thesis: verum
end;
then A33: not xn in 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 ; :: thesis: verum
end;
then ex x being set st
( x in h . n & not x in A ) ;
hence contradiction by A27, A29; :: thesis: verum