:: deftheorem defines reduces REWRITE1:def 3 :
for R being Relation
for a, b being object holds
( R reduces a,b iff ex p being RedSequence of R st
( p . 1 = a & p . (len p) = b ) );