let T be TopStruct ; :: thesis: the carrier of T = the carrier of (Omega T)
TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
hence the carrier of T = the carrier of (Omega T) ; :: thesis: verum