:: deftheorem Def1 defines UnOp FILTER_1:def 1 :
for D being non empty set
for R being Relation
for b₃ being UnOp of D holds
( b₃ is UnOp of D,R iff for x, y being Element of D st [x,y] in R holds
[(b₃ . x),(b₃ . y)] in R );