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, Def9;
then consider d being
Element of
N such that A11:
z1 <= d
and A12:
N . d in Oa /\ Ob
by WAYBEL_0:def 12;
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, MCART_1:7;
take
z
;
( a <= z & b <= z )
A14:
(
A1 `1 = aa &
A1 `2 = Oa )
by A7, MCART_1:7;
A15:
(
z2 `1 = d &
z2 `2 = Oa /\ Ob )
by MCART_1:7;
(
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, YELLOW_0:1;
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, YELLOW_0:1;
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, YELLOW_0:1;
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, XBOOLE_1:1, YELLOW_0:def 2;
then
x1 <= z1
by A3, A19, A22;
hence
x <= z
by YELLOW_0:1;
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
proof
set i = the
Element of
N;
let V be
a_neighborhood of
x;
M is_eventually_in V
(
x in Int V &
Int V is
open )
by CONNSP_2:def 1;
then A30:
Int V in the
carrier of
(OpenNeighborhoods x)
by YELLOW_6:30;
then
Int V is
a_neighborhood of
x
by Th21;
then
N is_often_in Int V
by A1, Def9;
then consider s being
Element of
N such that
the
Element of
N <= s
and A31:
N . s in Int V
by WAYBEL_0:def 12;
A32:
M is_eventually_in Int V
proof
[s,(Int V)] in S9
by A30, A31;
then reconsider j =
[s,(Int V)] as
Element of
M by A2;
take
j
;
WAYBEL_0:def 11 for b1 being Element of the carrier of M holds
( not j <= b1 or M . b1 in Int V )
let s9 be
Element of
M;
( not j <= s9 or M . s9 in Int V )
assume A33:
j <= s9
;
M . s9 in Int V
reconsider j1 =
j,
s1 =
s9 as
Element of
L ;
j1 <= s1
by A33, YELLOW_0:1;
then A34:
ex
s1,
s2 being
Element of
N st
(
s1 = j `1 &
s2 = s9 `1 &
s1 <= s2 &
s9 `2 c= j `2 )
by A3;
s9 in S9
by A2;
then consider ss being
Element of
N,
OO being
Element of
(OpenNeighborhoods x) such that A35:
s9 = [ss,OO]
and A36:
N . ss in OO
;
A37:
(
j `2 = Int V &
s9 `2 = OO )
by A35, MCART_1:7;
M . s9 =
the
mapping of
N . (s9 `1)
by A6
.=
N . ss
by A35, MCART_1:7
;
hence
M . s9 in Int V
by A36, A34, A37;
verum
end;
Int V c= V
by TOPS_1:16;
hence
M is_eventually_in V
by A32, WAYBEL_0:8;
verum
end;
hence
x in Lim M
by YELLOW_6:def 15; verum