let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( (delta_L R) . (X,Y) = 0 iff X = Y )
let X, Y be Subset of R; :: thesis: ( (delta_L R) . (X,Y) = 0 iff X = Y )
B1: ( (CMap (kappa R)) . (X,Y) >= 0 & (CMap (kappa R)) . (Y,X) >= 0 ) by XXREAL_1:1;

hereby :: thesis: ( X = Y implies (delta_L R) . (X,Y) = 0 )

assume (delta_L R) . (X,Y) = 0 ; :: thesis: X = Y
then (((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X))) / 2 = 0 by DeltaL;
then ( (CMap (kappa R)) . (X,Y) = 0 & (CMap (kappa R)) . (Y,X) = 0 ) by B1;
hence X = Y by Prop6a; :: thesis: verum

end;

assume A1: X = Y ; :: thesis: (delta_L R) . (X,Y) = 0
(delta_L R) . (X,Y) = (((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X))) / 2 by DeltaL
.= (0 + 0) / 2 by Prop6a, A1 ;
hence (delta_L R) . (X,Y) = 0 ; :: thesis: verum