for R, Q being Relation st R c= Q holds
for p being RedSequence of R holds p is RedSequence of Q