theorem Th9: :: REWRITE1:9
for R being Relation
for p being RedSequence of R holds Rev p is RedSequence of R ~