let R be non empty up-complete /\-complete order_consistent TopLattice; :: thesis: for N being eventually-directed net of R
for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let N be eventually-directed net of R; :: thesis: for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let x be Element of R; :: thesis: ( x <= lim_inf N iff x is_a_cluster_point_of N )
thus ( x <= lim_inf N implies x is_a_cluster_point_of N ) by Th28; :: thesis: ( x is_a_cluster_point_of N implies x <= lim_inf N )
thus ( x is_a_cluster_point_of N implies x <= lim_inf N ) :: thesis: verum

proof

assume A1: x is_a_cluster_point_of N ; :: thesis: x <= lim_inf 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;
for G being Subset of R st G is open & x in G holds
{(sup D)} meets G

proof

let G be Subset of R; :: thesis: ( G is open & x in G implies {(sup D)} meets G )
assume A2: G is open ; :: thesis: ( not x in G or {(sup D)} meets G )
assume x in G ; :: thesis: {(sup D)} meets G
then reconsider G = G as a_neighborhood of x by A2, CONNSP_2:3;
A3: N is_often_in G by A1;

now :: thesis: for i being Element of N holds sup D in G

let i be Element of N; :: thesis: sup D in G
consider j1 being Element of N such that
i <= j1 and
A4: N . j1 in G by A3;
consider j2 being Element of N such that
A5: for k being Element of N st j2 <= k holds
N . j1 <= N . k by WAYBEL_0:11;
defpred S₂[ Element of N] means $1 >= j2;
deffunc H₂( Element of N) -> Element of the carrier of R = N . $1;
set E = { H₂(k) where k is Element of N : S₂[k] } ;
A6: { H₂(k) where k is Element of N : S₂[k] } is Subset of R from DOMAIN_1:sch 8();
consider j9 being Element of N such that
A7: j9 >= j2 and
j9 >= j2 by YELLOW_6:def 3;
N . j9 in { H₂(k) where k is Element of N : S₂[k] } by A7;
then reconsider E9 = { H₂(k) where k is Element of N : S₂[k] } as non empty Subset of R by A6;
A8: ex_inf_of E9,R by WAYBEL_0:76;
N . j1 is_<=_than E9

proof

let b be Element of R; :: according to LATTICE3:def 8 :: thesis: ( not b in E9 or N . j1 <= b )
assume b in E9 ; :: thesis: N . j1 <= b
then ex k being Element of N st
( b = N . k & k >= j2 ) ;
hence N . j1 <= b by A5; :: thesis: verum

end;

then A9: N . j1 <= "/\" (E9,R) by A8, YELLOW_0:31;
for a being Element of R holds downarrow a = Cl {a} by Def2;
then A10: G is upper by A2, Th21;
then A11: "/\" (E9,R) in G by A4, A9;
"/\" (E9,R) in D ;
then "/\" (E9,R) <= sup D by Th17;
hence sup D in G by A10, A11; :: thesis: verum

end;

then A12: sup D in G ;
sup D in {(sup D)} by TARSKI:def 1;
hence {(sup D)} meets G by A12, XBOOLE_0:3; :: thesis: verum

end;

then x in Cl {(sup D)} by PRE_TOPC:24;
then x in downarrow (sup D) by Def2;
hence x <= lim_inf N by WAYBEL_0:17; :: thesis: verum

end;