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;
N . i in rng the mapping of N by A6, FUNCT_1:def 3;
then N . i >= b by A4, LATTICE3:def 8;
then A7: b "\/" (N . i) = N . i by YELLOW_0:24;
b in {b} by TARSKI:def 1;
hence N . i in {b} "\/" ([#] S) by A7, YELLOW_4:10; :: thesis: verum

end;

A8: 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
A9: x in dom the mapping of N and
A10: y = the mapping of N . x by FUNCT_1:def 3;
reconsider x = x as Element of N by A9;
y = N . x by A10;
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 ( {b} "\/" ([#] S) = { (b "\/" y) where y is Element of S : y in [#] S } & c in {b} "\/" ([#] S) ) by A3, A8, Th34, YELLOW_4:15;
then ex y being Element of S st
( c = b "\/" y & y in [#] S ) ;
hence d >= b by A1, YELLOW_0:22; :: thesis: verum