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

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

suppose A1: X \/ Y <> {} ; :: thesis: kappa_1 (X,Y) = kappa ((X \/ Y),Y)

then kappa ((X \/ Y),Y) = (card ((X \/ Y) /\ Y)) / (card (X \/ Y)) by KappaDef
.= (card Y) / (card (X \/ Y)) by XBOOLE_1:21 ;
hence kappa_1 (X,Y) = kappa ((X \/ Y),Y) by A1, Kappa1; :: thesis: verum

end;

suppose A1: X = {} ; :: thesis: kappa_1 (X,Y) = kappa ((X \/ Y),Y)

then AA: X c= Y ;
kappa ((X \/ Y),Y) = 1 by Prop1a, A1;
hence kappa_1 (X,Y) = kappa ((X \/ Y),Y) by Prop11a, AA; :: thesis: verum

end;

end;