:: deftheorem Def12 defines push-non-empty STACKS_1:def 12 :
for X being non empty non void StackSystem holds
( X is push-non-empty iff for s being stack of X
for e being Element of X holds not emp push (e,s) );