:: deftheorem defines are_Iso AFVECT0:def 10 :
for X, Y being non empty addLoopStr holds
( X,Y are_Iso iff ex f being Function of the carrier of X, the carrier of Y st f is_Iso_of X,Y );