theorem Th7: :: REWRITE1:7

for R being Relation
for a, b being object st [a,b] in R holds
<*a,b*> is RedSequence of R