theorem Th17: :: STACKS_1:17

for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
pop s1 == pop s2