let LL be non empty RelStr ; :: thesis:
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 set ; :: according to TARSKI:def 3 :: thesis:
assume a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis:
then ex x being Element of LL st a = (uparrow x) ` ;
hence a in bool the carrier of LL ; :: thesis:

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

proof

thus the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) by A1, PRE_TOPC:def 1; :: according to PRE_TOPC:def 1 :: thesis:

hereby :: thesis:

let a be Subset-Family of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #); :: thesis:
reconsider b = a as Subset-Family of S ;
assume a c= the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; :: thesis:
then union b in the topology of S by PRE_TOPC:def 1;
hence union a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; :: thesis:

end;

let a, b be Subset of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #); :: thesis:
assume that
A2: a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) and
A3: b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; :: thesis:
a /\ b in the topology of S by A2, A3, PRE_TOPC:def 1;
hence a /\ b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; :: thesis:

end;

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:
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:
A4: A is prebasis of S by CANTOR_1:18;
then consider F being Basis of S such that
A5: F c= FinMeetCl A by CANTOR_1:def 4;
A6: the topology of T c= UniCl F by CANTOR_1:def 2;
F c= the topology of T by TOPS_2:64;
then A7: F is Basis of T by A6, 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 A8: A = { ((uparrow x) `) where x is Element of T : verum } by Lm1;
A c= the topology of S by A4, TOPS_2:64;
hence { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A7, A5, A8, CANTOR_1:def 4, TOPS_2:64; :: according to WAYBEL19:def 1 :: thesis: