for R being finite Approximation_Space
for f being satisfying_RIF1 preRIF of R holds
( f is satisfying_RIF2 iff f is satisfying_RIF2* )