let R be finite Approximation_Space; 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; for kap being RIF of R holds
( (CMap kap) . (X,Y) = 0 iff X c= Y )
let kap be RIF of R; ( (CMap kap) . (X,Y) = 0 iff X c= Y )
thus
( (CMap kap) . (X,Y) = 0 implies X c= Y )
( X c= Y implies (CMap kap) . (X,Y) = 0 )
assume
X c= Y
; (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
; verum