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