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 :: thesis: for i being Element of N holds N . i in {b} "/\" ([#] S)
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;
then A7: b "/\" (N . i) = N . i by YELLOW_0:25;
b in {b} by TARSKI:def 1;
hence N . i in {b} "/\" ([#] S) by A7, YELLOW_4:37; :: thesis: verum
end;
A8: rng the mapping of N c= {b} "/\" ([#] S)
proof
let y be object ; :: 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 object 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;
downarrow b is closed by A2, Th28;
then {b} "/\" ([#] S) is closed by Th5;
then ( {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } & c in {b} "/\" ([#] S) ) by A3, A8, Th34, YELLOW_4:42;
then ex y being Element of S st
( c = b "/\" y & y in [#] S ) ;
hence d <= b by A1, YELLOW_0:23; :: thesis: verum