for R, S, T being TopStruct holds
( R is Refinement of S,T iff TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T )