for X being StackAlgebra
for s, s1 being stack of X st s1 in coset s holds
core s1 = core s