:: deftheorem Def16 defines ==_ STACKS_1:def 16 :
for X being StackAlgebra
for b₂ being Relation of the carrier' of X holds
( b₂ = ==_ X iff for s1, s2 being stack of X holds
( [s1,s2] in b₂ iff s1 == s2 ) );