:: deftheorem Def9 defines | RELAT_1:def 11 :
for R being Relation
for X being set
for b₃ being Relation holds
( b₃ = R | X iff for x, y being object holds
( [x,y] in b₃ iff ( x in X & [x,y] in R ) ) );