let S be Hausdorff compact TopLattice; :: thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N ) )
assume A1: for x being Element of S holds x "/\" is continuous ; :: thesis: for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N )
let N be net of S; :: thesis: ( N is eventually-filtered implies ( ex_inf_of N & inf N in Lim N ) )
assume A2: N is eventually-filtered ; :: thesis: ( ex_inf_of N & inf N in Lim N )
A3: for c, d being Point of S st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d

proof

let c, d be Point of S; :: thesis: ( c is_a_cluster_point_of N & d is_a_cluster_point_of N implies c = d )
assume that
A4: c is_a_cluster_point_of N and
A5: d is_a_cluster_point_of N ; :: thesis: c = d
thus c = inf N by A1, A2, A4, Th36
.= d by A1, A2, A5, Th36 ; :: thesis: verum

end;

consider c being Point of S such that
A6: c is_a_cluster_point_of N by Th30;
thus ex_inf_of N :: thesis: inf N in Lim N

proof

reconsider d = c as Element of S ;
set X = rng the mapping of N;
( rng the mapping of N is_>=_than d & ( for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b ) ) by A1, A2, A6, Lm7, Lm8;
hence ex_inf_of rng the mapping of N,S by YELLOW_0:16; :: according to WAYBEL_9:def 4 :: thesis: verum

end;

c = inf N by A1, A2, A6, Th36;
hence inf N in Lim N by A6, A3, Th33; :: thesis: verum