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 S1[ stack of X] means core $1 = core s;
A2: S1[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 & S1[x] holds
S1[y]
let x, y be stack of X; :: thesis: ( ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S1[x] implies S1[y] )
assume A5: ( ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S1[x] ) ; :: thesis: S1[y]
then ( ( not emp x & y = pop x ) or ex e being Element of X st y = push (e,x) ) by Def18;
hence S1[y] by A5, Th27, Th28; :: thesis: verum
end;
thus S1[s1] from STACKS_1:sch 6(A2, A3, A4); :: thesis: verum