let T be TopStruct ; :: thesis: T | ([#] T) = TopStruct(# the carrier of T,the topology of T #)
( TopStruct(# the carrier of T,the topology of T #) is strict SubSpace of T & the carrier of T = [#] TopStruct(# the carrier of T,the topology of T #) ) by Th2, PRE_TOPC:31;
hence T | ([#] T) = TopStruct(# the carrier of T,the topology of T #) by PRE_TOPC:def 10; :: thesis: verum