theorem Th30: :: STACKS_1:30

for X being StackAlgebra
for s being stack of X
for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s )