let LL be non empty RelStr ; :: thesis: ex T being correct strict TopAugmentation of LL st T is lower
set A = { ((uparrow x) `) where x is Element of LL : verum } ;
{ ((uparrow x) `) where x is Element of LL : verum } c= bool the carrier of LL

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) `) where x is Element of LL : verum } or a in bool the carrier of LL )
assume a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis: a in bool the carrier of LL
then ex x being Element of LL st a = (uparrow x) ` ;
hence a in bool the carrier of LL ; :: thesis: verum

end;

then reconsider A = { ((uparrow x) `) where x is Element of LL : verum } as Subset-Family of LL ;
set T = TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #);
reconsider S = TopStruct(# the carrier of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace by CANTOR_1:15;
A1: TopStruct(# the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #), the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) #) = S ;
TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) is TopSpace-like by A1, PRE_TOPC:def 1;
then reconsider T = TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace-like strict TopRelStr ;
take T ; :: thesis: ( T is correct strict TopAugmentation of LL & T is lower )
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of LL, the InternalRel of LL #) ;
hence T is correct strict TopAugmentation of LL by YELLOW_9:def 4; :: thesis: T is lower
A2: A is prebasis of S by CANTOR_1:18;
then consider F being Basis of S such that
A3: F c= FinMeetCl A by CANTOR_1:def 4;
A4: the topology of T c= UniCl F by CANTOR_1:def 2;
F c= the topology of T by TOPS_2:64;
then A5: F is Basis of T by A4, CANTOR_1:def 2, TOPS_2:64;
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of LL, the InternalRel of LL #) ;
then A6: A = { ((uparrow x) `) where x is Element of T : verum } by Lm1;
A c= the topology of S by A2, TOPS_2:64;
hence { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A5, A3, A6, CANTOR_1:def 4, TOPS_2:64; :: according to WAYBEL19:def 1 :: thesis: verum