set f = MarczewskiDistance R;
for a being Subset of R holds (MarczewskiDistance R) . (a,a) = 0
proof
let a be Subset of R; :: thesis: (MarczewskiDistance R) . (a,a) = 0
(MarczewskiDistance R) . (a,a) = 1 - (JaccardIndex (a,a)) by JacDef2
.= 1 - 1 by JacRefl ;
hence (MarczewskiDistance R) . (a,a) = 0 ; :: thesis: verum
end;
hence MarczewskiDistance R is Reflexive by METRIC_1:def 2; :: thesis: ( MarczewskiDistance R is discerning & MarczewskiDistance R is symmetric )
a1: for a, b being Subset of R st (MarczewskiDistance R) . (a,b) = 0 holds
a = b
proof
let a, b be Subset of R; :: thesis: ( (MarczewskiDistance R) . (a,b) = 0 implies a = b )
assume (MarczewskiDistance R) . (a,b) = 0 ; :: thesis: a = b
then 1 - (JaccardIndex (a,b)) = 0 by JacDef2;
hence a = b by JacRefl; :: thesis: verum
end;
set A = bool the carrier of R;
for a, b being Element of bool the carrier of R holds (MarczewskiDistance R) . (a,b) = (MarczewskiDistance R) . (b,a)
proof
let a, b be Element of bool the carrier of R; :: thesis: (MarczewskiDistance R) . (a,b) = (MarczewskiDistance R) . (b,a)
(MarczewskiDistance R) . (a,b) = 1 - (JaccardIndex (a,b)) by JacDef2
.= 1 - (JaccardIndex (b,a)) by JacSym
.= (MarczewskiDistance R) . (b,a) by JacDef2 ;
hence (MarczewskiDistance R) . (a,b) = (MarczewskiDistance R) . (b,a) ; :: thesis: verum
end;
hence ( MarczewskiDistance R is discerning & MarczewskiDistance R is symmetric ) by a1, METRIC_1:def 4, METRIC_1:def 3; :: thesis: verum