for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T
for X being Subset of T st X = the carrier of S & Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )