let R be finite Approximation_Space; :: thesis: for A, B being Subset of R holds (MarczewskiDistance R) . (A,B) = (delta_1 R) . (A,B)
let A, B be Subset of R; :: thesis: (MarczewskiDistance R) . (A,B) = (delta_1 R) . (A,B)
(MarczewskiDistance R) . (A,B) = (card (A \+\ B)) / (card (A \/ B)) by Similar2;
hence (MarczewskiDistance R) . (A,B) = (delta_1 R) . (A,B) by For191; :: thesis: verum