let R be finite Approximation_Space; 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; ( 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 )
; ( 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; verum