theorem Th9: :: POLNOT_1:9

for P being FinSequence-membered set holds
( {} in P * & P c= P * )