:: deftheorem defines emp STACKS_1:def 3 :
for X being StackSystem
for s being stack of X holds
( emp s iff s in the s_empty of X );