:: deftheorem defines push STACKS_1:def 6 :
for X being non empty non void StackSystem
for s being stack of X
for e being Element of X holds push (e,s) = the s_push of X . (e,s);