let R be finite Approximation_Space; :: thesis: for Y, Z, W being Subset of R st Z misses W holds
kappa (Y,W) <= kappa ((Y \ Z),W)
let Y, Z, W be Subset of R; :: thesis: ( Z misses W implies kappa (Y,W) <= kappa ((Y \ Z),W) )
assume A0: Z misses W ; :: thesis: kappa (Y,W) <= kappa ((Y \ Z),W)

per cases ( Y /\ W <> {} or ( Y /\ W = {} & Y \/ Z <> {} & Y <> {} ) or ( Y /\ W = {} & Y \/ Z <> {} & Y = {} ) or ( Y /\ W = {} & Y \/ Z = {} ) ) ;

suppose S3: Y /\ W <> {} ; :: thesis: kappa (Y,W) <= kappa ((Y \ Z),W)

A1: Y <> {} by S3;

per cases ( Y c= Z or not Y c= Z ) ;

suppose Y c= Z ; :: thesis: kappa (Y,W) <= kappa ((Y \ Z),W)

then kappa ((Y \ Z),W) = 1 by KappaDef, XBOOLE_1:37;
hence kappa (Y,W) <= kappa ((Y \ Z),W) by XXREAL_1:1; :: thesis: verum

end;

suppose b1: not Y c= Z ; :: thesis: kappa (Y,W) <= kappa ((Y \ Z),W)

then B1: Y \ Z <> {} by XBOOLE_1:37;
B2: (Y \ Z) /\ W = (Y /\ W) \ (Z /\ W) by XBOOLE_1:111
.= Y /\ W by A0 ;
card (Y \ Z) <= card Y by NAT_1:43, XBOOLE_1:36;
then (card (Y /\ W)) / (card Y) <= (card (Y /\ W)) / (card (Y \ Z)) by XREAL_1:118, B1;
then kappa (Y,W) <= (card ((Y \ Z) /\ W)) / (card (Y \ Z)) by A1, KappaDef, B2;
hence kappa (Y,W) <= kappa ((Y \ Z),W) by KappaDef, b1, XBOOLE_1:37; :: thesis: verum

end;

end;

end;

suppose Z0: ( Y /\ W = {} & Y \/ Z <> {} & Y <> {} ) ; :: thesis: kappa (Y,W) <= kappa ((Y \ Z),W)

then Y misses W ;
then kappa (Y,W) = 0 by Z0, Prop2b;
hence kappa (Y,W) <= kappa ((Y \ Z),W) by XXREAL_1:1; :: thesis: verum

end;

suppose ( Y /\ W = {} & Y \/ Z <> {} & Y = {} ) ; :: thesis: kappa (Y,W) <= kappa ((Y \ Z),W)

hence kappa (Y,W) <= kappa ((Y \ Z),W) ; :: thesis: verum

end;

suppose ( Y /\ W = {} & Y \/ Z = {} ) ; :: thesis: kappa (Y,W) <= kappa ((Y \ Z),W)

then ( Y = {} & Z = {} ) ;
hence kappa (Y,W) <= kappa ((Y \ Z),W) ; :: thesis: verum

end;

end;