let R be non empty up-complete /\-complete order_consistent TopLattice; :: thesis: for N being net of R
for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
let N be net of R; :: thesis: for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
let x be Element of R; :: thesis: ( x <= lim_inf N implies x is_a_cluster_point_of N )
assume A1: x <= lim_inf N ; :: thesis: x is_a_cluster_point_of N
defpred S₁[ Element of N] means verum;
deffunc H₁( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,R);
set X = { H₁(j) where j is Element of N : S₁[j] } ;
{ H₁(j) where j is Element of N : S₁[j] } is Subset of R from DOMAIN_1:sch 8();
then reconsider D = { H₁(j) where j is Element of N : S₁[j] } as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th7;
sup D = lim_inf N ;
then A2: sup D = sup (inf_net N) by Th24;
let V be a_neighborhood of x; :: according to WAYBEL_9:def 9 :: thesis: N is_often_in V
for a being Element of R holds downarrow a = Cl {a} by Def2;
then A3: Int V is upper by Th21;
x in Int V by CONNSP_2:def 1;
then sup D in Int V by A1, A3;
then reconsider W = Int V as a_neighborhood of sup D by CONNSP_2:3;
A4: Int V c= V by TOPS_1:16;
inf_net N is_eventually_in W by A2, Def2;
then N is_eventually_in W by A3, Th26;
then N is_eventually_in V by A4, WAYBEL_0:8;
hence N is_often_in V by YELLOW_6:19; :: thesis: verum