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 s9 being Element of TS st
( s9 = s & ex t being Element of TS st
( t in X & t,x ==>* s9,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