let A be partial non-empty UAStr ; :: thesis: LimDomRel A c= DomRel A
let x, y be set ; :: 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:106;
y in the carrier of A by A1, ZFMISC_1:106;
then [x,y] in (DomRel A) |^ A,0 by A1, A2, Def8;
hence [x,y] in DomRel A by Th17; :: thesis: verum