theorem Th52: :: WAYBEL21:52

for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is infs-inheriting