consider T being correct lower TopAugmentation of R;
consider S being correct Scott TopAugmentation of R;
A1: ( RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R,the InternalRel of R #) ) by YELLOW_9:def 4;
consider RR being Refinement of S,T;
A2: the carrier of RR = the carrier of S \/ the carrier of T by YELLOW_9:def 6;
then reconsider O = the topology of RR as Subset-Family of R by 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;
take LL ; :: thesis: ( LL is Lawson & LL is strict & LL is TopSpace-like )
TopStruct(# the carrier of LL,the topology of LL #) = TopStruct(# the carrier of RR,the topology of RR #) by A1, A2;
then A3: LL is TopSpace-like by TEX_2:12;
reconsider A = the topology of S \/ the topology of T as prebasis of RR by YELLOW_9:def 6;
reconsider A' = A as Subset-Family of LL by A1, A2;
FinMeetCl A is Basis of RR by YELLOW_9:23;
then UniCl (FinMeetCl A) = O by YELLOW_9:22;
then FinMeetCl A' is Basis of LL by A1, A2, A3, YELLOW_9:22;
then the topology of S \/ the topology of T is prebasis of LL by A3, YELLOW_9:23;
then LL is Refinement of S,T by A1, A2, A3, YELLOW_9:def 6;
hence ( LL is Lawson & LL is strict & LL is TopSpace-like ) by Th29; :: thesis: verum