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
proof
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;
hence T is with_compact_semilattices ; :: thesis: verum