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