theorem Th25: :: STACKS_1:25
for X being StackAlgebra
for s being stack of X holds coset s = { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 }