let x, z, y be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega )
for TS being transition-system of 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 of 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 of F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
let TS be transition-system of F; :: thesis: ( not <%> E in rng (dom the Tran of TS) implies not x,z ==>. y,z,TS )
assume A: 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
C: ( v = z & x,w -->. y,TS & z = w ^ v ) by DefDir;
[[x,w],y] in the Tran of TS by C, DefProd;
then D: [x,w] in dom the Tran of TS by RELAT_1:20;
w = <%> E by C, FLANG_2:4;
hence contradiction by A, D, RELAT_1:20; :: thesis: verum