let T be continuous complete Lawson TopLattice; :: thesis: for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T ex X being Subset of T st
( X = the carrier of S & X is closed )
let S be non empty full infs-inheriting directed-sups-inheriting SubRelStr of T; :: thesis: ex X being Subset of T st
( X = the carrier of S & X is closed )
reconsider X = the carrier of S as Subset of T by YELLOW_0:def 13;
take X ; :: thesis: ( X = the carrier of S & X is closed )
thus X = the carrier of S ; :: thesis: X is closed
reconsider S = S as complete CLSubFrame of T by Th18;
consider SL being correct Lawson TopAugmentation of S;
A1: RelStr(# the carrier of SL,the InternalRel of SL #) = RelStr(# the carrier of S,the InternalRel of S #) by YELLOW_9:def 4;
then A2: [#] SL = X ;
set f = incl SL,T;
set f' = incl S,T;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then A3: ( incl SL,T = id the carrier of SL & incl S,T = id the carrier of SL ) by A1, YELLOW_9:def 1;
A4: [#] SL is compact by COMPTS_1:10;
( incl S,T is infs-preserving & incl S,T is directed-sups-preserving & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T,the InternalRel of T #) ) by Th8, Th10;
then A5: ( incl SL,T is infs-preserving & incl SL,T is directed-sups-preserving ) by A1, A3, Th6;
then incl SL,T is SemilatticeHomomorphism of SL,T by Th5;
then incl SL,T is continuous by A5, Th46;
then (incl SL,T) .: ([#] SL) is compact by A4, WEIERSTR:14;
then X is compact by A2, A3, FUNCT_1:162;
hence X is closed by COMPTS_1:16; :: thesis: verum