let S be Hausdorff compact TopLattice; :: thesis: for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds
downarrow x is closed
let b be Element of S; :: thesis: ( ( for b being Element of S holds b "/\" is continuous ) implies downarrow b is closed )
assume for a being Element of S holds a "/\" is continuous ; :: thesis: downarrow b is closed
then A1: b "/\" is continuous ;
set g1 = (rng (b "/\")) |` (b "/\");
A2: (rng (b "/\")) |` (b "/\") = b "/\" by RELAT_1:94;
A3: dom (b "/\") = the carrier of S by FUNCT_2:def 1;
A4: {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } by YELLOW_4:42;
A5: rng (b "/\") = {b} "/\" ([#] S)

proof

thus rng (b "/\") c= {b} "/\" ([#] S) :: according to XBOOLE_0:def 10 :: thesis: {b} "/\" ([#] S) c= rng (b "/\")

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng (b "/\") or q in {b} "/\" ([#] S) )
assume q in rng (b "/\") ; :: thesis: q in {b} "/\" ([#] S)
then consider x being object such that
A6: x in dom (b "/\") and
A7: (b "/\") . x = q by FUNCT_1:def 3;
reconsider x1 = x as Element of S by A6;
q = b "/\" x1 by A7, WAYBEL_1:def 18;
hence q in {b} "/\" ([#] S) by A4; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {b} "/\" ([#] S) or q in rng (b "/\") )
assume q in {b} "/\" ([#] S) ; :: thesis: q in rng (b "/\")
then consider y being Element of S such that
A8: q = b "/\" y and
y in [#] S by A4;
q = (b "/\") . y by A8, WAYBEL_1:def 18;
hence q in rng (b "/\") by A3, FUNCT_1:def 3; :: thesis: verum

end;

then rng ((rng (b "/\")) |` (b "/\")) = {b} "/\" ([#] S) by RELAT_1:94
.= [#] (S | (rng (b "/\"))) by A5, PRE_TOPC:def 5
.= the carrier of (S | (rng (b "/\"))) ;
then reconsider g1 = (rng (b "/\")) |` (b "/\") as Function of S,(S | (rng (b "/\"))) by A2, A3, FUNCT_2:1;
rng g1 = {b} "/\" ([#] S) by A5, RELAT_1:94
.= [#] (S | ({b} "/\" ([#] S))) by PRE_TOPC:def 5 ;
then S | ({b} "/\" ([#] S)) is compact by A1, A2, A5, COMPTS_1:14, PRE_TOPC:27;
then {b} "/\" ([#] S) is compact by COMPTS_1:3;
hence downarrow b is closed by Th5; :: thesis: verum