:: deftheorem CDef defines CMap ROUGHIF2:def 1 :
for R being finite Approximation_Space
for f, b₃ being preRIF of R holds
( b₃ = CMap f iff for x, y being Subset of R holds b₃ . (x,y) = 1 - (f . (x,y)) );