for X being StackAlgebra
for s being stack of X ex s1 being stack of X st
( emp s1 & s1 in coset s )