set S = the correct Scott TopAugmentation of R;
set T = the correct lower TopAugmentation of R;
A1: RelStr(# the carrier of the correct Scott TopAugmentation of R, the InternalRel of the correct Scott TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def 4;
set RR = the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R;
A2: the carrier of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R = the carrier of the correct Scott TopAugmentation of R \/ the carrier of the correct lower TopAugmentation of R by YELLOW_9:def 6;
A3: RelStr(# the carrier of the correct lower TopAugmentation of R, the InternalRel of the correct lower TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def 4;
then reconsider O = the topology of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R as Subset-Family of R by A2, A1;
set LL = TopRelStr(# the carrier of R, the InternalRel of R,O #);
RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,O #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,O #) #) = RelStr(# the carrier of R, the InternalRel of R #) ;
then reconsider LL = TopRelStr(# the carrier of R, the InternalRel of R,O #) as TopAugmentation of R by YELLOW_9:def 4;
TopStruct(# the carrier of LL, the topology of LL #) = TopStruct(# the carrier of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R, the topology of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R #) by A3, A1, A2;
then A4: LL is correct by TEX_2:7;
reconsider A = the topology of the correct Scott TopAugmentation of R \/ the topology of the correct lower TopAugmentation of R as prebasis of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by YELLOW_9:def 6;
reconsider A9 = A as Subset-Family of LL by A3, A1, A2;
take LL ; :: thesis: ( LL is Lawson & LL is strict & LL is correct )
FinMeetCl A is Basis of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by YELLOW_9:23;
then UniCl (FinMeetCl A) = O by YELLOW_9:22;
then FinMeetCl A9 is Basis of LL by A3, A1, A2, A4, YELLOW_9:22;
then the topology of the correct Scott TopAugmentation of R \/ the topology of the correct lower TopAugmentation of R is prebasis of LL by A4, YELLOW_9:23;
then LL is Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by A3, A1, A2, A4, YELLOW_9:def 6;
hence ( LL is Lawson & LL is strict & LL is correct ) by Th29; :: thesis: verum