theorem Th26: :: PUA2MSS1:27

for A being partial non-empty UAStr
for P being a_partition of A holds P is_finer_than Class (LimDomRel A)