theorem :: REWRITE3:16

for x, y, z being object
for X1, X2 being set
for TS1 being transition-system over X1
for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds
x,y -->. z,TS2 ;