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 M is symmetric ; :: thesis: WellSpace (a,X) is symmetric
then reconsider M = M as symmetric MetrStruct ;
reconsider a = a as Point of M ;

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))
.= (dist (a,b1)) + (dist (b2,a))
.= (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)
.= (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