let R be finite Approximation_Space; 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; (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; verum