:: deftheorem Def1 defines .: RELSET_2:def 1 :
for A being set
for R being Relation
for b₃ being Function holds
( b₃ = .: (R,A) iff ( dom b₃ = bool A & ( for X being set st X c= A holds
b₃ . X = R .: X ) ) );