let R be finite Approximation_Space; :: thesis: for Y, Z, W being Subset of R st Y misses Z & Z c= W holds
kappa (Y,W) >= kappa ((Y \ Z),W)
let Y, Z, W be Subset of R; :: thesis: ( Y misses Z & Z c= W implies kappa (Y,W) >= kappa ((Y \ Z),W) )
assume A0: ( Y misses Z & Z c= W ) ; :: thesis: kappa (Y,W) >= kappa ((Y \ Z),W)
per cases ( Y <> {} or Y = {} ) ;
suppose Y <> {} ; :: thesis: kappa (Y,W) >= kappa ((Y \ Z),W)
thus kappa (Y,W) >= kappa ((Y \ Z),W) by A0, XBOOLE_1:83; :: thesis: verum
end;
suppose Y = {} ; :: thesis: kappa (Y,W) >= kappa ((Y \ Z),W)
hence kappa (Y,W) >= kappa ((Y \ Z),W) ; :: thesis: verum
end;
end;