let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( (delta_1 R) . (X,Y) = 0 iff X = Y )
let X, Y be Subset of R; :: thesis: ( (delta_1 R) . (X,Y) = 0 iff X = Y )
B1: ( (CMap (kappa_1 R)) . (X,Y) >= 0 & (CMap (kappa_1 R)) . (Y,X) >= 0 ) by XXREAL_1:1;
hereby :: thesis: ( X = Y implies (delta_1 R) . (X,Y) = 0 )
assume (delta_1 R) . (X,Y) = 0 ; :: thesis: X = Y
then ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 0 by Delta1;
then ( (CMap (kappa_1 R)) . (X,Y) = 0 & (CMap (kappa_1 R)) . (Y,X) = 0 ) by B1;
hence X = Y by Prop6a; :: thesis: verum
end;
assume A1: X = Y ; :: thesis: (delta_1 R) . (X,Y) = 0
(delta_1 R) . (X,Y) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) by Delta1
.= ((CMap (kappa_1 R)) . (X,X)) + 0 by Prop6a, A1
.= 0 + 0 by Prop6a ;
hence (delta_1 R) . (X,Y) = 0 ; :: thesis: verum