set cTS = bool the carrier of TS;
defpred S₁[ set , set ] means for c being Element of bool the carrier of TS
for i being Element of E ^omega st $1 = [c,i] holds
( len i = 1 & $2 = i -succ_of c,TS );
consider tTS being Relation of [:(bool the carrier of TS),(Lex E):],(bool the carrier of TS) such that
A: for x being Element of [:(bool the carrier of TS),(Lex E):]
for y being Element of bool the carrier of TS holds
( [x,y] in tTS iff S₁[x,y] ) from RELSET_1:sch 2();
set bTS = transition-system(# (bool the carrier of TS),tTS #);
reconsider bTS = transition-system(# (bool the carrier of TS),tTS #) as strict transition-system of Lex E ;
take bTS ; :: thesis: ( the carrier of bTS = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of S,TS ) ) ) )
thus the carrier of bTS = bool the carrier of TS ; :: thesis: for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of S,TS ) )
let S be Subset of TS; :: thesis: for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of S,TS ) )
let w be Element of E ^omega ; :: thesis: for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of S,TS ) )
let T be Subset of TS; :: thesis: ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of S,TS ) )
thus ( [[S,w],T] in the Tran of bTS implies ( len w = 1 & T = w -succ_of S,TS ) ) :: thesis: ( len w = 1 & T = w -succ_of S,TS implies [[S,w],T] in the Tran of bTS )

proof

assume D: [[S,w],T] in the Tran of bTS ; :: thesis: ( len w = 1 & T = w -succ_of S,TS )
then reconsider xc = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:106;
[xc,T] in tTS by D;
hence ( len w = 1 & T = w -succ_of S,TS ) by A; :: thesis: verum

end;

assume B: ( len w = 1 & T = w -succ_of S,TS ) ; :: thesis: [[S,w],T] in the Tran of bTS
set x = [S,w];

D: now

let xc be Element of bool the carrier of TS; :: thesis: for xi being Element of E ^omega st [S,w] = [xc,xi] holds
( len xi = 1 & T = xi -succ_of xc,TS )
let xi be Element of E ^omega ; :: thesis: ( [S,w] = [xc,xi] implies ( len xi = 1 & T = xi -succ_of xc,TS ) )
assume C: [S,w] = [xc,xi] ; :: thesis: ( len xi = 1 & T = xi -succ_of xc,TS )
( xc = S & xi = w ) by C, ZFMISC_1:33;
hence ( len xi = 1 & T = xi -succ_of xc,TS ) by B; :: thesis: verum

end;

w in Lex E by B, ThLex20;
then reconsider x = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:106;
[x,T] in tTS by A, D;
hence [[S,w],T] in the Tran of bTS ; :: thesis: verum