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 8;
then A7: b "\/" (N . i) = N . i by YELLOW_0:24;
( b in {b} & Ni in [#] S ) by TARSKI:def 1;
hence N . i in {b} "\/" ([#] S) by A7, YELLOW_4:10; :: thesis: verum

end;

A8: {b} "\/" ([#] S) = { (b "\/" y) where y is Element of S : y in [#] S } by YELLOW_4:15;
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;

uparrow b is closed by A2, Th27;
then {b} "\/" ([#] S) is closed by Th4;
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:22; :: thesis: verum