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_{1}[ 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_{1}[n,x] )

A21: dom S = NAT and

A22: rng S c= REAL \ NAT and

A23: for n being object st n in NAT holds

S_{1}[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)).[

then A24: ([#] R^1) \ O is open by PRE_TOPC:def 3;

set A = ((O `) \ NAT) \/ {REAL};

((O `) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL}

reconsider A = A as Subset of REAL? ;

NAT c= O `

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 )

( x in h . n & not x in A ) ;

hence contradiction by A27, A29; :: thesis: verum

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

( 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

proof

consider S being Function such that
let n be object ; :: thesis: ( n in NAT implies ex x being object st

( x in REAL \ NAT & S_{1}[n,x] ) )

assume A4: n in NAT ; :: thesis: ex x being object st

( x in REAL \ NAT & S_{1}[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_{1}[n,x] )

A14: r < 1_{1}[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;( x in REAL \ NAT & S

assume A4: n in NAT ; :: thesis: ex x being object st

( x in REAL \ NAT & S

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

A14: r < 1

proof

A16:
not x in NAT
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;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

proof

hence
x in REAL \ NAT
by XBOOLE_0:def 5; :: thesis: S
assume
x in NAT
; :: thesis: contradiction

then reconsider x = x as Element of NAT ;

end;then reconsider x = x as Element of NAT ;

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

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;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

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

A21: dom S = NAT and

A22: rng S c= REAL \ NAT and

A23: for n being object st n in NAT holds

S

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

then
O is closed
by Th9;
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;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

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

then reconsider A = ((O `) \ NAT) \/ {REAL} as Subset of REAL? by Def8;
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;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

reconsider A = A as Subset of REAL? ;

NAT c= O `

proof

then
( A is open & REAL in A )
by A24, Th28;
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;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

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

then
ex x being set st
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

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;( 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

then A33:
not xn in {REAL}
by TARSKI:def 1;
assume
xn = REAL
; :: thesis: contradiction

then REAL in REAL by A22, A30, A31, XBOOLE_0:def 5;

hence contradiction ; :: thesis: verum

end;then REAL in REAL by A22, A30, A31, XBOOLE_0:def 5;

hence contradiction ; :: thesis: verum

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

( x in h . n & not x in A ) ;

hence contradiction by A27, A29; :: thesis: verum