let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R
for kap being RIF of R holds
( (CMap kap) . (X,Y) = 0 iff X c= Y )
let X, Y be Subset of R; :: thesis: for kap being RIF of R holds
( (CMap kap) . (X,Y) = 0 iff X c= Y )
let kap be RIF of R; :: thesis: ( (CMap kap) . (X,Y) = 0 iff X c= Y )
thus ( (CMap kap) . (X,Y) = 0 implies X c= Y ) :: thesis: ( X c= Y implies (CMap kap) . (X,Y) = 0 )

proof

assume (CMap kap) . (X,Y) = 0 ; :: thesis: X c= Y
then 1 - (kap . (X,Y)) = 0 by CDef;
hence X c= Y by ROUGHIF1:def 7; :: thesis: verum

end;

assume X c= Y ; :: thesis: (CMap kap) . (X,Y) = 0
then A1: kap . (X,Y) = 1 by ROUGHIF1:def 7;
(CMap kap) . (X,Y) = 1 - 1 by A1, CDef;
hence (CMap kap) . (X,Y) = 0 ; :: thesis: verum