:: deftheorem Def10 defines |` RELAT_1:def 12 :
for Y being set
for R, b<sub>3</sub> being Relation holds
( b<sub>3</sub> = Y |` R iff for x, y being object holds
( [x,y] in b₃ iff ( y in Y & [x,y] in R ) ) );