let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R st X <> {} & X misses Y holds
( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) )
let X, Y, Z be Subset of R; :: thesis: ( X <> {} & X misses Y implies ( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) ) )
assume A1: ( X <> {} & X misses Y ) ; :: thesis: ( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) )
then D1: kappa (X,Y) = 0 by Prop2b;
D3: kappa (X,Z) = kappa (X,((Z /\ Y) \/ (Z \ Y))) by XBOOLE_1:51
.= (kappa (X,(Z /\ Y))) + (kappa (X,(Z \ Y))) by Prop1e, A1, XBOOLE_1:89 ;
kappa (X,(Z /\ Y)) <= 0 by D1, Prop1b, XBOOLE_1:17;
then D5: kappa (X,(Z /\ Y)) = 0 by XXREAL_1:1;
e1: kappa (X,(Z \/ Y)) <= (kappa (X,Z)) + (kappa (X,Y)) by Prop1d;
kappa (X,Z) <= kappa (X,(Z \/ Y)) by Prop1b, XBOOLE_1:7;
hence ( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) ) by D5, D3, e1, D1, XXREAL_0:1; :: thesis: verum