let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds (delta_1 R) . (X,Y) = (delta_1 R) . (Y,X)
let X, Y be Subset of R; :: thesis: (delta_1 R) . (X,Y) = (delta_1 R) . (Y,X)
(delta_1 R) . (X,Y) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) by Delta1;
hence (delta_1 R) . (X,Y) = (delta_1 R) . (Y,X) by Delta1; :: thesis: verum