let T be non empty TopSpace; :: thesis: T, TopStruct(# the carrier of T, the topology of T #) are_homeomorphic
reconsider f = id T as Function of T,TopStruct(# the carrier of T, the topology of T #) ;
take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
thus dom f = [#] T ; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] TopStruct(# the carrier of T, the topology of T #) & f is one-to-one & f is continuous & f /" is continuous )
thus rng f = [#] T
.= [#] TopStruct(# the carrier of T, the topology of T #) ; :: thesis: ( f is one-to-one & f is continuous & f /" is continuous )
thus f is V14() ; :: thesis: ( f is continuous & f /" is continuous )
thus f is continuous by YELLOW12:36; :: thesis: f /" is continuous
thus f /" is continuous by YELLOW12:36; :: thesis: verum