theorem :: PUA2MSS1:25

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