set cTS = bool the carrier of TS;
defpred S1[ 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 S1[x,y] ) from 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 ;
hence ( len xi = 1 & T = xi -succ_of (xc,TS) ) by ; :: thesis: verum
end;
w in Lex E by ;
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