let x be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega )
for TS being non empty transition-system of 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 of 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 of 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 of 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 A: 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 set such that
B: x = [y,z] by RELAT_1:def 1;
consider s being Element of TS, v being Element of E ^omega , t being Element of TS, w being Element of E ^omega such that
C: ( y = [s,v] & z = [t,w] ) by A, B, ThRel10;
thus ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] by B, C; :: thesis: verum