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