:: deftheorem Def7 defines LimDomRel PUA2MSS1:def 7 :
for A being partial non-empty UAStr
for b₂ being Relation of the carrier of A holds
( b₂ = LimDomRel A iff for x, y being Element of A holds
( [x,y] in b₂ iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) );