let M be MetrStruct ; :: thesis: for a being Point of M
for X being set holds
( ( M is Reflexive implies WellSpace a,X is Reflexive ) & ( M is symmetric implies WellSpace a,X is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace a,X is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace a,X is discerning ) )
let a be Point of M; :: thesis: for X being set holds
( ( M is Reflexive implies WellSpace a,X is Reflexive ) & ( M is symmetric implies WellSpace a,X is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace a,X is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace a,X is discerning ) )
let X be set ; :: thesis: ( ( M is Reflexive implies WellSpace a,X is Reflexive ) & ( M is symmetric implies WellSpace a,X is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace a,X is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace a,X is discerning ) )
set XX = [:X,(the carrier of M \ {a}):] \/ {[X,a]};
set w = well_dist a,X;
set W = WellSpace a,X;
thus ( M is Reflexive implies WellSpace a,X is Reflexive ) :: thesis: ( ( M is symmetric implies WellSpace a,X is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace a,X is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace a,X is discerning ) )

proof

assume A1: M is Reflexive ; :: thesis: WellSpace a,X is Reflexive

now

let A be Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: (well_dist a,X) . A,A = 0
consider y being set , b being Point of M such that
A2: A = [y,b] and
( ( y in X & b <> a ) or ( y = X & b = a ) ) by Th38;
thus (well_dist a,X) . A,A = dist b,b by A2, Def10
.= 0 by A1, METRIC_1:1 ; :: thesis: verum

end;

then well_dist a,X is Reflexive by METRIC_1:def 3;
hence WellSpace a,X is Reflexive by METRIC_1:def 7; :: thesis: verum

end;

thus ( M is symmetric implies WellSpace a,X is symmetric ) :: thesis: ( ( M is triangle & M is symmetric & M is Reflexive implies WellSpace a,X is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace a,X is discerning ) )

proof

assume A3: M is symmetric ; :: thesis: WellSpace a,X is symmetric

now

let A, B be Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: (well_dist a,X) . A,B = (well_dist a,X) . B,A
consider y1 being set , b1 being Point of M such that
A4: A = [y1,b1] and
A5: ( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) by Th38;
consider y2 being set , b2 being Point of M such that
A6: B = [y2,b2] and
A7: ( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) by Th38;

now

per cases ( ( b1 = a & y1 = X & b2 = a & y2 = X ) or y1 <> y2 or ( b1 <> a & b2 <> a & y1 = y2 ) ) by A5, A7;

suppose ( b1 = a & y1 = X & b2 = a & y2 = X ) ; :: thesis: (well_dist a,X) . A,B = (well_dist a,X) . B,A

hence (well_dist a,X) . A,B = (well_dist a,X) . B,A by A4, A6; :: thesis: verum

end;

suppose A8: y1 <> y2 ; :: thesis: (well_dist a,X) . A,B = (well_dist a,X) . B,A

hence (well_dist a,X) . A,B = (dist b1,a) + (dist a,b2) by A4, A6, Def10
.= (dist a,b1) + (dist a,b2) by A3, METRIC_1:3
.= (dist a,b1) + (dist b2,a) by A3, METRIC_1:3
.= (well_dist a,X) . B,A by A4, A6, A8, Def10 ;
:: thesis: verum

end;

suppose A9: ( b1 <> a & b2 <> a & y1 = y2 ) ; :: thesis: (well_dist a,X) . A,B = (well_dist a,X) . B,A

hence (well_dist a,X) . A,B = dist b1,b2 by A4, A6, Def10
.= dist b2,b1 by A3, METRIC_1:3
.= (well_dist a,X) . B,A by A4, A6, A9, Def10 ;
:: thesis: verum

end;

end;

end;

hence (well_dist a,X) . A,B = (well_dist a,X) . B,A ; :: thesis: verum

end;

then well_dist a,X is symmetric by METRIC_1:def 5;
hence WellSpace a,X is symmetric by METRIC_1:def 9; :: thesis: verum

end;

thus ( M is triangle & M is symmetric & M is Reflexive implies WellSpace a,X is triangle ) :: thesis: ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace a,X is discerning )

proof

assume A10: ( M is triangle & M is symmetric & M is Reflexive ) ; :: thesis: WellSpace a,X is triangle

now

let A, B, C be Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C)
consider y1 being set , b1 being Point of M such that
A11: A = [y1,b1] and
( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) by Th38;
consider y2 being set , b2 being Point of M such that
A12: B = [y2,b2] and
( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) by Th38;
consider y3 being set , b3 being Point of M such that
A13: C = [y3,b3] and
( ( y3 in X & b3 <> a ) or ( y3 = X & b3 = a ) ) by Th38;

now

per cases ( ( y1 = y2 & y1 = y3 ) or ( y1 <> y2 & y1 = y3 ) or ( y1 = y2 & y1 <> y3 ) or ( y1 <> y2 & y1 <> y3 & y2 <> y3 ) or ( y1 <> y2 & y1 <> y3 & y2 = y3 ) ) ;

suppose A14: ( y1 = y2 & y1 = y3 ) ; :: thesis: (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C)

then A15: dist b2,b3 = (well_dist a,X) . B,C by A12, A13, Def10;
A16: dist b1,b2 = (well_dist a,X) . A,B by A11, A12, A14, Def10;
dist b1,b3 = (well_dist a,X) . A,C by A11, A13, A14, Def10;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A10, A16, A15, METRIC_1:4; :: thesis: verum

