for P, Q, R being FinSequence-membered set st P c= R * & Q c= R * holds
P ^ Q c= R *