take id T ; :: thesis: id T is being_homeomorphism
thus id T is being_homeomorphism by Th20; :: thesis: verum