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 A1, CARD_3:96;
defpred S₁[ 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 & S₁[n,x] )

proof

let n be object ; :: thesis: ( n in NAT implies ex x being object st
( x in REAL \ NAT & S₁[n,x] ) )
assume A4: n in NAT ; :: thesis: ex x being object 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 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 A5, YELLOW_8:12;
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 Th28;
reconsider An9 = An as Subset of R^1 ;
Kn is open by TOPMETR:14;
then A9: An9 /\ Kn is open by A6, TOPS_1:11;
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 A4, A7, XBOOLE_0:def 4;
then consider r being Real such that
A10: r > 0 and
A11: Ball (m9,r) c= An /\ Kn by A9, TOPMETR:15;
reconsider r = r as Real ;
m < m + r by A10, XREAL_1:29;
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 & 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:24;
then A15: (- r) + m < (- (1 / 2)) + m by XREAL_1:6;
(- (1 / 2)) + m < r + m by A10, XREAL_1:6;
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: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;

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:19;
then m - x < r by XREAL_1:19;
then A18: m - x < 1 by A14, XXREAL_0:2;
m >= x + 1 by A17, NAT_1:13;
hence contradiction by A18, XREAL_1:19; :: 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:8;
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 object st n in NAT holds
S₁[n,S . n] from FUNCT_1:sch 6(A3);
reconsider S = S as sequence of R^1 by A21, A22, FUNCT_2:2, TOPMETR:17, 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 3;
set A = ((O `) \ NAT) \/ {REAL};
((O `) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL}

proof

let x be object ; :: 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:17, 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 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 A22, XBOOLE_0:def 5;
hence x in O ` by A25, TOPMETR:17, XBOOLE_0:def 5, NUMBERS:19; :: thesis: verum

end;

then ( A is open & REAL in A ) by A24, Th28;
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 A2, A26, FUNCT_1:def 3;
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 3;
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