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