let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds (delta_L R) . (X,Y) = (delta_L R) . (Y,X)
let X, Y be Subset of R; :: thesis: (delta_L R) . (X,Y) = (delta_L R) . (Y,X)
(delta_L R) . (X,Y) = (((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X))) / 2 by DeltaL;
hence (delta_L R) . (X,Y) = (delta_L R) . (Y,X) by DeltaL; :: thesis: verum