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