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:10;
hence T | ([#] T) = TopStruct(# the carrier of T, the topology of T #) by PRE_TOPC:def 5; :: thesis: verum