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