let R be finite Approximation_Space; :: thesis: for f being preRIF of R holds CMap (CMap f) = f
let f be preRIF of R; :: thesis: CMap (CMap f) = f
set g = CMap f;
for x being Element of [:(bool the carrier of R),(bool the carrier of R):] holds (CMap (CMap f)) . x = f . x

proof

let x be Element of [:(bool the carrier of R),(bool the carrier of R):]; :: thesis: (CMap (CMap f)) . x = f . x
reconsider x1 = x `1 , x2 = x `2 as Subset of R ;
(CMap (CMap f)) . x = (CMap (CMap f)) . (x1,x2) by MCART_1:21
.= 1 - ((CMap f) . (x1,x2)) by CDef
.= 1 - (1 - (f . (x1,x2))) by CDef
.= f . x by MCART_1:21 ;
hence (CMap (CMap f)) . x = f . x ; :: thesis: verum

end;

hence CMap (CMap f) = f ; :: thesis: verum