:: deftheorem Def12 defines " RELAT_1:def 14 :
for R being Relation
for Y, b₃ being set holds
( b₃ = R " Y iff for x being object holds
( x in b₃ iff ex y being object st
( [x,y] in R & y in Y ) ) );