theorem Lem5: :: BAGORD_2:22

for I being non empty set
for R being Relation of I
for r being RedSequence of R st len r > 1 holds
r . (len r) in I