:: deftheorem Def18 defines ConstructionRed STACKS_1:def 18 :
for X being StackAlgebra
for b₂ being Relation of the carrier' of X holds
( b₂ = ConstructionRed X iff for s1, s2 being stack of X holds
( [s1,s2] in b₂ iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) );