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

W3: now

let x, y be stack of X; :: thesis: ( ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S₁[x] implies S₁[y] )
assume A2: ( 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 CRED;
hence S₁[y] by A2, Th12, Th13; :: thesis: verum

end;

thus S₁[s1] from STACKS_1:sch 6(W1, W2, W3); :: thesis: verum