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 XX = [:X,(the carrier of M \ {A}):] \/ {[X,A]};
set w = well_dist A,X;
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: ( [X,A] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} & [x0,b] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} ) by A1, Th38;
A9: X <> x0 by A1;
then (dist A,A) + (dist A,b) = (well_dist A,X) . [X,A],[x0,b] by A8, Def10
.= (well_dist A,X) . [x0,b],[X,A] by A6, A8, METRIC_1:def 5
.= (dist b,A) + (dist A,A) by A8, A9, Def10 ;
hence dist a,b = dist b,a by A7; :: thesis: verum

end;

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

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

end;

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

then A13: ( [x0,a] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} & [x0,b] in [:X,(the carrier of M \ {A}):] \/ {[X,A]} ) by A1, Th38;
hence dist a,b = (well_dist A,X) . [x0,a],[x0,b] by Def10
.= (well_dist A,X) . [x0,b],[x0,a] by A6, A13, METRIC_1:def 5
.= dist b,a by A13, 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 A14: ( 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;
( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & dist a,c = (well_dist A,X) . Xa,Xc & dist a,b = (well_dist A,X) . Xa,Xb & dist b,c = (well_dist A,X) . Xb,Xc ) by A14, Def10, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

suppose A15: ( 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;
x0 <> X by A1;
then ( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & dist a,b = (well_dist A,X) . Xa,Xb & (dist a,a) + (dist a,c) = (well_dist A,X) . Xa,Xc & (dist a,a) + (dist b,c) = (well_dist A,X) . Xb,Xc & dist a,a = 0 ) by A2, A14, A15, Def10, METRIC_1:1, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

suppose A16: ( 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;
x0 <> X by A1;
then ( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & dist a,c = (well_dist A,X) . Xa,Xc & (dist a,a) + (dist a,b) = (well_dist A,X) . Xa,Xb & (dist b,c) + (dist a,a) = (well_dist A,X) . Xb,Xc & dist a,a = 0 ) by A2, A14, A16, Def10, METRIC_1:1, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

suppose A17: ( 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;
x0 <> X by A1;
then ( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & (dist a,a) + (dist a,c) = (well_dist A,X) . Xa,Xc & (dist a,a) + (dist a,b) = (well_dist A,X) . Xa,Xb & dist b,c = (well_dist A,X) . Xb,Xc & dist a,a = 0 ) by A2, A14, A17, Def10, METRIC_1:1, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

suppose A18: ( 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;
x0 <> X by A1;
then ( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & (dist a,c) + (dist c,c) = (well_dist A,X) . Xa,Xc & (dist a,b) + (dist c,c) = (well_dist A,X) . Xa,Xb & dist b,c = (well_dist A,X) . Xb,Xc & dist c,c = 0 ) by A2, A14, A18, Def10, METRIC_1:1, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

suppose A19: ( 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;
x0 <> X by A1;
then ( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & dist a,c = (well_dist A,X) . Xa,Xc & (dist a,b) + (dist b,b) = (well_dist A,X) . Xa,Xb & (dist b,b) + (dist b,c) = (well_dist A,X) . Xb,Xc & dist b,b = 0 ) by A2, A14, A19, Def10, METRIC_1:1, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

suppose A20: ( 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;
x0 <> X by A1;
then ( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & (dist a,c) + (dist c,c) = (well_dist A,X) . Xa,Xc & dist a,b = (well_dist A,X) . Xa,Xb & (dist b,c) + (dist c,c) = (well_dist A,X) . Xb,Xc & dist c,c = 0 ) by A2, A14, A20, Def10, METRIC_1:1, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: 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;
( (well_dist A,X) . Xa,Xc <= ((well_dist A,X) . Xa,Xb) + ((well_dist A,X) . Xb,Xc) & dist a,c = (well_dist A,X) . Xa,Xc & dist a,b = (well_dist A,X) . Xa,Xb & dist b,c = (well_dist A,X) . Xb,Xc ) by A14, Def10, METRIC_1:def 6;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: 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 A21: ( 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 A22: 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 A23: ( 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 ( (dist a,a) + (dist a,b) = (well_dist A,X) . Xa,Xb & dist a,a = 0 ) by A2, A21, A23, Def10, METRIC_1:1;
then Xa = Xb by A21, A22, METRIC_1:def 4;
hence a = b by ZFMISC_1:33; :: thesis: verum

end;

suppose A24: ( 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 ( (dist a,b) + (dist b,b) = (well_dist A,X) . Xa,Xb & dist b,b = 0 ) by A2, A21, A24, Def10, METRIC_1:1;
then Xa = Xb by A21, A22, 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 A21, A22, 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