let M be MetrStruct ; :: thesis: for a being Point of M
for X being non empty set holds
( ( well_dist a,X is Reflexive implies M is Reflexive ) & ( well_dist a,X is symmetric implies M is symmetric ) & ( well_dist a,X is triangle & well_dist a,X is Reflexive implies M is triangle ) & ( well_dist a,X is discerning & well_dist a,X is Reflexive implies M is discerning ) )
let A be Point of M; :: thesis: for X being non empty set holds
( ( well_dist A,X is Reflexive implies M is Reflexive ) & ( well_dist A,X is symmetric implies M is symmetric ) & ( well_dist A,X is triangle & well_dist A,X is Reflexive implies M is triangle ) & ( well_dist A,X is discerning & well_dist A,X is Reflexive implies M is discerning ) )
let X be non empty set ; :: thesis: ( ( well_dist A,X is Reflexive implies M is Reflexive ) & ( well_dist A,X is symmetric implies M is symmetric ) & ( well_dist A,X is triangle & well_dist A,X is Reflexive implies M is triangle ) & ( well_dist A,X is discerning & well_dist A,X is Reflexive implies M is discerning ) )
consider x0 being set such that
A1: x0 in X by XBOOLE_0:def 1;
set w = well_dist A,X;
set XX = [:X,(the carrier of M \ {A}):] \/ {[X,A]};
thus A2: ( well_dist A,X is Reflexive implies M is Reflexive ) :: thesis: ( ( well_dist A,X is symmetric implies M is symmetric ) & ( well_dist A,X is triangle & well_dist A,X is Reflexive implies M is triangle ) & ( well_dist A,X is discerning & well_dist A,X is Reflexive implies M is discerning ) )

proof

assume A3: well_dist A,X is Reflexive ; :: thesis: M is Reflexive

now

let a be Element of M; :: thesis: dist a,a = 0

now

per cases ( a = A or a <> A ) ;

suppose a = A ; :: thesis: dist a,a = 0

then A4: [X,a] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by Th38;
hence dist a,a = (well_dist A,X) . [X,a],[X,a] by Def10
.= 0 by A3, A4, METRIC_1:def 3 ;
:: thesis: verum

end;

suppose a <> A ; :: thesis: dist a,a = 0

then A5: [x0,a] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
hence dist a,a = (well_dist A,X) . [x0,a],[x0,a] by Def10
.= 0 by A3, A5, METRIC_1:def 3 ;
:: thesis: verum

end;

end;

end;

hence dist a,a = 0 ; :: thesis: verum

end;

hence M is Reflexive by METRIC_1:1; :: thesis: verum

end;

thus ( well_dist A,X is symmetric implies M is symmetric ) :: thesis: ( ( well_dist A,X is triangle & well_dist A,X is Reflexive implies M is triangle ) & ( well_dist A,X is discerning & well_dist A,X is Reflexive implies M is discerning ) )

proof

assume A6: well_dist A,X is symmetric ; :: thesis: M is symmetric

now

let a, b be Element of M; :: thesis: dist a,b = dist b,a

now

per cases ( ( a = A & b = A ) or ( a = A & b <> A ) or ( a <> A & b = A ) or ( a <> A & b <> A ) ) ;

suppose ( a = A & b = A ) ; :: thesis: dist a,b = dist b,a

hence dist a,b = dist b,a ; :: thesis: verum

end;

suppose A7: ( a = A & b <> A ) ; :: thesis: dist a,b = dist b,a

then A8: [x0,b] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A9: [X,A] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by Th38;
A10: X <> x0 by A1;
then (dist A,A) + (dist A,b) = (well_dist A,X) . [X,A],[x0,b] by A9, A8, Def10
.= (well_dist A,X) . [x0,b],[X,A] by A6, A9, A8, METRIC_1:def 5
.= (dist b,A) + (dist A,A) by A9, A8, A10, Def10 ;
hence dist a,b = dist b,a by A7; :: thesis: verum

end;

suppose A11: ( a <> A & b = A ) ; :: thesis: dist a,b = dist b,a

