theorem Th6: :: REWRITE1:6

for R being Relation
for a being object holds <*a*> is RedSequence of R