let N be complete Lawson TopLattice; :: thesis: for T being complete LATTICE
for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of T,the InternalRel of T #) holds
TopRelStr(# the carrier of A,the InternalRel of A,the topology of A #) = TopRelStr(# the carrier of N,the InternalRel of N,the topology of N #)
let T be complete LATTICE; :: thesis: for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of T,the InternalRel of T #) holds
TopRelStr(# the carrier of A,the InternalRel of A,the topology of A #) = TopRelStr(# the carrier of N,the InternalRel of N,the topology of N #)
let A be correct Lawson TopAugmentation of T; :: thesis: ( RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of T,the InternalRel of T #) implies TopRelStr(# the carrier of A,the InternalRel of A,the topology of A #) = TopRelStr(# the carrier of N,the InternalRel of N,the topology of N #) )
assume A1: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of T,the InternalRel of T #) ; :: thesis: TopRelStr(# the carrier of A,the InternalRel of A,the topology of A #) = TopRelStr(# the carrier of N,the InternalRel of N,the topology of N #)
A2: RelStr(# the carrier of A,the InternalRel of A #) = RelStr(# the carrier of N,the InternalRel of N #) by A1, YELLOW_9:def 4;
consider l being correct lower TopAugmentation of T;
consider S being correct Scott TopAugmentation of T;
A3: ( the topology of l = omega T & the topology of S = sigma T ) by WAYBEL19:def 2, YELLOW_9:51;
A4: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & RelStr(# the carrier of l,the InternalRel of l #) = RelStr(# the carrier of T,the InternalRel of T #) ) by YELLOW_9:def 4;
A5: N is Refinement of S,l

proof

thus the carrier of N = the carrier of S \/ the carrier of l by A1, A4; :: according to YELLOW_9:def 6 :: thesis: the topology of S \/ the topology of l is prebasis of N
(sigma N) \/ (omega N) is prebasis of N by WAYBEL19:def 3;
then (sigma T) \/ (omega N) is prebasis of N by A1, YELLOW_9:52;
hence the topology of S \/ the topology of l is prebasis of N by A1, A3, WAYBEL19:3; :: thesis: verum

end;

the topology of S \/ the topology of l c= bool the carrier of N

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the topology of S \/ the topology of l or a in bool the carrier of N )
assume a in the topology of S \/ the topology of l ; :: thesis: a in bool the carrier of N
then ( a in the topology of S or a in the topology of l ) by XBOOLE_0:def 3;
hence a in bool the carrier of N by A1, A4; :: thesis: verum

end;

then reconsider X = the topology of S \/ the topology of l as Subset-Family of N ;
reconsider X = X as Subset-Family of N ;
the topology of N = UniCl (FinMeetCl X) by A5, YELLOW_9:56
.= lambda T by A1, A3, WAYBEL19:33
.= the topology of A by WAYBEL19:def 4 ;
hence TopRelStr(# the carrier of A,the InternalRel of A,the topology of A #) = TopRelStr(# the carrier of N,the InternalRel of N,the topology of N #) by A2; :: thesis: verum