end;

suppose A17: ( y1 <> y2 & y1 = y3 ) ; :: thesis: (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C)

then A18: (dist b2,a) + (dist a,b3) = (well_dist a,X) . B,C by A12, A13, Def10;
A19: dist b1,b2 <= (dist b1,a) + (dist a,b2) by A10, METRIC_1:4;
A20: dist b2,b3 <= (dist b2,a) + (dist a,b3) by A10, METRIC_1:4;
(dist b1,a) + (dist a,b2) = (well_dist a,X) . A,B by A11, A12, A17, Def10;
then A21: (dist b1,b2) + (dist b2,b3) <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A18, A19, A20, XREAL_1:9;
A22: dist b1,b3 <= (dist b1,b2) + (dist b2,b3) by A10, METRIC_1:4;
dist b1,b3 = (well_dist a,X) . A,C by A11, A13, A17, Def10;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A21, A22, XXREAL_0:2; :: thesis: verum

end;

suppose A23: ( y1 = y2 & y1 <> y3 ) ; :: thesis: (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C)

A24: dist b1,a <= (dist b1,b2) + (dist b2,a) by A10, METRIC_1:4;
(dist b1,a) + (dist a,b3) = (well_dist a,X) . A,C by A11, A13, A23, Def10;
then A25: (well_dist a,X) . A,C <= ((dist b1,b2) + (dist b2,a)) + (dist a,b3) by A24, XREAL_1:8;
A26: (dist b2,a) + (dist a,b3) = (well_dist a,X) . B,C by A12, A13, A23, Def10;
dist b1,b2 = (well_dist a,X) . A,B by A11, A12, A23, Def10;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A26, A25; :: thesis: verum

end;

suppose A27: ( y1 <> y2 & y1 <> y3 & y2 <> y3 ) ; :: thesis: (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C)

A28: 0 <= dist b2,a by A10, METRIC_1:5;
(dist b2,a) + (dist a,b3) = (well_dist a,X) . B,C by A12, A13, A27, Def10;
then A29: 0 + (dist a,b3) <= (well_dist a,X) . B,C by A28, XREAL_1:8;
A30: 0 <= dist a,b2 by A10, METRIC_1:5;
(dist b1,a) + (dist a,b2) = (well_dist a,X) . A,B by A11, A12, A27, Def10;
then A31: (dist b1,a) + 0 <= (well_dist a,X) . A,B by A30, XREAL_1:8;
(dist b1,a) + (dist a,b3) = (well_dist a,X) . A,C by A11, A13, A27, Def10;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A31, A29, XREAL_1:9; :: thesis: verum

end;

suppose A32: ( y1 <> y2 & y1 <> y3 & y2 = y3 ) ; :: thesis: (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C)

A33: dist a,b3 <= (dist a,b2) + (dist b2,b3) by A10, METRIC_1:4;
(dist b1,a) + (dist a,b3) = (well_dist a,X) . A,C by A11, A13, A32, Def10;
then A34: (well_dist a,X) . A,C <= (dist b1,a) + ((dist a,b2) + (dist b2,b3)) by A33, XREAL_1:9;
A35: dist b2,b3 = (well_dist a,X) . B,C by A12, A13, A32, Def10;
(dist b1,a) + (dist a,b2) = (well_dist a,X) . A,B by A11, A12, A32, Def10;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A35, A34; :: thesis: verum

end;

end;

end;

hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) ; :: thesis: verum

end;

then well_dist a,X is triangle by METRIC_1:def 6;
hence WellSpace a,X is triangle by METRIC_1:def 10; :: thesis: verum

end;

assume A36: ( M is triangle & M is symmetric & M is Reflexive & M is discerning ) ; :: thesis: WellSpace a,X is discerning

now

let A, B be Element of [:X,(the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: ( (well_dist a,X) . A,B = 0 implies A = B )
consider y1 being set , b1 being Point of M such that
A37: A = [y1,b1] and
A38: ( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) by Th38;
consider y2 being set , b2 being Point of M such that
A39: B = [y2,b2] and
A40: ( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) by Th38;
assume A41: (well_dist a,X) . A,B = 0 ; :: thesis: A = B

now

per cases ( y1 = y2 or y1 <> y2 ) ;

suppose A42: y1 = y2 ; :: thesis: A = B

then (well_dist a,X) . A,B = dist b1,b2 by A37, A39, Def10;
hence A = B by A36, A41, A37, A39, A42, METRIC_1:2; :: thesis: verum

end;

suppose y1 <> y2 ; :: thesis: A = B

then A43: (well_dist a,X) . A,B = (dist b1,a) + (dist a,b2) by A37, A39, Def10;
A44: dist b1,a >= 0 by A36, METRIC_1:5;
dist a,b2 >= 0 by A36, METRIC_1:5;
then dist b1,a = 0 by A41, A43, A44;
hence A = B by A36, A41, A37, A38, A39, A40, A43, METRIC_1:2; :: thesis: verum

end;

end;

end;

hence A = B ; :: thesis: verum

end;

then well_dist a,X is discerning by METRIC_1:def 4;
hence WellSpace a,X is discerning by METRIC_1:def 8; :: thesis: verum