:: deftheorem Def4 defines Homeomorphism TOPGRP_1:def 4 :
for T being TopStruct
for b₂ being Function of T,T holds
( b₂ is Homeomorphism of T iff b₂ is being_homeomorphism );