:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def 3 :
for S, T being TopStruct st S,T are_homeomorphic holds
for b₃ being Function of S,T holds
( b₃ is Homeomorphism of S,T iff b₃ is being_homeomorphism );