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;