let S be Hausdorff compact TopLattice; :: thesis: for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
c = inf N
let c be Point of S; :: thesis: for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
c = inf N
let N be net of S; :: thesis: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N implies c = inf N )
assume that
A1: for x being Element of S holds x "/\" is continuous and
A2: N is eventually-filtered and
A3: c is_a_cluster_point_of N ; :: thesis: c = inf N
reconsider c' = c as Element of S ;
A4: c' is_<=_than rng the mapping of N by A1, A2, A3, Lm7;
for b being Element of S st rng the mapping of N is_>=_than b holds
c' >= b by A1, A3, Lm8;
hence c = inf (rng the mapping of N) by A4, YELLOW_0:31
.= inf N by YELLOW_2:def 6 ;
:: thesis: verum