:: deftheorem defines are_isomorphic STACKS_1:def 22 :
for X1, X2 being StackAlgebra holds
( X1,X2 are_isomorphic iff ex F, G being Function st F,G form_isomorphism_between X1,X2 );