let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over 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 over 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 over 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 :: thesis: for x being object st x in (<%> E) -succ_of (S,TS) holds
x in S

let x be object ; :: 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 :: thesis: for x being object st x in S holds
x in (<%> E) -succ_of (S,TS)

let x be object ; :: 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