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