let T be continuous complete Lawson TopLattice; 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; 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
; ( X = the carrier of S & X is closed )
thus
X = the carrier of S
; 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; verum