:: deftheorem defines pop STACKS_1:def 4 :
for X being non void StackSystem
for s being stack of X holds pop s = the s_pop of X . s;