for L being TopLattice
for x being Element of L st ( for X being Subset of L st X is open holds
X is upper ) holds
uparrow x is compact