let R be finite Approximation_Space; for X, Y being Subset of R holds
( (delta_L R) . (X,Y) = 0 iff X = Y )
let X, Y be Subset of R; ( (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;
assume A1:
X = Y
; (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
; verum