for X being non empty set
for R being Relation of X
for r being RedSequence of R st r . 1 in X holds
r is FinSequence of X