theorem Th9: :: STACKS_1:9

for X being StackAlgebra
for s being stack of X st not emp s holds
top s = |.s.| . 1