let R, S, T be TopStruct ; :: thesis: ( R is Refinement of S,T iff TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T )

hereby :: thesis: ( TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T implies R is Refinement of S,T )

assume A1: R is Refinement of S,T ; :: thesis: TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T
then reconsider R1 = R as TopSpace ;
the topology of S \/ the topology of T is prebasis of R by A1, YELLOW_9:def 6;
then A2: the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R1, the topology of R1 #) by Th33;
the carrier of TopStruct(# the carrier of R1, the topology of R1 #) = the carrier of S \/ the carrier of T by A1, YELLOW_9:def 6;
hence TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T by A2, YELLOW_9:def 6; :: thesis: verum

end;

assume A3: TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T ; :: thesis: R is Refinement of S,T
then reconsider R1 = R as TopSpace by TEX_2:7;
the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R, the topology of R #) by A3, YELLOW_9:def 6;
then A4: the topology of S \/ the topology of T is prebasis of R1 by Th33;
the carrier of R1 = the carrier of S \/ the carrier of T by A3, YELLOW_9:def 6;
hence R is Refinement of S,T by A4, YELLOW_9:def 6; :: thesis: verum