let T be non empty TopSpace; for N being net of T
for x being Point of T st x is_a_cluster_point_of N holds
ex M being subnet of N st x in Lim M
let N be net of T; for x being Point of T st x is_a_cluster_point_of N holds
ex M being subnet of N st x in Lim M
let x be Point of T; ( x is_a_cluster_point_of N implies ex M being subnet of N st x in Lim M )
assume A1:
x is_a_cluster_point_of N
; ex M being subnet of N st x in Lim M
set q = the Element of N;
set S9 = { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } ;
reconsider O = [#] T as Element of (OpenNeighborhoods x) by YELLOW_6:30;
N . the Element of N in [#] T
;
then
[ the Element of N,O] in { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O }
;
then reconsider S9 = { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } as non empty set ;
set n = the mapping of N;
defpred S1[ set , set ] means ex s1, s2 being Element of N st
( s1 = $1 `1 & s2 = $2 `1 & s1 <= s2 & $2 `2 c= $1 `2 );
consider L being non empty strict RelStr such that
A2:
the carrier of L = S9
and
A3:
for a, b being Element of L holds
( a <= b iff S1[a,b] )
from YELLOW_0:sch 1();
deffunc H1( Element of L) -> set = the mapping of N . ($1 `1);
A4:
for a being Element of L holds H1(a) in the carrier of T
consider g being Function of the carrier of L, the carrier of T such that
A6:
for x being Element of L holds g . x = H1(x)
from FUNCT_2:sch 8(A4);
set M = NetStr(# the carrier of L, the InternalRel of L,g #);
for a, b being Element of NetStr(# the carrier of L, the InternalRel of L,g #) ex z being Element of NetStr(# the carrier of L, the InternalRel of L,g #) st
( a <= z & b <= z )
proof
let a,
b be
Element of
NetStr(# the
carrier of
L, the
InternalRel of
L,
g #);
ex z being Element of NetStr(# the carrier of L, the InternalRel of L,g #) st
( a <= z & b <= z )
a in S9
by A2;
then consider aa being
Element of
N,
Oa being
Element of
(OpenNeighborhoods x) such that A7:
a = [aa,Oa]
and
N . aa in Oa
;
b in S9
by A2;
then consider bb being
Element of
N,
Ob being
Element of
(OpenNeighborhoods x) such that A8:
b = [bb,Ob]
and
N . bb in Ob
;
consider z1 being
Element of
N such that A9:
aa <= z1
and A10:
bb <= z1
by YELLOW_6:def 3;
(
Oa is
a_neighborhood of
x &
Ob is
a_neighborhood of
x )
by Th21;
then
Oa /\ Ob is
a_neighborhood of
x
by CONNSP_2:2;
then
N is_often_in Oa /\ Ob
by A1;
then consider d being
Element of
N such that A11:
z1 <= d
and A12:
N . d in Oa /\ Ob
;
Oa /\ Ob is
Element of
(OpenNeighborhoods x)
by Th22;
then
[d,(Oa /\ Ob)] in S9
by A12;
then reconsider z =
[d,(Oa /\ Ob)] as
Element of
NetStr(# the
carrier of
L, the
InternalRel of
L,
g #)
by A2;
reconsider A1 =
a,
C7 =
b,
z2 =
z as
Element of
L ;
A13:
(
C7 `1 = bb &
C7 `2 = Ob )
by A8;
take
z
;
( a <= z & b <= z )
A14:
(
A1 `1 = aa &
A1 `2 = Oa )
by A7;
A15:
(
z2 `1 = d &
z2 `2 = Oa /\ Ob )
;
(
Oa /\ Ob c= Ob &
bb <= d )
by A10, A11, XBOOLE_1:17, YELLOW_0:def 2;
then A16:
C7 <= z2
by A3, A13, A15;
(
Oa /\ Ob c= Oa &
aa <= d )
by A9, A11, XBOOLE_1:17, YELLOW_0:def 2;
then
A1 <= z2
by A3, A14, A15;
hence
(
a <= z &
b <= z )
by A16;
verum
end;
then reconsider M = NetStr(# the carrier of L, the InternalRel of L,g #) as prenet of T by YELLOW_6:def 3;
M is transitive
proof
let x,
y,
z be
Element of
M;
YELLOW_0:def 2 ( not x <= y or not y <= z or x <= z )
assume that A17:
x <= y
and A18:
y <= z
;
x <= z
reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
L ;
x1 <= y1
by A17;
then consider sx,
sy being
Element of
N such that A19:
sx = x1 `1
and A20:
(
sy = y1 `1 &
sx <= sy &
y1 `2 c= x1 `2 )
by A3;
y1 <= z1
by A18;
then consider s1,
s2 being
Element of
N such that A21:
s1 = y1 `1
and A22:
s2 = z1 `1
and A23:
(
s1 <= s2 &
z1 `2 c= y1 `2 )
by A3;
(
sx <= s2 &
z1 `2 c= x1 `2 )
by A20, A21, A23, YELLOW_0:def 2;
then
x1 <= z1
by A3, A19, A22;
hence
x <= z
;
verum
end;
then reconsider M = M as net of T ;
M is subnet of N
then reconsider M = M as subnet of N ;
take
M
; x in Lim M
for V being a_neighborhood of x holds M is_eventually_in V
hence
x in Lim M
by YELLOW_6:def 15; verum