let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X <> {} & Y <> {} holds
(delta_L R) . (X,Y) = (((card (X \ Y)) / (card X)) + ((card (Y \ X)) / (card Y))) / 2
let X, Y be Subset of R; :: thesis: ( X <> {} & Y <> {} implies (delta_L R) . (X,Y) = (((card (X \ Y)) / (card X)) + ((card (Y \ X)) / (card Y))) / 2 )
assume A1: ( X <> {} & Y <> {} ) ; :: thesis: (delta_L R) . (X,Y) = (((card (X \ Y)) / (card X)) + ((card (Y \ X)) / (card Y))) / 2
then A2: (CMap (kappa R)) . (X,Y) = (card (X \ Y)) / (card X) by PropEx3k;
(CMap (kappa R)) . (Y,X) = (card (Y \ X)) / (card Y) by A1, PropEx3k;
hence (delta_L R) . (X,Y) = (((card (X \ Y)) / (card X)) + ((card (Y \ X)) / (card Y))) / 2 by DeltaL, A2; :: thesis: verum