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
; ( 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; verum