let S be Hausdorff compact TopLattice; :: thesis: for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let N be net of S; :: thesis: for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let c be Point of S; :: thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let d be Element of S; :: thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N implies for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b )
assume that
A1: c = d and
A2: for x being Element of S holds x "/\" is continuous and
A3: c is_a_cluster_point_of N ; :: thesis: for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let b be Element of S; :: thesis: ( rng the mapping of N is_<=_than b implies d <= b )
assume A4: rng the mapping of N is_<=_than b ; :: thesis: d <= b

A5: now

let i be Element of N; :: thesis: N . i in {b} "/\" ([#] S)
A6: the carrier of N = dom the mapping of N by FUNCT_2:def 1;
then reconsider Ni = N . i as Element of rng the mapping of N by FUNCT_1:def 5;
N . i in rng the mapping of N by A6, FUNCT_1:def 5;
then N . i <= b by A4, LATTICE3:def 9;
then A7: b "/\" (N . i) = N . i by YELLOW_0:25;
( b in {b} & Ni in [#] S ) by TARSKI:def 1;
hence N . i in {b} "/\" ([#] S) by A7, YELLOW_4:37; :: thesis: verum

end;

A8: {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } by YELLOW_4:42;
A9: rng the mapping of N c= {b} "/\" ([#] S)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng the mapping of N or y in {b} "/\" ([#] S) )
assume y in rng the mapping of N ; :: thesis: y in {b} "/\" ([#] S)
then consider x being set such that
A10: x in dom the mapping of N and
A11: y = the mapping of N . x by FUNCT_1:def 5;
reconsider x = x as Element of N by A10;
y = N . x by A11;
hence y in {b} "/\" ([#] S) by A5; :: thesis: verum

end;

downarrow b is closed by A2, Th28;
then {b} "/\" ([#] S) is closed by Th5;
then c in {b} "/\" ([#] S) by A3, A9, Th34;
then consider y being Element of S such that
A12: c = b "/\" y and
y in [#] S by A8;
thus d <= b by A1, A12, YELLOW_0:23; :: thesis: verum