:: deftheorem Def11 defines .: RELAT_1:def 13 :
for R being Relation
for X, b₃ being set holds
( b₃ = R .: X iff for y being object holds
( y in b₃ iff ex x being object st
( [x,y] in R & x in X ) ) );