let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R holds kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))
let X, Y, Z be Subset of R; :: thesis: kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))

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

suppose A0: X <> {} ; :: thesis: kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))

then A1: kappa (X,(Y \/ Z)) = (card (X /\ (Y \/ Z))) / (card X) by KappaDef;
A2: kappa (X,Y) = (card (X /\ Y)) / (card X) by A0, KappaDef;
A3: kappa (X,Z) = (card (X /\ Z)) / (card X) by A0, KappaDef;
X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z) by XBOOLE_1:23;
then (card (X /\ (Y \/ Z))) / (card X) <= ((card (X /\ Y)) + (card (X /\ Z))) / (card X) by XREAL_1:72, CARD_2:43;
hence kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z)) by A2, A3, A1, XCMPLX_1:62; :: thesis: verum

end;

suppose A2: X = {} ; :: thesis: kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))

then A3: kappa (X,(Y \/ Z)) = 1 by KappaDef;
( kappa (X,Y) = 1 & kappa (X,Z) = 1 ) by A2, KappaDef;
hence kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z)) by A3; :: thesis: verum

end;

end;