assume A1:
REAL? is first-countable
; :: thesis: contradiction
reconsider y = REAL as Point of REAL? by Th30;
consider B being Basis of y such that
A2:
B is countable
by A1, Def1;
consider h being Function of NAT ,B such that
A3:
rng h = B
by A2, CARD_3:146;
defpred S1[ set , set ] means ex m being Element of NAT st
( m = $1 & $2 in (h . $1) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ );
A4:
for n being set st n in NAT holds
ex x being set st
( x in REAL \ NAT & S1[n,x] )
proof
let n be
set ;
:: thesis: ( n in NAT implies ex x being set st
( x in REAL \ NAT & S1[n,x] ) )
assume A5:
n in NAT
;
:: thesis: ex x being set st
( x in REAL \ NAT & S1[n,x] )
then
n in dom h
by FUNCT_2:def 1;
then A6:
h . n in rng h
by FUNCT_1:def 5;
then reconsider Bn =
h . n as
Subset of
REAL? by A3;
reconsider Bn =
Bn as
Subset of
REAL? ;
(
Bn is
open &
y in Bn )
by A6, YELLOW_8:21;
then consider An being
Subset of
R^1 such that A7:
An is
open
and A8:
NAT c= An
and A9:
Bn = (An \ NAT ) \/ {REAL }
by Th31;
reconsider An' =
An as
Subset of
(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
reconsider m =
n as
Element of
NAT by A5;
reconsider m' =
m as
Point of
RealSpace by METRIC_1:def 14;
A10:
Ball m',
(1 / 4) = ].(m - (1 / 4)),(m + (1 / 4)).[
by Th7;
dist m',
m' = 0
by METRIC_1:1;
then
m' in Ball m',
(1 / 4)
by METRIC_1:12;
then A11:
n in An /\ (Ball m',(1 / 4))
by A5, A8, XBOOLE_0:def 4;
reconsider Kn =
Ball m',
(1 / 4) as
Subset of
(TopSpaceMetr RealSpace ) by TOPMETR:16;
Kn is
open
by TOPMETR:21;
then
An' /\ Kn is
open
by A7, TOPMETR:def 7, TOPS_1:38;
then consider r being
real number such that A12:
r > 0
and A13:
Ball m',
r c= An /\ Kn
by A11, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
A14:
r < 1
m < m + r
by A12, XREAL_1:31;
then
m - r < m
by XREAL_1:21;
then consider x being
real number such that A17:
m - r < x
and A18:
x < m
by XREAL_1:7;
reconsider x =
x as
Real by XREAL_0:def 1;
take
x
;
:: thesis: ( x in REAL \ NAT & S1[n,x] )
x + 0 < m + r
by A12, A18, XREAL_1:10;
then
x in { a where a is Real : ( m - r < a & a < m + r ) }
by A17;
then
x in ].(m - r),(m + r).[
by RCOMP_1:def 2;
then A19:
x in Ball m',
r
by A12, Th7;
then A20:
x in ].(m - (1 / 4)),(m + (1 / 4)).[
by A10, A13, XBOOLE_0:def 4;
A21:
not
x in NAT
x in An
by A13, A19, XBOOLE_0:def 4;
then
x in An \ NAT
by A21, XBOOLE_0:def 5;
then A23:
x in Bn
by A9, XBOOLE_0:def 3;
thus
x in REAL \ NAT
by A21, XBOOLE_0:def 5;
:: thesis: S1[n,x]
take
m
;
:: thesis: ( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ )
thus
(
m = n &
x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ )
by A20, A23, XBOOLE_0:def 4;
:: thesis: verum
end;
consider S being Function such that
A24:
dom S = NAT
and
A25:
rng S c= REAL \ NAT
and
A26:
for n being set st n in NAT holds
S1[n,S . n]
from WELLORD2:sch 1(A4);
reconsider S = S as sequence of R^1 by A24, A25, FUNCT_2:4, TOPMETR:24, XBOOLE_1:1;
A27:
for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[
reconsider O = rng S as Subset of R^1 ;
O is closed
by A27, Th9;
then A30:
([#] R^1 ) \ O is open
by PRE_TOPC:def 6;
A31:
NAT c= O `
set A = ((O ` ) \ NAT ) \/ {REAL };
((O ` ) \ NAT ) \/ {REAL } c= (REAL \ NAT ) \/ {REAL }
then reconsider A = ((O ` ) \ NAT ) \/ {REAL } as Subset of REAL? by Def7;
reconsider A = A as Subset of REAL? ;
( A is open & REAL in A )
by A30, A31, Th31;
then consider V being Subset of REAL? such that
A33:
( V in B & V c= A )
by YELLOW_8:22;
A34:
for n being Element of NAT ex x being set st
( x in h . n & not x in A )
consider n1 being set such that
A39:
n1 in dom h
and
A40:
V = h . n1
by A3, A33, FUNCT_1:def 5;
reconsider n = n1 as Element of NAT by A39;
consider x being set such that
A41:
( x in h . n & not x in A )
by A34;
thus
contradiction
by A33, A40, A41; :: thesis: verum