consider R being Refinement of S,T;
set R1 = TopStruct(# the carrier of R, the topology of R #);
the topology of S \/ the topology of T is prebasis of R by YELLOW_9:def 6;
then ( the carrier of TopStruct(# the carrier of R, the topology of R #) = the carrier of S \/ the carrier of T & the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R, the topology of R #) ) by Th33, YELLOW_9:def 6;
then reconsider R1 = TopStruct(# the carrier of R, the topology of R #) as Refinement of S,T by YELLOW_9:def 6;
take R1 ; :: thesis: R1 is strict
thus R1 is strict ; :: thesis: verum