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-directed holds
( ex_sup_of N & sup 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-directed holds
( ex_sup_of N & sup N in Lim N )
let N be net of S; :: thesis: ( N is eventually-directed implies ( ex_sup_of N & sup N in Lim N ) )
assume A2: N is eventually-directed ; :: thesis: ( ex_sup_of N & sup 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 = sup N by A1, A2, A4, Th35
.= d by A1, A2, A5, Th35 ; :: thesis: verum

end;

consider c being Point of S such that
A6: c is_a_cluster_point_of N by Th30;
thus ex_sup_of N :: thesis: sup 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, Lm5, Lm6;
hence ex_sup_of rng the mapping of N,S by YELLOW_0:15; :: according to WAYBEL_9:def 3 :: thesis: verum

end;

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