let A be partial non-empty UAStr ; :: thesis: LimDomRel A c= DomRel A
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in LimDomRel A or [x,y] in DomRel A )
assume A1: [x,y] in LimDomRel A ; :: thesis: [x,y] in DomRel A
then A2: x in the carrier of A by ZFMISC_1:87;
y in the carrier of A by A1, ZFMISC_1:87;
then [x,y] in (DomRel A) |^ (A,0) by A1, A2, Def7;
hence [x,y] in DomRel A by Th15; :: thesis: verum