let N be non empty TopSpace-like TopRelStr ; :: thesis: ( N is with_compact_semilattices implies N is with_small_semilattices )
assume A3: 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 & A is compact ) ; :: according to WAYBEL30:def 3 :: 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
A4: for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact ) by A3;
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 A4; :: thesis: verum