:: deftheorem defines -->. REWRITE3:def 2 :
for X being set
for TS being transition-system over X
for x, y, z being object holds
( x,y -->. z,TS iff [[x,y],z] in the Tran of TS );