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 \/ Z),W) >= kappa (Y,W)
let Y, Z, W be Subset of R; :: thesis: ( Y misses Z & Z c= W implies kappa ((Y \/ Z),W) >= kappa (Y,W) )
assume A0: ( Y misses Z & Z c= W ) ; :: thesis: kappa ((Y \/ Z),W) >= kappa (Y,W)

per cases ( Y <> {} or Y = {} ) ;

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

Y /\ W c= Y by XBOOLE_1:17;
then T2: (card (Y /\ W)) / (card Y) <= ((card (Y /\ W)) + (card Z)) / ((card Y) + (card Z)) by Lemacik, AA, NAT_1:43;
T4: (card Y) + (card Z) = card (Y \/ Z) by A0, CARD_2:40;
Z misses Y /\ W by A0, XBOOLE_1:63, XBOOLE_1:17;
then T3: (card (Y /\ W)) + (card Z) = card ((Y /\ W) \/ Z) by CARD_2:40;
T1: (Y \/ Z) /\ W = (Y /\ W) \/ (Z /\ W) by XBOOLE_1:23
.= (Y /\ W) \/ Z by A0, XBOOLE_1:28 ;
kappa (Y,W) <= (card ((Y /\ W) \/ Z)) / (card (Y \/ Z)) by T4, KappaDef, AA, T2, T3;
hence kappa ((Y \/ Z),W) >= kappa (Y,W) by KappaDef, AA, T1; :: thesis: verum

end;

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

then kappa ((Y \/ Z),W) = 1 by Prop1a, A0;
hence kappa ((Y \/ Z),W) >= kappa (Y,W) by XXREAL_1:1; :: thesis: verum

end;

end;