then A12: [x0,a] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A13: [X,A] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by Th38;
A14: X <> x0 by A1;
then (dist A,A) + (dist A,a) = (well_dist A,X) . [X,A],[x0,a] by A13, A12, Def10
.= (well_dist A,X) . [x0,a],[X,A] by A6, A13, A12, METRIC_1:def 5
.= (dist a,A) + (dist A,A) by A13, A12, A14, Def10 ;
hence dist a,b = dist b,a by A11; :: thesis: verum

end;

suppose A15: ( a <> A & b <> A ) ; :: thesis: dist a,b = dist b,a

then A16: [x0,b] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A17: [x0,a] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, A15, Th38;
hence dist a,b = (well_dist A,X) . [x0,a],[x0,b] by A16, Def10
.= (well_dist A,X) . [x0,b],[x0,a] by A6, A17, A16, METRIC_1:def 5
.= dist b,a by A17, A16, Def10 ;
:: thesis: verum

end;

end;

end;

hence dist a,b = dist b,a ; :: thesis: verum

end;

hence M is symmetric by METRIC_1:3; :: thesis: verum

end;

thus ( well_dist A,X is triangle & well_dist A,X is Reflexive implies M is triangle ) :: thesis: ( well_dist A,X is discerning & well_dist A,X is Reflexive implies M is discerning )

proof

assume A18: ( well_dist A,X is triangle & well_dist A,X is Reflexive ) ; :: thesis: M is triangle

now

let a, b, c be Point of M; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

now

per cases ( ( a = A & b = A & c = A ) or ( a = A & b = A & c <> A ) or ( a = A & b <> A & c = A ) or ( a = A & b <> A & c <> A ) or ( a <> A & b = A & c = A ) or ( a <> A & b = A & c <> A ) or ( a <> A & b <> A & c = A ) or ( a <> A & b <> A & c <> A ) ) ;

