let N be non empty TopSpace-like TopRelStr ; :: thesis: ( N is with_open_semilattices implies N is with_small_semilattices )
assume A1: 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 ; :: according to WAYBEL30:def 4 :: thesis: N is with_small_semilattices
let x be Point of N; :: according to WAYBEL30:def 2 :: thesis: ex J being basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting
consider J being Basis of x such that
A2: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A1;
reconsider J = J as basis of x by YELLOW13:23;
take J ; :: thesis: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting
thus for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A2; :: thesis: verum