let x, X be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega )
for TS being non empty transition-system of F
for s being Element of TS holds
( s in x -succ_of X,TS iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F
for s being Element of TS holds
( s in x -succ_of X,TS iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F
for s being Element of TS holds
( s in x -succ_of X,TS iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let TS be non empty transition-system of F; :: thesis: for s being Element of TS holds
( s in x -succ_of X,TS iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let s be Element of TS; :: thesis: ( s in x -succ_of X,TS iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
thus ( s in x -succ_of X,TS implies ex t being Element of TS st
( t in X & t,x ==>* s,TS ) ) :: thesis: ( ex t being Element of TS st
( t in X & t,x ==>* s,TS ) implies s in x -succ_of X,TS )

proof

assume s in x -succ_of X,TS ; :: thesis: ex t being Element of TS st
( t in X & t,x ==>* s,TS )
then ex s' being Element of TS st
( s' = s & ex t being Element of TS st
( t in X & t,x ==>* s',TS ) ) ;
hence ex t being Element of TS st
( t in X & t,x ==>* s,TS ) ; :: thesis: verum

end;

thus ( ex t being Element of TS st
( t in X & t,x ==>* s,TS ) implies s in x -succ_of X,TS ) ; :: thesis: verum