let T be 1 -element TopRelStr ; :: thesis: ( T is reflexive & T is TopSpace-like implies T is with_compact_semilattices )

assume ( T is reflexive & T is TopSpace-like ) ; :: thesis: T is with_compact_semilattices

then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ;

W is with_compact_semilattices

assume ( T is reflexive & T is TopSpace-like ) ; :: thesis: T is with_compact_semilattices

then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ;

W is with_compact_semilattices

proof

hence
T is with_compact_semilattices
; :: thesis: verum
let x be Point of W; :: according to WAYBEL30:def 3 :: thesis: ex J being basis of x st

for A being Subset of W st A in J holds

( subrelstr A is meet-inheriting & A is compact )

reconsider J = { the carrier of W} as basis of x by YELLOW13:21;

take J ; :: thesis: for A being Subset of W st A in J holds

( subrelstr A is meet-inheriting & A is compact )

let A be Subset of W; :: thesis: ( A in J implies ( subrelstr A is meet-inheriting & A is compact ) )

assume A8: A in J ; :: thesis: ( subrelstr A is meet-inheriting & A is compact )

subrelstr ([#] W) is infs-inheriting ;

then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A8, TARSKI:def 1;

K is meet-inheriting ;

hence subrelstr A is meet-inheriting ; :: thesis: A is compact

A = [#] W by A8, TARSKI:def 1;

hence A is compact ; :: thesis: verum

end;for A being Subset of W st A in J holds

( subrelstr A is meet-inheriting & A is compact )

reconsider J = { the carrier of W} as basis of x by YELLOW13:21;

take J ; :: thesis: for A being Subset of W st A in J holds

( subrelstr A is meet-inheriting & A is compact )

let A be Subset of W; :: thesis: ( A in J implies ( subrelstr A is meet-inheriting & A is compact ) )

assume A8: A in J ; :: thesis: ( subrelstr A is meet-inheriting & A is compact )

subrelstr ([#] W) is infs-inheriting ;

then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A8, TARSKI:def 1;

K is meet-inheriting ;

hence subrelstr A is meet-inheriting ; :: thesis: A is compact

A = [#] W by A8, TARSKI:def 1;

hence A is compact ; :: thesis: verum