for R being Relation
for P being RedSequence of R
for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds
( q1 is RedSequence of R & q2 is RedSequence of R )