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 A1: for a being Element of S holds a "/\" is continuous ; :: thesis: downarrow b is closed
A2: {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } by YELLOW_4:42;
A3: b "/\" is continuous by A1;
set g1 = (rng (b "/\" )) | (b "/\" );
A4: (rng (b "/\" )) | (b "/\" ) = b "/\" by RELAT_1:125;
A5: dom (b "/\" ) = the carrier of S by FUNCT_2:def 1;
A6: 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 set ; :: 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 set such that
A7: x in dom (b "/\" ) and
A8: (b "/\" ) . x = q by FUNCT_1:def 5;
reconsider x1 = x as Element of S by A7;
q = b "/\" x1 by A8, WAYBEL_1:def 18;
hence q in {b} "/\" ([#] S) by A2; :: thesis: verum

end;

let q be set ; :: 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
A9: ( q = b "/\" y & y in [#] S ) by A2;
q = (b "/\" ) . y by A9, WAYBEL_1:def 18;
hence q in rng (b "/\" ) by A5, FUNCT_1:def 5; :: thesis: verum

end;

then rng ((rng (b "/\" )) | (b "/\" )) = {b} "/\" ([#] S) by RELAT_1:125
.= [#] (S | (rng (b "/\" ))) by A6, PRE_TOPC:def 10
.= the carrier of (S | (rng (b "/\" ))) ;
then reconsider g1 = (rng (b "/\" )) | (b "/\" ) as Function of S,(S | (rng (b "/\" ))) by A4, A5, FUNCT_2:3;
rng g1 = {b} "/\" ([#] S) by A6, RELAT_1:125
.= [#] (S | ({b} "/\" ([#] S))) by PRE_TOPC:def 10 ;
then S | ({b} "/\" ([#] S)) is compact by A3, A4, A6, COMPTS_1:23, PRE_TOPC:57;
then {b} "/\" ([#] S) is compact by COMPTS_1:12;
then {b} "/\" ([#] S) is closed ;
hence downarrow b is closed by Th5; :: thesis: verum