:: deftheorem defines /\/ FILTER_1:def 3 :
for D being non empty set
for R being Equivalence_Relation of D
for u being UnOp of D st u is UnOp of D,R holds
for b₄ being UnOp of (Class R) holds
( b₄ = u /\/ R iff for x, y being set st x in Class R & y in x holds
b₄ . x = Class (R,(u . y)) );