:: deftheorem Def9 defines push-pop STACKS_1:def 9 :
for X being non empty non void StackSystem holds
( X is push-pop iff for s being stack of X st not emp s holds
s = push ((top s),(pop s)) );