:: deftheorem Def6 defines Refinement YELLOW_9:def 6 :
for T1, T2 being TopStruct
for b₃ being TopSpace holds
( b₃ is Refinement of T1,T2 iff ( the carrier of b₃ = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b₃ ) );