let X be StackAlgebra; :: thesis: for s, s1 being stack of X st s1 in coset s holds
core s1 = core s
let s, s1 be stack of X; :: thesis: ( s1 in coset s implies core s1 = core s )
assume A1: s1 in coset s ; :: thesis: core s1 = core s
set R = ConstructionRed X;
defpred S₁[ stack of X] means core $1 = core s;
A2: S₁[s] ;
coset s = { s2 where s2 is stack of X : ConstructionRed X reduces s,s2 } by Th25;
then ex s2 being stack of X st
( s1 = s2 & ConstructionRed X reduces s,s2 ) by A1;
then A3: ConstructionRed X reduces s,s1 ;

A4: now :: thesis: for x, y being stack of X st ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S₁[x] holds
S₁[y]

let x, y be stack of X; :: thesis: ( ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S₁[x] implies S₁[y] )
assume A5: ( ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S₁[x] ) ; :: thesis: S₁[y]
then ( ( not emp x & y = pop x ) or ex e being Element of X st y = push (e,x) ) by Def18;
hence S₁[y] by A5, Th27, Th28; :: thesis: verum

end;

thus S₁[s1] from STACKS_1:sch 6(A2, A3, A4); :: thesis: verum