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] & ( ( 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] & ( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) ) by Th38;
consider y2 being set , b2 being Point of M such that
A5: ( B = [y2,b2] & ( ( 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 A4, A5;

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, A5; :: thesis: verum

end;

suppose A6: 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, A5, 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, A5, A6, Def10 ;
:: thesis: verum

end;

suppose A7: ( 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, A5, Def10
.= dist b2,b1 by A3, METRIC_1:3
.= (well_dist a,X) . B,A by A4, A5, A7, 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 A8: ( 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
A9: ( A = [y1,b1] & ( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) ) by Th38;
consider y2 being set , b2 being Point of M such that
A10: ( B = [y2,b2] & ( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) ) by Th38;
consider y3 being set , b3 being Point of M such that
A11: ( C = [y3,b3] & ( ( 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 ( y1 = y2 & y1 = y3 ) ; :: thesis: (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C)

then ( dist b1,b3 = (well_dist a,X) . A,C & dist b1,b2 = (well_dist a,X) . A,B & dist b2,b3 = (well_dist a,X) . B,C & dist b1,b3 <= (dist b1,b2) + (dist b2,b3) ) by A8, A9, A10, A11, Def10, METRIC_1:4;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) ; :: thesis: verum

end;

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

then A12: ( dist b1,b3 = (well_dist a,X) . A,C & (dist b1,a) + (dist a,b2) = (well_dist a,X) . A,B & (dist b2,a) + (dist a,b3) = (well_dist a,X) . B,C & dist b1,b2 <= (dist b1,a) + (dist a,b2) & dist b2,b3 <= (dist b2,a) + (dist a,b3) ) by A8, A9, A10, A11, Def10, METRIC_1:4;
then ( (dist b1,b2) + (dist b2,b3) <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) & dist b1,b3 <= (dist b1,b2) + (dist b2,b3) ) by A8, METRIC_1:4, XREAL_1:9;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A12, XXREAL_0:2; :: thesis: verum

end;

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

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

end;

suppose ( 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)

then A14: ( (dist b1,a) + (dist a,b3) = (well_dist a,X) . A,C & (dist b1,a) + (dist a,b2) = (well_dist a,X) . A,B & (dist b2,a) + (dist a,b3) = (well_dist a,X) . B,C ) by A9, A10, A11, Def10;
( 0 <= dist a,b2 & 0 <= dist b2,a ) by A8, METRIC_1:5;
then ( (dist b1,a) + 0 <= (well_dist a,X) . A,B & 0 + (dist a,b3) <= (well_dist a,X) . B,C ) by A14, XREAL_1:8;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A14, XREAL_1:9; :: thesis: verum

end;

suppose ( 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)

then A15: ( (dist b1,a) + (dist a,b3) = (well_dist a,X) . A,C & (dist b1,a) + (dist a,b2) = (well_dist a,X) . A,B & dist b2,b3 = (well_dist a,X) . B,C & dist a,b3 <= (dist a,b2) + (dist b2,b3) ) by A8, A9, A10, A11, Def10, METRIC_1:4;
then (well_dist a,X) . A,C <= (dist b1,a) + ((dist a,b2) + (dist b2,b3)) by XREAL_1:9;
hence (well_dist a,X) . A,C <= ((well_dist a,X) . A,B) + ((well_dist a,X) . B,C) by A15; :: 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 A16: ( 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 )
assume A17: (well_dist a,X) . A,B = 0 ; :: thesis: A = B
consider y1 being set , b1 being Point of M such that
A18: ( A = [y1,b1] & ( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) ) by Th38;
consider y2 being set , b2 being Point of M such that
A19: ( B = [y2,b2] & ( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) ) by Th38;

now

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

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

then (well_dist a,X) . A,B = dist b1,b2 by A18, A19, Def10;
hence A = B by A16, A17, A18, A19, A20, METRIC_1:2; :: thesis: verum

end;

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

then ( (well_dist a,X) . A,B = (dist b1,a) + (dist a,b2) & dist a,b2 >= 0 & dist b1,a >= 0 ) by A16, A18, A19, Def10, METRIC_1:5;
then ( dist b1,a = 0 & dist a,b2 = 0 ) by A17;
hence A = B by A16, A18, A19, 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