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

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