theorem Th14: :: POLNOT_1:14

for P, Q being FinSequence-membered set
for n being Nat st Q c= P * holds
Q ^^ n c= P *