for N being with_infima topological_semilattice TopPoset
for C being Subset of N st subrelstr C is meet-inheriting holds
subrelstr (Cl C) is meet-inheriting