let S be Hausdorff compact TopLattice; :: thesis: for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
let N be net of S; :: thesis: for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
let c be Point of S; :: thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
let d be Element of S; :: thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N implies d is_<=_than rng the mapping of N )
assume that
A1: c = d and
A2: for x being Element of S holds x "/\" is continuous and
A3: N is eventually-filtered and
A4: c is_a_cluster_point_of N ; :: thesis: d is_<=_than rng the mapping of N
let i be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not i in rng the mapping of N or d <= i )
assume i in rng the mapping of N ; :: thesis: d <= i
then consider iJ being object such that
A5: iJ in dom the mapping of N and
A6: the mapping of N . iJ = i by FUNCT_1:def 3;
reconsider i1 = iJ as Element of N by A5;
downarrow (N . i1) is closed by A2, Th28;
then A7: Cl (downarrow (N . i1)) = downarrow (N . i1) by PRE_TOPC:22;
N is_eventually_in downarrow (N . i1)
proof
consider j being Element of N such that
A8: for k being Element of N st j <= k holds
N . i1 >= N . k by A3, WAYBEL_0:12;
take j ; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in downarrow (N . i1) )
let k be Element of N; :: thesis: ( not j <= k or N . k in downarrow (N . i1) )
assume j <= k ; :: thesis: N . k in downarrow (N . i1)
then N . i1 >= N . k by A8;
hence N . k in downarrow (N . i1) by WAYBEL_0:17; :: thesis: verum
end;
then consider t being Element of N such that
A9: for j being Element of N st t <= j holds
N . j in downarrow (N . i1) ;
reconsider A = N | t as subnet of N ;
A10: rng the mapping of A c= downarrow (N . i1)
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng the mapping of A or q in downarrow (N . i1) )
assume q in rng the mapping of A ; :: thesis: q in downarrow (N . i1)
then consider x being object such that
A11: x in dom the mapping of A and
A12: q = the mapping of A . x by FUNCT_1:def 3;
reconsider x = x as Element of A by A11;
consider y being Element of N such that
A13: y = x and
A14: t <= y by Def7;
A . x = N . y by A13, Th16;
hence q in downarrow (N . i1) by A9, A12, A14; :: thesis: verum
end;
c is_a_cluster_point_of A
proof
let O be a_neighborhood of c; :: according to WAYBEL_9:def 9 :: thesis: A is_often_in O
let i be Element of A; :: according to WAYBEL_0:def 12 :: thesis: ex b1 being Element of the carrier of A st
( i <= b1 & A . b1 in O )
consider i2 being Element of N such that
A15: i2 = i and
A16: t <= i2 by Def7;
N is_often_in O by A4;
then consider j2 being Element of N such that
A17: i2 <= j2 and
A18: N . j2 in O ;
t <= j2 by A16, A17, YELLOW_0:def 2;
then reconsider j = j2 as Element of A by Def7;
take j ; :: thesis: ( i <= j & A . j in O )
A is full SubNetStr of N by Th14;
hence i <= j by A15, A17, YELLOW_6:12; :: thesis: A . j in O
thus A . j in O by A18, Th16; :: thesis: verum
end;
then consider M being subnet of A such that
A19: c in Lim M by Th32;
reconsider R = rng the mapping of M as Subset of S ;
A20: downarrow (N . i1) = { z where z is Element of S : z "\/" (N . i1) = N . i1 } by Lm2;
ex f being Function of M,A st
( the mapping of M = the mapping of A * f & ( for m being Element of A ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p ) ) by YELLOW_6:def 9;
then R c= rng the mapping of A by RELAT_1:26;
then R c= downarrow (N . i1) by A10;
then A21: Cl R c= Cl (downarrow (N . i1)) by PRE_TOPC:19;
c in Cl R by A19, Th24;
then c in downarrow (N . i1) by A7, A21;
then ex z being Element of S st
( c = z & z "\/" (N . i1) = N . i1 ) by A20;
hence d <= i by A1, A6, YELLOW_0:24; :: thesis: verum