set f = SymmetricDiffDist X;
for x being Element of bool X holds (SymmetricDiffDist X) . (x,x) = 0
proof
let x be Element of bool X; :: thesis: (SymmetricDiffDist X) . (x,x) = 0
(SymmetricDiffDist X) . (x,x) = card (x \+\ x) by SymDist
.= card ({} X) by XBOOLE_1:92
.= 0 ;
hence (SymmetricDiffDist X) . (x,x) = 0 ; :: thesis: verum
end;
hence SymmetricDiffDist X is Reflexive by METRIC_1:def 2; :: thesis: ( SymmetricDiffDist X is discerning & SymmetricDiffDist X is symmetric & SymmetricDiffDist X is triangle )
for a, b being Element of bool X st (SymmetricDiffDist X) . (a,b) = 0 holds
a = b
proof
let a, b be Subset of X; :: thesis: ( (SymmetricDiffDist X) . (a,b) = 0 implies a = b )
assume (SymmetricDiffDist X) . (a,b) = 0 ; :: thesis: a = b
then card (a \+\ b) = 0 by SymDist;
then ( a \ b = {} & b \ a = {} ) ;
hence a = b by XBOOLE_1:37; :: thesis: verum
end;
hence SymmetricDiffDist X is discerning by METRIC_1:def 3; :: thesis: ( SymmetricDiffDist X is symmetric & SymmetricDiffDist X is triangle )
for a, b being Element of bool X holds (SymmetricDiffDist X) . (a,b) = (SymmetricDiffDist X) . (b,a)
proof
let a, b be Subset of X; :: thesis: (SymmetricDiffDist X) . (a,b) = (SymmetricDiffDist X) . (b,a)
(SymmetricDiffDist X) . (a,b) = card (a \+\ b) by SymDist
.= (SymmetricDiffDist X) . (b,a) by SymDist ;
hence (SymmetricDiffDist X) . (a,b) = (SymmetricDiffDist X) . (b,a) ; :: thesis: verum
end;
hence SymmetricDiffDist X is symmetric by METRIC_1:def 4; :: thesis: SymmetricDiffDist X is triangle
for a, b, c being Element of bool X holds (SymmetricDiffDist X) . (a,c) <= ((SymmetricDiffDist X) . (a,b)) + ((SymmetricDiffDist X) . (b,c))
proof
let a, b, c be Element of bool X; :: thesis: (SymmetricDiffDist X) . (a,c) <= ((SymmetricDiffDist X) . (a,b)) + ((SymmetricDiffDist X) . (b,c))
B1: (SymmetricDiffDist X) . (a,c) = card (a \+\ c) by SymDist;
B2: (SymmetricDiffDist X) . (a,b) = card (a \+\ b) by SymDist;
B3: (SymmetricDiffDist X) . (b,c) = card (b \+\ c) by SymDist;
a \+\ c = (a \+\ b) \+\ (b \+\ c) by Jajo;
then A1: card (a \+\ c) <= card ((a \+\ b) \/ (b \+\ c)) by NAT_1:43, Lack;
card ((a \+\ b) \/ (b \+\ c)) <= (card (a \+\ b)) + (card (b \+\ c)) by CARD_2:43;
hence (SymmetricDiffDist X) . (a,c) <= ((SymmetricDiffDist X) . (a,b)) + ((SymmetricDiffDist X) . (b,c)) by B1, B2, B3, A1, XXREAL_0:2; :: thesis: verum
end;
hence SymmetricDiffDist X is triangle by METRIC_1:def 5; :: thesis: verum