:: deftheorem Def4 defines with_open_semilattices WAYBEL30:def 4 :
for N being non empty TopRelStr holds
( N is with_open_semilattices iff for x being Point of N ex J being Basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting );