let S be TopStruct ; :: thesis: S,S are_homeomorphic
take id S ; :: according to T_0TOPSP:def 1 :: thesis: id S is being_homeomorphism
thus id S is being_homeomorphism ; :: thesis: verum