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 Th11;
sup D = lim_inf N ;
then A2: sup D = sup (inf_net N) by Th29;
let V be a_neighborhood of x; :: according to WAYBEL_9:def 9 :: thesis: N is_often_in V
A3: for a being Element of R holds downarrow a = Cl {a} by Def2;
Int V is open by TOPS_1:51;
then A4: Int V is upper by A3, Th25;
x in Int V by CONNSP_2:def 1;
then sup D in Int V by A1, A4, WAYBEL_0:def 20;
then reconsider W = Int V as a_neighborhood of sup D by CONNSP_2:5, TOPS_1:51;
A5: Int V c= V by TOPS_1:44;
inf_net N is_eventually_in W by A2, Def2;
then N is_eventually_in W by A4, Th31;
then N is_eventually_in V by A5, WAYBEL_0:8;
hence N is_often_in V by YELLOW_6:28; :: thesis: verum