suppose ( a = A & b = A & c = A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [X,a], Xb = [X,b], Xc = [X,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by Th38;
A19: dist a,c = (well_dist A,X) . Xa,Xc by Def10;
A20: dist a,b = (well_dist A,X) . Xa,Xb by Def10;
(well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) by A18, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) by A19, A20, Def10; :: thesis: verum

end;

suppose A21: ( a = A & b = A & c <> A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [X,a], Xb = [X,b], Xc = [x0,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
dist a,a = 0 by A2, A18, METRIC_1:1;
hence dist a,c <= (dist a,b) + (dist b,c) by A21; :: thesis: verum

end;

suppose A22: ( a = A & b <> A & c = A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [X,a], Xb = [x0,b], Xc = [X,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A23: x0 <> X by A1;
then A24: (dist b,c) + (dist a,a) = (well_dist A,X) . Xb,Xc by A22, Def10;
A25: dist a,a = 0 by A2, A18, METRIC_1:1;
A26: (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) by A18, METRIC_1:def 6;
(dist a,a) + (dist a,b) = (well_dist A,X) . Xa,Xb by A22, A23, Def10;
hence dist a,c <= (dist a,b) + (dist b,c) by A26, A24, A25, Def10; :: thesis: verum

end;

suppose A27: ( a = A & b <> A & c <> A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [X,a], Xb = [x0,b], Xc = [x0,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A28: x0 <> X by A1;
then A29: (dist a,a) + (dist a,b) = (well_dist A,X) . Xa,Xb by A27, Def10;
A30: dist a,a = 0 by A2, A18, METRIC_1:1;
A31: (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) by A18, METRIC_1:def 6;
(dist a,a) + (dist a,c) = (well_dist A,X) . Xa,Xc by A27, A28, Def10;
hence dist a,c <= (dist a,b) + (dist b,c) by A31, A29, A30, Def10; :: thesis: verum

end;

suppose A32: ( a <> A & b = A & c = A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [x0,a], Xb = [X,b], Xc = [X,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
dist c,c = 0 by A2, A18, METRIC_1:1;
hence dist a,c <= (dist a,b) + (dist b,c) by A32; :: thesis: verum

end;

suppose A33: ( a <> A & b = A & c <> A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [x0,a], Xb = [X,b], Xc = [x0,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A34: x0 <> X by A1;
then A35: (dist b,b) + (dist b,c) = (well_dist A,X) . Xb,Xc by A33, Def10;
A36: dist b,b = 0 by A2, A18, METRIC_1:1;
A37: (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) by A18, METRIC_1:def 6;
(dist a,b) + (dist b,b) = (well_dist A,X) . Xa,Xb by A33, A34, Def10;
hence dist a,c <= (dist a,b) + (dist b,c) by A37, A35, A36, Def10; :: thesis: verum

end;

suppose A38: ( a <> A & b <> A & c = A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [x0,a], Xb = [x0,b], Xc = [X,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A39: x0 <> X by A1;
then A40: (dist b,c) + (dist c,c) = (well_dist A,X) . Xb,Xc by A38, Def10;
A41: dist c,c = 0 by A2, A18, METRIC_1:1;
A42: (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) by A18, METRIC_1:def 6;
(dist a,c) + (dist c,c) = (well_dist A,X) . Xa,Xc by A38, A39, Def10;
hence dist a,c <= (dist a,b) + (dist b,c) by A42, A40, A41, Def10; :: thesis: verum

end;

suppose ( a <> A & b <> A & c <> A ) ; :: thesis: dist a,c <= (dist a,b) + (dist b,c)

then reconsider Xa = [x0,a], Xb = [x0,b], Xc = [x0,c] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
A43: dist a,c = (well_dist A,X) . Xa,Xc by Def10;
A44: dist a,b = (well_dist A,X) . Xa,Xb by Def10;
(well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) by A18, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) by A43, A44, Def10; :: thesis: verum

end;

end;

end;

hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

hence M is triangle by METRIC_1:4; :: thesis: verum

end;

assume A45: ( well_dist A,X is discerning & well_dist A,X is Reflexive ) ; :: thesis: M is discerning

now

let a, b be Point of M; :: thesis: ( dist a,b = 0 implies a = b )
assume A46: dist a,b = 0 ; :: thesis: a = b

now

per cases ( ( a = A & b = A ) or ( a = A & b <> A ) or ( a <> A & b = A ) or ( a <> A & b <> A ) ) ;

suppose ( a = A & b = A ) ; :: thesis: a = b

hence a = b ; :: thesis: verum

end;

suppose A47: ( a = A & b <> A ) ; :: thesis: a = b

then reconsider Xa = [X,a], Xb = [x0,b] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
x0 <> X by A1;
then A48: (dist a,a) + (dist a,b) = (well_dist A,X) . Xa,Xb by A47, Def10;
dist a,a = 0 by A2, A45, METRIC_1:1;
then Xa = Xb by A45, A46, A48, METRIC_1:def 4;
hence a = b by ZFMISC_1:33; :: thesis: verum

end;

suppose A49: ( a <> A & b = A ) ; :: thesis: a = b

then reconsider Xa = [x0,a], Xb = [X,b] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
x0 <> X by A1;
then A50: (dist a,b) + (dist b,b) = (well_dist A,X) . Xa,Xb by A49, Def10;
dist b,b = 0 by A2, A45, METRIC_1:1;
then Xa = Xb by A45, A46, A50, METRIC_1:def 4;
hence a = b by ZFMISC_1:33; :: thesis: verum

end;

suppose ( a <> A & b <> A ) ; :: thesis: a = b

then reconsider Xa = [x0,a], Xb = [x0,b] as Element of [:X,(the carrier of M \ {A}):] \/ {[X,A]} by A1, Th38;
dist a,b = (well_dist A,X) . Xa,Xb by Def10;
then Xa = Xb by A45, A46, METRIC_1:def 4;
hence a = b by ZFMISC_1:33; :: thesis: verum

end;

end;

end;

hence a = b ; :: thesis: verum

end;

hence M is discerning by METRIC_1:2; :: thesis: verum