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