let x be object ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
let TS be non empty transition-system over F; :: thesis: ( x in ==>.-relation TS implies ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] )
assume A1: x in ==>.-relation TS ; :: thesis: ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
then consider y, z being object such that
A2: x = [y,z] by RELAT_1:def 1;
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( y = [s,v] & z = [t,w] ) by A1, A2, Th31;
hence ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] by A2; :: thesis: verum