:: deftheorem Def11 defines pop-push STACKS_1:def 11 :
for X being non empty non void StackSystem holds
( X is pop-push iff for s being stack of X
for e being Element of X holds s = pop (push (e,s)) );