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

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