theorem Th12: :: STACKS_1:12

for X being StackAlgebra
for x being Element of the carrier of X * ex s being stack of X st |.s.| = x