let x, y be object ; 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, <%> E -->. y,TS
let E be 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, <%> E -->. y,TS
let F be Subset of (E ^omega); for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x, <%> E -->. y,TS
let TS be transition-system over F; ( not <%> E in rng (dom the Tran of TS) implies not x, <%> E -->. y,TS )
assume A1:
not <%> E in rng (dom the Tran of TS)
; not x, <%> E -->. y,TS
assume
x, <%> E -->. y,TS
; contradiction
then
[[x,(<%> E)],y] in the Tran of TS
;
then
[x,(<%> E)] in dom the Tran of TS
by XTUPLE_0:def 12;
hence
contradiction
by A1, XTUPLE_0:def 13; verum