let S be Hausdorff TopLattice; :: thesis: for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds
uparrow x is closed
let x be Element of S; :: thesis: ( ( for a being Element of S holds a "/\" is continuous ) implies uparrow x is closed )
assume for a being Element of S holds a "/\" is continuous ; :: thesis: uparrow x is closed
then A1: x "/\" is continuous ;
( (x "/\") " {x} = uparrow x & {x} is closed ) by Th7, PCOMPS_1:7;
hence uparrow x is closed by A1; :: thesis: verum