:: deftheorem Def20 defines /== STACKS_1:def 20 :
for X being StackAlgebra
for b₂ being strict StackSystem holds
( b₂ = X /== iff ( the carrier of b₂ = the carrier of X & the carrier' of b₂ = Class (==_ X) & the s_empty of b₂ = { the s_empty of X} & the s_push of b₂ = the s_push of X /\/ (==_ X) & the s_pop of b₂ = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of (Class (==_ X)) holds the s_top of b₂ = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) ) );