let R be finite Approximation_Space; :: thesis: for Y, Z, W being Subset of R st Z misses W holds
kappa ((Y \/ Z),W) <= kappa (Y,W)
let Y, Z, W be Subset of R; :: thesis: ( Z misses W implies kappa ((Y \/ Z),W) <= kappa (Y,W) )
assume A0: Z misses W ; :: thesis: kappa ((Y \/ Z),W) <= kappa (Y,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 \/ Z),W) <= kappa (Y,W)
A1: Y <> {} by S3;
A3: (Y \/ Z) /\ W = Y /\ W by XBOOLE_1:78, A0;
card Y <= card (Y \/ Z) by NAT_1:43, XBOOLE_1:7;
then (card (Y /\ W)) / (card (Y \/ Z)) <= (card (Y /\ W)) / (card Y) by A1, XREAL_1:118;
then (card ((Y \/ Z) /\ W)) / (card (Y \/ Z)) <= kappa (Y,W) by A1, KappaDef, A3;
hence kappa ((Y \/ Z),W) <= kappa (Y,W) by A1, KappaDef; :: thesis: verum
end;
suppose Z0: ( Y /\ W = {} & Y \/ Z <> {} & Y <> {} ) ; :: thesis: kappa ((Y \/ Z),W) <= kappa (Y,W)
then Z1: Y misses W ;
then Y \/ Z misses W by A0, XBOOLE_1:70;
then kappa ((Y \/ Z),W) = 0 by Z0, Prop2b;
hence kappa ((Y \/ Z),W) <= kappa (Y,W) by Z1, Z0, Prop2b; :: thesis: verum
end;
suppose Z0: ( Y /\ W = {} & Y \/ Z <> {} & Y = {} ) ; :: thesis: kappa ((Y \/ Z),W) <= kappa (Y,W)
then kappa ((Y \/ Z),W) = 0 by A0, Prop2b;
hence kappa ((Y \/ Z),W) <= kappa (Y,W) by Z0, KappaDef; :: thesis: verum
end;
suppose ( Y /\ W = {} & Y \/ Z = {} ) ; :: thesis: kappa ((Y \/ Z),W) <= kappa (Y,W)
then ( Y = {} & Z = {} ) ;
hence kappa ((Y \/ Z),W) <= kappa (Y,W) ; :: thesis: verum
end;
end;