:: deftheorem Def5 defines TopExtension YELLOW_9:def 5 :
for T being TopStruct
for b₂ being TopSpace holds
( b₂ is TopExtension of T iff ( the carrier of T = the carrier of b₂ & the topology of T c= the topology of b₂ ) );