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 ;
TopStruct(# the carrier of R1,the topology of R1 #) is Refinement of S,T

proof

thus 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; :: according to YELLOW_9:def 6 :: thesis: the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R1,the topology of R1 #)
the topology of S \/ the topology of T is prebasis of R by A1, YELLOW_9:def 6;
hence the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R1,the topology of R1 #) by Th33; :: thesis: verum

end;

hence TopStruct(# the carrier of R,the topology of R #) is Refinement of S,T ; :: thesis: verum

end;

assume A2: 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:12;
R1 is Refinement of S,T

proof

thus the carrier of R1 = the carrier of S \/ the carrier of T by A2, YELLOW_9:def 6; :: according to YELLOW_9:def 6 :: thesis: the topology of S \/ the topology of T is prebasis of R1
the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R,the topology of R #) by A2, YELLOW_9:def 6;
hence the topology of S \/ the topology of T is prebasis of R1 by Th33; :: thesis: verum

end;

hence R is Refinement of S,T ; :: thesis: verum