:: deftheorem Def15 defines proper-for-identity STACKS_1:def 15 :
for X being StackAlgebra holds
( X is proper-for-identity iff for s1, s2 being stack of X st s1 == s2 holds
s1 = s2 );