theorem Th5: :: STACKS_1:5

for X being StackAlgebra
for s being stack of X st emp s holds
|.s.| = {}