theorem Th28: :: STACKS_1:28

for X being StackAlgebra
for s being stack of X st not emp s holds
core (pop s) = core s