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;
set f = incl SL,T;
set f9 = incl S,T;
A2: the carrier of S c= the carrier of T by YELLOW_0:def 13;
then A3: incl SL,T = id the carrier of SL by A1, YELLOW_9:def 1;
A4: incl S,T = id the carrier of SL by A1, A2, YELLOW_9:def 1;
A5: [#] SL is compact by COMPTS_1:10;
A6: incl S,T is infs-preserving by Th8;
RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T,the InternalRel of T #) ;
then A7: ( incl SL,T is infs-preserving & incl SL,T is directed-sups-preserving ) by A1, A3, A4, A6, Th6, Th10;
then incl SL,T is SemilatticeHomomorphism of SL,T by Th5;
then incl SL,T is continuous by A7, Th46;
then (incl SL,T) .: ([#] SL) is compact by A5, WEIERSTR:14;
then X is compact by A1, A3, FUNCT_1:162;
hence X is closed by COMPTS_1:16; :: thesis: verum