let x, y, z be object ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
let F be Subset of (E ^omega); :: thesis: for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
let TS be transition-system over F; :: thesis: ( not <%> E in rng (dom the Tran of TS) implies not x,z ==>. y,z,TS )
assume A1: not <%> E in rng (dom the Tran of TS) ; :: thesis: not x,z ==>. y,z,TS
assume x,z ==>. y,z,TS ; :: thesis: contradiction
then consider v, w being Element of E ^omega such that
A2: v = z and
A3: x,w -->. y,TS and
A4: z = w ^ v ;
[[x,w],y] in the Tran of TS by A3;
then A5: [x,w] in dom the Tran of TS by XTUPLE_0:def 12;
w = <%> E by A2, A4, FLANG_2:4;
hence contradiction by A1, A5, XTUPLE_0:def 13; :: thesis: verum