:: deftheorem Def17 defines coset STACKS_1:def 17 :
for X being StackAlgebra
for s being stack of X
for b₃ being Subset of the carrier' of X holds
( b₃ = coset s iff ( s in b₃ & ( for e being Element of X
for s1 being stack of X st s1 in b₃ holds
( push (e,s1) in b₃ & ( not emp s1 implies pop s1 in b₃ ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
b₃ c= A ) ) );