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
A1: 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 over 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 A2: [[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:87;
[xc,T] in tTS by A2;
hence ( len w = 1 & T = w -succ_of (S,TS) ) by A1; :: thesis: verum

end;

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

A5: now :: thesis: for xc being Element of bool the carrier of TS
for xi being Element of E ^omega st [S,w] = [xc,xi] holds
( len xi = 1 & T = xi -succ_of (xc,TS) )

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 A6: [S,w] = [xc,xi] ; :: thesis: ( len xi = 1 & T = xi -succ_of (xc,TS) )
xc = S by A6, XTUPLE_0:1;
hence ( len xi = 1 & T = xi -succ_of (xc,TS) ) by A3, A4, A6, XTUPLE_0:1; :: thesis: verum

end;

w in Lex E by A3, Th9;
then reconsider x = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87;
[x,T] in tTS by A1, A5;
hence [[S,w],T] in the Tran of bTS ; :: thesis: verum