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 Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of S,TS = S
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F
for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of S,TS = S
let TS be non empty transition-system of F; :: thesis: for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of S,TS = S
let S be Subset of TS; :: thesis: ( not <%> E in rng (dom the Tran of TS) implies (<%> E) -succ_of S,TS = S )
assume A1: not <%> E in rng (dom the Tran of TS) ; :: thesis: (<%> E) -succ_of S,TS = S

A2: now

let x be set ; :: thesis: ( x in (<%> E) -succ_of S,TS implies x in S )
assume x in (<%> E) -succ_of S,TS ; :: thesis: x in S
then ex s being Element of TS st
( s in S & s, <%> E ==>* x,TS ) by Th103;
hence x in S by A1, Th100; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in S implies x in (<%> E) -succ_of S,TS )
assume A3: x in S ; :: thesis: x in (<%> E) -succ_of S,TS
x, <%> E ==>* x,TS by Th95;
hence x in (<%> E) -succ_of S,TS by A3; :: thesis: verum

end;

hence (<%> E) -succ_of S,TS = S by A2, TARSKI:2; :: thesis: verum