theorem Th15: :: REWRITE3:15

for x, y, z being object
for X being set
for TS being transition-system over X st x,y -->. z,TS holds
( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )