let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y))
let X, Y be Subset of R; :: thesis: (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y))

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

suppose A0: X \/ Y <> {} ; :: thesis: (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y))

then A2: (CMap (kappa_1 R)) . (Y,X) = (card (Y \ X)) / (card (X \/ Y)) by PropEx3;
(delta_1 R) . (X,Y) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) by Delta1
.= ((card (X \ Y)) / (card (X \/ Y))) + ((card (Y \ X)) / (card (X \/ Y))) by A0, PropEx3, A2
.= ((card (X \ Y)) + (card (Y \ X))) / (card (X \/ Y)) by XCMPLX_1:62
.= (card (X \+\ Y)) / (card (X \/ Y)) by XBOOLE_1:82, CARD_2:40 ;
hence (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y)) ; :: thesis: verum

end;

suppose A0: X \/ Y = {} ; :: thesis: (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y))

then ( X = {} & Y = {} ) ;
then ( (CMap (kappa_1 R)) . (X,Y) = 0 & (CMap (kappa_1 R)) . (Y,X) = 0 ) by Prop6a;
then (delta_1 R) . (X,Y) = 0 + 0 by Delta1;
hence (delta_1 R) . (X,Y) = (card (X \+\ Y)) / (card (X \/ Y)) by A0; :: thesis: verum

end;

end;