let X be set ; :: thesis: for E being non empty set
for w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
let E be non empty set ; :: thesis: for w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
let w be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
let TS be non empty transition-system over F; :: thesis: for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
let S be Subset of TS; :: thesis: ( len w = 1 implies ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) )
assume A1: len w = 1 ; :: thesis: ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
thus ( X = w -succ_of (S,TS) implies S,w ==>* X, _bool TS ) :: thesis: ( S,w ==>* X, _bool TS implies X = w -succ_of (S,TS) )

proof

assume X = w -succ_of (S,TS) ; :: thesis: S,w ==>* X, _bool TS
then [[S,w],X] in the Tran of (_bool TS) by A1, Def1;
then S,w -->. X, _bool TS by REWRITE3:def 2;
then S,w ==>. X, <%> E, _bool TS by REWRITE3:23;
then S,w ==>* X, <%> E, _bool TS by REWRITE3:87;
hence S,w ==>* X, _bool TS by REWRITE3:def 7; :: thesis: verum

end;

assume S,w ==>* X, _bool TS ; :: thesis: X = w -succ_of (S,TS)
then A2: S,w ==>* X, <%> E, _bool TS by REWRITE3:def 7;
ex e being Element of E st
( w = <%e%> & w . 0 = e ) by A1, Th4;
then S,w ^ {} ==>. X, <%> E, _bool TS by A2, Th12;
then A3: S,w -->. X, _bool TS by REWRITE3:24;
then X in _bool TS by REWRITE3:15;
then X in the carrier of (_bool TS) ;
then reconsider X9 = X as Subset of TS by Def1;
[[S,w],X9] in the Tran of (_bool TS) by A3, REWRITE3:def 2;
hence X = w -succ_of (S,TS) by Def1; :: thesis: verum