:: deftheorem Defff defines ff_0 ROUGHS_5:def 5 :
for R being non empty RelStr
for f being Function of the carrier of R,(bool the carrier of R)
for b₃ being map of R holds
( b₃ = ff_0 f iff for x being Subset of R holds b₃ . x = { u where u is Element of R : f . u meets x } );