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 ;
A2: (x "/\" ) " {x} = uparrow x by Th7;
{x} is closed by PCOMPS_1:10;
hence uparrow x is closed by A1, A2, PRE_TOPC:def 12; :: thesis: verum