theorem Th39: :: STACKS_1:39

for X being StackAlgebra
for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )