theorem Th7: :: STACKS_1:7

for X being StackAlgebra
for s being stack of X st not emp s holds
|.(pop s).| = Del (|.s.|,1)