let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( (CMap (kappa R)) . (X,Y) = 0 iff X c= Y )
let X, Y be Subset of R; :: thesis: ( (CMap (kappa R)) . (X,Y) = 0 iff X c= Y )
thus ( (CMap (kappa R)) . (X,Y) = 0 implies X c= Y ) :: thesis: ( X c= Y implies (CMap (kappa R)) . (X,Y) = 0 )
proof
assume (CMap (kappa R)) . (X,Y) = 0 ; :: thesis: X c= Y
then 1 - ((kappa R) . (X,Y)) = 0 by CDef;
then kappa (X,Y) = 1 by ROUGHIF1:def 2;
hence X c= Y by ROUGHIF1:6; :: thesis: verum
end;
assume X c= Y ; :: thesis: (CMap (kappa R)) . (X,Y) = 0
then A1: kappa (X,Y) = 1 by ROUGHIF1:6;
(CMap (kappa R)) . (X,Y) = 1 - ((kappa R) . (X,Y)) by CDef
.= 1 - 1 by A1, ROUGHIF1:def 2 ;
hence (CMap (kappa R)) . (X,Y) = 0 ; :: thesis: verum