let A be Subset of REAL? ; :: according to FRECHET:def 5 :: thesis: for x being Point of REAL? st x in Cl A holds
ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
let x be Point of REAL? ; :: thesis: ( x in Cl A implies ex S being sequence of REAL? st
( rng S c= A & x in Lim S ) )
assume A1:
x in Cl A
; :: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
x in the carrier of REAL?
;
then
x in (REAL \ NAT ) \/ {REAL }
by Def7;
then A2:
( x in REAL \ NAT or x in {REAL } )
by XBOOLE_0:def 3;
per cases
( x in REAL \ NAT or ( x = REAL & x in A ) or ( x = REAL & not x in A ) )
by A2, TARSKI:def 1;
suppose A25:
(
x = REAL & not
x in A )
;
:: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )then reconsider A' =
A as
Subset of
R^1 by Th32;
ex
k being
Point of
R^1 st
(
k in NAT & ex
S' being
sequence of
R^1 st
(
rng S' c= A' &
S' is_convergent_to k ) )
proof
defpred S1[
set ,
set ]
means ( $1
in $2 & $2
in the
topology of
R^1 & $2
/\ A' = {} );
assume A26:
for
k being
Point of
R^1 holds
( not
k in NAT or for
S' being
sequence of
R^1 holds
( not
rng S' c= A' or not
S' is_convergent_to k ) )
;
:: thesis: contradiction
A27:
for
k being
set st
k in NAT holds
ex
U1 being
set st
S1[
k,
U1]
proof
given k being
set such that A28:
k in NAT
and A29:
for
U1 being
set st
k in U1 &
U1 in the
topology of
R^1 holds
not
U1 /\ A' = {}
;
:: thesis: contradiction
reconsider k =
k as
Point of
R^1 by A28, TOPMETR:24;
reconsider k'' =
k as
Point of
(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
reconsider k' =
k'' as
Point of
RealSpace by TOPMETR:16;
consider Bs being
Basis of
k'' such that A30:
Bs = { (Ball k',(1 / n)) where n is Element of NAT : n <> 0 }
and
Bs is
countable
and A31:
ex
f being
Function of
NAT ,
Bs st
for
n being
set st
n in NAT holds
ex
n' being
Element of
NAT st
(
n = n' &
f . n = Ball k',
(1 / (n' + 1)) )
by Th11;
consider h being
Function of
NAT ,
Bs such that A32:
for
n being
set st
n in NAT holds
ex
n' being
Element of
NAT st
(
n = n' &
h . n = Ball k',
(1 / (n' + 1)) )
by A31;
defpred S2[
set ,
set ]
means $2
in (h . $1) /\ A';
A33:
for
n being
set st
n in NAT holds
ex
z being
set st
(
z in the
carrier of
R^1 &
S2[
n,
z] )
consider S' being
Function such that A36:
(
dom S' = NAT &
rng S' c= the
carrier of
R^1 )
and A37:
for
n being
set st
n in NAT holds
S2[
n,
S' . n]
from WELLORD2:sch 1(A33);
reconsider S' =
S' as
Function of
NAT ,the
carrier of
R^1 by A36, FUNCT_2:4;
A38:
S' is_convergent_to k
rng S' c= A'
hence
contradiction
by A26, A28, A38;
:: thesis: verum
end;
consider g being
Function such that A47:
(
dom g = NAT & ( for
k being
set st
k in NAT holds
S1[
k,
g . k] ) )
from CLASSES1:sch 1(A27);
rng g c= bool the
carrier of
R^1
then reconsider F =
rng g as
Subset-Family of
R^1 ;
F is
open
then A52:
union F is
open
by TOPS_2:26;
(union F) \ NAT c= REAL \ NAT
by TOPMETR:24, XBOOLE_1:33;
then
((union F) \ NAT ) \/ {REAL } c= (REAL \ NAT ) \/ {REAL }
by XBOOLE_1:9;
then reconsider B =
((union F) \ NAT ) \/ {REAL } as
Subset of
REAL? by Def7;
reconsider B =
B as
Subset of
REAL? ;
A53:
B /\ A = {}
NAT c= union F
then
(
B is
open &
REAL in B )
by A52, Th31;
then
A meets B
by A1, A25, PRE_TOPC:def 13;
hence
contradiction
by A53, XBOOLE_0:def 7;
:: thesis: verum
end; then consider k being
Point of
R^1 such that A61:
k in NAT
and A62:
ex
S' being
sequence of
R^1 st
(
rng S' c= A' &
S' is_convergent_to k )
;
consider S' being
sequence of
R^1 such that A63:
rng S' c= A'
and A64:
S' is_convergent_to k
by A62;
reconsider S =
S' as
sequence of
REAL? by A63, Th2, XBOOLE_1:1;
take
S
;
:: thesis: ( rng S c= A & x in Lim S )thus
rng S c= A
by A63;
:: thesis: x in Lim S
S is_convergent_to x
hence
x in Lim S
by Def4;
:: thesis: verum end;