let R be finite Approximation_Space; for X, Y being Subset of R holds
( (delta_2 R) . (X,Y) = 0 iff X = Y )
let X, Y be Subset of R; ( (delta_2 R) . (X,Y) = 0 iff X = Y )
B1:
( (CMap (kappa_2 R)) . (X,Y) >= 0 & (CMap (kappa_2 R)) . (Y,X) >= 0 )
by XXREAL_1:1;
assume A1:
X = Y
; (delta_2 R) . (X,Y) = 0
(delta_2 R) . (X,Y) =
((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,X))
by Delta2
.=
((CMap (kappa_2 R)) . (X,X)) + 0
by Prop6a, A1
.=
0 + 0
by Prop6a
;
hence
(delta_2 R) . (X,Y) = 0
; verum