:: deftheorem defines == STACKS_1:def 14 :
for X being StackAlgebra
for s1, s2 being stack of X holds
( s1 == s2 iff |.s1.| = |.s2.| );