let X be StackAlgebra; :: thesis: for s being stack of X holds core s in coset s
let s be stack of X; :: thesis: core s in coset s
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A1: ( t . 1 = s & t . (len t) = core s ) and
for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) by Def19;
ConstructionRed X reduces s, core s by A1;
then core s in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ;
hence core s in coset s by Th25; :: thesis: verum