theorem :: STACKS_1:21

for X being StackAlgebra
for s being stack of X
for e being Element of X holds
( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )