for R being Approximation_Space
for x being Subset of R holds (f_0 R) . x is exact