let A be partial non-empty UAStr ; :: thesis: for R being Relation of the carrier of A holds R |^ A c= R
let R be Relation of the carrier of A; :: thesis: R |^ A c= R
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R |^ A or [x,y] in R )
assume A1: [x,y] in R |^ A ; :: thesis: [x,y] in R
then A2: x in the carrier of A by ZFMISC_1:87;
y in the carrier of A by A1, ZFMISC_1:87;
hence [x,y] in R by A1, A2, Def5; :: thesis: verum