let R be finite Approximation_Space; :: thesis: for f being satisfying_RIF1 preRIF of R holds
( f is satisfying_RIF2 iff f is satisfying_RIF2* )
let f be satisfying_RIF1 preRIF of R; :: thesis: ( f is satisfying_RIF2 iff f is satisfying_RIF2* )
thus ( f is satisfying_RIF2 implies f is satisfying_RIF2* ) :: thesis: ( f is satisfying_RIF2* implies f is satisfying_RIF2 )

proof

assume A1: f is satisfying_RIF2 ; :: thesis: f is satisfying_RIF2*
let X, Y, Z be Subset of R; :: according to ROUGHIF1:def 13 :: thesis: ( f . (Y,Z) = 1 implies f . (X,Y) <= f . (X,Z) )
assume f . (Y,Z) = 1 ; :: thesis: f . (X,Y) <= f . (X,Z)
then Y c= Z by RIF1Def;
hence f . (X,Y) <= f . (X,Z) by A1; :: thesis: verum

end;

assume A2: f is satisfying_RIF2* ; :: thesis: f is satisfying_RIF2
let X, Y, Z be Subset of R; :: according to ROUGHIF1:def 8 :: thesis: ( Y c= Z implies f . (X,Y) <= f . (X,Z) )
assume Y c= Z ; :: thesis: f . (X,Y) <= f . (X,Z)
then f . (Y,Z) = 1 by RIF1Def;
hence f . (X,Y) <= f . (X,Z) by A2; :: thesis: verum