theorem Th3: :: PUA2MSS1:4

for X, Y being set st X is_finer_than Y holds
for p being FinSequence of X ex q being FinSequence of Y st product p c= product q