:: deftheorem defines are_isomorphic BCIALG_6:def 9 :
for X, X9 being BCI-algebra holds
( X,X9 are_isomorphic iff ex f being BCI-homomorphism of X,X9 st f is bijective );