theorem Th20: :: REWRITE3:20

for x1, x2, y1, y2 being object
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) by Th15;