theorem :: WAYBEL32:20

for R being complete connected LATTICE
for T being Scott TopAugmentation of R
for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) )