:: deftheorem Def8 defines pop-finite STACKS_1:def 8 :
for X being non empty non void StackSystem holds
( X is pop-finite iff for f being sequence of the carrier' of X ex i being Nat ex s being stack of X st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) );