:: Metric Spaces
:: by Stanis{\l}awa Kanas, Adam Lecko and Mariusz Startek
::
:: Received May 3, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct MetrStruct  ->  1-sorted ;
aggrMetrStruct(# carrier, distance #) ->  MetrStruct ;
sel distance c1 ->  Function of [: the carrier of c1, the carrier of c1:],REAL;
end;

registration
cluster non empty strict for MetrStruct ;
existence
 ex b1 being MetrStruct st
( not b1 is empty & b1 is strict )
proofend;
end;

definition
let A, B be set ;
let f be PartFunc of [:A,B:],REAL;
let a be Element of A;
let b be Element of B;
:: original:.
redefine funcf . (a,b) ->  Real;
coherence
 f . (a,b) is Real
proofend;
end;

definition
let M be MetrStruct ;
let a, b be Element of M;
func dist (a,b) ->  Real equals :: METRIC_1:def 1
 the distance of M . (a,b);
coherence
 the distance of M . (a,b) is Real ;
end;

:: deftheorem  defines dist METRIC_1:def_1_:_
 for M being MetrStruct
for a, b being Element of M holds dist (a,b) = the distance of M . (a,b);

notation
synonym  Empty^2-to-zero for  op2 ;
end;

definition
:: original:Empty^2-to-zero
redefine func Empty^2-to-zero  ->  Function of [:1,1:],REAL;
coherence
 Empty^2-to-zero is Function of [:1,1:],REAL
proofend;
end;

Lm1:  op2 . ({},{}) = 0
proofend;

Lm2:  for x, y being Element of 1 holds
( op2 . (x,y) = 0 iff x = y )
proofend;

Lm3:  for x, y being Element of 1 holds op2 . (x,y) = op2 . (y,x)
proofend;

registration
cluster Empty^2-to-zero  ->  natural-valued for Function;
coherence
 for b1 being Function st b1 = op2 holds
b1 is natural-valued ;
end;

registration
let f be natural-valued Function;
let x, y be set ;
clusterf . (x,y) ->  natural ;
coherence
 f . (x,y) is natural ;
end;

Lm4:  for x, y, z being Element of 1 holds op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z))
proofend;

definition
let A be set ;
let f be PartFunc of [:A,A:],REAL;
attrf is Reflexive  means :Def2: :: METRIC_1:def 2
 for a being Element of A holds f . (a,a) = 0 ;
attrf is discerning  means :Def3: :: METRIC_1:def 3
 for a, b being Element of A st f . (a,b) = 0 holds
a = b;
attrf is symmetric  means :Def4: :: METRIC_1:def 4
 for a, b being Element of A holds f . (a,b) = f . (b,a);
attrf is triangle  means :Def5: :: METRIC_1:def 5
 for a, b, c being Element of A holds f . (a,c) <= (f . (a,b)) + (f . (b,c));
end;

:: deftheorem Def2 defines Reflexive METRIC_1:def_2_:_
 for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is Reflexive iff for a being Element of A holds f . (a,a) = 0 );

:: deftheorem Def3 defines discerning METRIC_1:def_3_:_
 for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is discerning iff for a, b being Element of A st f . (a,b) = 0 holds
a = b );

:: deftheorem Def4 defines symmetric METRIC_1:def_4_:_
 for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is symmetric iff for a, b being Element of A holds f . (a,b) = f . (b,a) );

:: deftheorem Def5 defines triangle METRIC_1:def_5_:_
 for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is triangle iff for a, b, c being Element of A holds f . (a,c) <= (f . (a,b)) + (f . (b,c)) );

definition
let M be MetrStruct ;
attrM is Reflexive  means :Def6: :: METRIC_1:def 6
 the distance of M is Reflexive ;
attrM is discerning  means :Def7: :: METRIC_1:def 7
 the distance of M is discerning ;
attrM is symmetric  means :Def8: :: METRIC_1:def 8
 the distance of M is symmetric ;
attrM is triangle  means :Def9: :: METRIC_1:def 9
 the distance of M is triangle ;
end;

:: deftheorem Def6 defines Reflexive METRIC_1:def_6_:_
 for M being MetrStruct holds
( M is Reflexive iff the distance of M is Reflexive );

:: deftheorem Def7 defines discerning METRIC_1:def_7_:_
 for M being MetrStruct holds
( M is discerning iff the distance of M is discerning );

:: deftheorem Def8 defines symmetric METRIC_1:def_8_:_
 for M being MetrStruct holds
( M is symmetric iff the distance of M is symmetric );

:: deftheorem Def9 defines triangle METRIC_1:def_9_:_
 for M being MetrStruct holds
( M is triangle iff the distance of M is triangle );

registration
cluster non empty strict Reflexive discerning symmetric triangle for MetrStruct ;
existence
 ex b1 being MetrStruct st
( b1 is strict &amp; b1 is Reflexive &amp; b1 is discerning &amp; b1 is symmetric &amp; b1 is triangle &amp; not b1 is empty )
proofend;
end;

definition
mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct ;
end;

theorem Th1: :: METRIC_1:1
for M being MetrStruct holds
( ( for a being Element of M holds dist (a,a) = 0 ) iff M is Reflexive )
proofend;

theorem Th2: :: METRIC_1:2
for M being MetrStruct holds
( ( for a, b being Element of M st dist (a,b) = 0 holds
a = b ) iff M is discerning )
proofend;

theorem Th3: :: METRIC_1:3
for M being MetrStruct st ( for a, b being Element of M holds dist (a,b) = dist (b,a) ) holds
M is symmetric
proofend;

theorem Th4: :: METRIC_1:4
for M being MetrStruct holds
( ( for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) iff M is triangle )
proofend;

definition
let M be symmetric MetrStruct ;
let a, b be Element of M;
:: original:dist
redefine func dist (a,b) ->  Real;
commutativity
 for a, b being Element of M holds dist (a,b) = dist (b,a)
proofend;
end;

theorem Th5: :: METRIC_1:5
for M being Reflexive symmetric triangle MetrStruct
for a, b being Element of M holds 0 <= dist (a,b)
proofend;

theorem Th6: :: METRIC_1:6
for M being MetrStruct st ( for a, b, c being Element of M holds
( ( dist (a,b) = 0 implies a = b ) &amp; ( a = b implies dist (a,b) = 0 ) &amp; dist (a,b) = dist (b,a) &amp; dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ) holds
M is MetrSpace
proofend;

theorem Th7: :: METRIC_1:7
for M being MetrSpace
for x, y being Element of M st x <> y holds
0 < dist (x,y)
proofend;

definition
let A be set ;
func discrete_dist A ->  Function of [:A,A:],REAL means :Def10: :: METRIC_1:def 10
 for x, y being Element of A holds
( it . (x,x) = 0 &amp; ( x <> y implies it . (x,y) = 1 ) );
existence
 ex b1 being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b1 . (x,x) = 0 &amp; ( x <> y implies b1 . (x,y) = 1 ) )
proofend;
uniqueness
 for b1, b2 being Function of [:A,A:],REAL st ( for x, y being Element of A holds
( b1 . (x,x) = 0 &amp; ( x <> y implies b1 . (x,y) = 1 ) ) ) &amp; ( for x, y being Element of A holds
( b2 . (x,x) = 0 &amp; ( x <> y implies b2 . (x,y) = 1 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines discrete_dist METRIC_1:def_10_:_
 for A being set
for b2 being Function of [:A,A:],REAL holds
( b2 = discrete_dist A iff for x, y being Element of A holds
( b2 . (x,x) = 0 &amp; ( x <> y implies b2 . (x,y) = 1 ) ) );

definition
let A be set ;
func DiscreteSpace A ->  strict MetrStruct  equals :: METRIC_1:def 11
 MetrStruct(# A,(discrete_dist A) #);
coherence
 MetrStruct(# A,(discrete_dist A) #) is strict MetrStruct ;
end;

:: deftheorem  defines DiscreteSpace METRIC_1:def_11_:_
 for A being set holds DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #);

registration
let A be non empty set ;
cluster DiscreteSpace A ->  non empty strict ;
coherence
 not DiscreteSpace A is empty ;
end;

registration
let A be set ;
cluster DiscreteSpace A ->  strict Reflexive discerning symmetric triangle ;
coherence
 ( DiscreteSpace A is Reflexive &amp; DiscreteSpace A is discerning &amp; DiscreteSpace A is symmetric &amp; DiscreteSpace A is triangle )
proofend;
end;

definition
func real_dist  ->  Function of [:REAL,REAL:],REAL means :Def12: :: METRIC_1:def 12
 for x, y being Element of REAL holds it . (x,y) = abs (x - y);
existence
 ex b1 being Function of [:REAL,REAL:],REAL st
for x, y being Element of REAL holds b1 . (x,y) = abs (x - y)
proofend;
uniqueness
 for b1, b2 being Function of [:REAL,REAL:],REAL st ( for x, y being Element of REAL holds b1 . (x,y) = abs (x - y) ) &amp; ( for x, y being Element of REAL holds b2 . (x,y) = abs (x - y) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines real_dist METRIC_1:def_12_:_
 for b1 being Function of [:REAL,REAL:],REAL holds
( b1 = real_dist iff for x, y being Element of REAL holds b1 . (x,y) = abs (x - y) );

theorem Th8: :: METRIC_1:8
for x, y being Element of REAL holds
( real_dist . (x,y) = 0 iff x = y )
proofend;

theorem Th9: :: METRIC_1:9
for x, y being Element of REAL holds real_dist . (x,y) = real_dist . (y,x)
proofend;

theorem Th10: :: METRIC_1:10
for x, y, z being Element of REAL holds real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y))
proofend;

definition
func RealSpace  ->  strict MetrStruct  equals :: METRIC_1:def 13
 MetrStruct(# REAL,real_dist #);
coherence
 MetrStruct(# REAL,real_dist #) is strict MetrStruct ;
end;

:: deftheorem  defines RealSpace METRIC_1:def_13_:_
 RealSpace = MetrStruct(# REAL,real_dist #);

registration
cluster RealSpace  ->  non empty strict ;
coherence
 not RealSpace is empty ;
end;

registration
cluster RealSpace  ->  strict Reflexive discerning symmetric triangle ;
coherence
 ( RealSpace is Reflexive &amp; RealSpace is discerning &amp; RealSpace is symmetric &amp; RealSpace is triangle )
proofend;
end;

definition
let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func Ball (p,r) ->  Subset of M means :Def14: :: METRIC_1:def 14
it =  {  q where q is Element of M : dist (p,q) < r  }   if  not M is empty
otherwise it is empty ;
existence
 ( ( not M is empty implies ex b1 being Subset of M st b1 =  {  q where q is Element of M : dist (p,q) < r  }  ) &amp; ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proofend;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty &amp; b1 =  {  q where q is Element of M : dist (p,q) < r  }  &amp; b2 =  {  q where q is Element of M : dist (p,q) < r  }  implies b1 = b2 ) &amp; ( M is empty &amp; b1 is empty &amp; b2 is empty implies b1 = b2 ) );
;
end;

:: deftheorem Def14 defines Ball METRIC_1:def_14_:_
 for M being MetrStruct
for p being Element of M
for r being real number
for b4 being Subset of M holds
( ( not M is empty implies ( b4 = Ball (p,r) iff b4 =  {  q where q is Element of M : dist (p,q) < r  }  ) ) &amp; ( M is empty implies ( b4 = Ball (p,r) iff b4 is empty ) ) );

definition
let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func cl_Ball (p,r) ->  Subset of M means :Def15: :: METRIC_1:def 15
it =  {  q where q is Element of M : dist (p,q) <= r  }   if  not M is empty
otherwise it is empty ;
existence
 ( ( not M is empty implies ex b1 being Subset of M st b1 =  {  q where q is Element of M : dist (p,q) <= r  }  ) &amp; ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proofend;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty &amp; b1 =  {  q where q is Element of M : dist (p,q) <= r  }  &amp; b2 =  {  q where q is Element of M : dist (p,q) <= r  }  implies b1 = b2 ) &amp; ( M is empty &amp; b1 is empty &amp; b2 is empty implies b1 = b2 ) );
;
end;

:: deftheorem Def15 defines cl_Ball METRIC_1:def_15_:_
 for M being MetrStruct
for p being Element of M
for r being real number
for b4 being Subset of M holds
( ( not M is empty implies ( b4 = cl_Ball (p,r) iff b4 =  {  q where q is Element of M : dist (p,q) <= r  }  ) ) &amp; ( M is empty implies ( b4 = cl_Ball (p,r) iff b4 is empty ) ) );

definition
let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func Sphere (p,r) ->  Subset of M means :Def16: :: METRIC_1:def 16
it =  {  q where q is Element of M : dist (p,q) = r  }   if  not M is empty
otherwise it is empty ;
existence
 ( ( not M is empty implies ex b1 being Subset of M st b1 =  {  q where q is Element of M : dist (p,q) = r  }  ) &amp; ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proofend;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty &amp; b1 =  {  q where q is Element of M : dist (p,q) = r  }  &amp; b2 =  {  q where q is Element of M : dist (p,q) = r  }  implies b1 = b2 ) &amp; ( M is empty &amp; b1 is empty &amp; b2 is empty implies b1 = b2 ) );
;
end;

:: deftheorem Def16 defines Sphere METRIC_1:def_16_:_
 for M being MetrStruct
for p being Element of M
for r being real number
for b4 being Subset of M holds
( ( not M is empty implies ( b4 = Sphere (p,r) iff b4 =  {  q where q is Element of M : dist (p,q) = r  }  ) ) &amp; ( M is empty implies ( b4 = Sphere (p,r) iff b4 is empty ) ) );

theorem Th11: :: METRIC_1:11
for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in Ball (p,r) iff ( not M is empty &amp; dist (p,x) < r ) )
proofend;

theorem Th12: :: METRIC_1:12
for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in cl_Ball (p,r) iff ( not M is empty &amp; dist (p,x) <= r ) )
proofend;

theorem Th13: :: METRIC_1:13
for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in Sphere (p,r) iff ( not M is empty &amp; dist (p,x) = r ) )
proofend;

theorem Th14: :: METRIC_1:14
for r being real number
for M being MetrStruct
for p being Element of M holds Ball (p,r) c= cl_Ball (p,r)
proofend;

theorem Th15: :: METRIC_1:15
for r being real number
for M being MetrStruct
for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)
proofend;

theorem :: METRIC_1:16
for r being real number
for M being MetrStruct
for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)
proofend;

theorem :: METRIC_1:17
for r being real number
for M being non empty MetrStruct
for p being Element of M holds Ball (p,r) =  {  q where q is Element of M : dist (p,q) < r  }  by Def14;

theorem :: METRIC_1:18
for r being real number
for M being non empty MetrStruct
for p being Element of M holds cl_Ball (p,r) =  {  q where q is Element of M : dist (p,q) <= r  }  by Def15;

theorem :: METRIC_1:19
for r being real number
for M being non empty MetrStruct
for p being Element of M holds Sphere (p,r) =  {  q where q is Element of M : dist (p,q) = r  }  by Def16;

begin

theorem :: METRIC_1:20
for x being set holds Empty^2-to-zero . (x,x) = 0
proofend;

theorem Th21: :: METRIC_1:21
for x, y being Element of 1 st x <> y holds
0 < Empty^2-to-zero . (x,y)
proofend;

theorem Th22: :: METRIC_1:22
for x, y being Element of 1 holds Empty^2-to-zero . (x,y) = Empty^2-to-zero . (y,x) by Lm3;

theorem Th23: :: METRIC_1:23
for x, y, z being Element of 1 holds Empty^2-to-zero . (x,z) <= (Empty^2-to-zero . (x,y)) + (Empty^2-to-zero . (y,z)) by Lm4;

theorem Th24: :: METRIC_1:24
for x, y, z being Element of 1 holds Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z)))
proofend;

set M0 = MetrStruct(# 1,Empty^2-to-zero #);

definition
let A be non empty set ;
let f be Function of [:A,A:],REAL;
attrf is Discerning  means :Def17: :: METRIC_1:def 17
 for a, b being Element of A st a <> b holds
0 < f . (a,b);
end;

:: deftheorem Def17 defines Discerning METRIC_1:def_17_:_
 for A being non empty set
for f being Function of [:A,A:],REAL holds
( f is Discerning iff for a, b being Element of A st a <> b holds
0 < f . (a,b) );

definition
let M be non empty MetrStruct ;
attrM is Discerning  means :Def18: :: METRIC_1:def 18
 the distance of M is Discerning ;
end;

:: deftheorem Def18 defines Discerning METRIC_1:def_18_:_
 for M being non empty MetrStruct holds
( M is Discerning iff the distance of M is Discerning );

theorem Th25: :: METRIC_1:25
for M being non empty MetrStruct holds
( ( for a, b being Element of M st a <> b holds
0 < dist (a,b) ) iff M is Discerning )
proofend;

registration
cluster MetrStruct(# 1,Empty^2-to-zero #) ->  non empty ;
coherence
 not MetrStruct(# 1,Empty^2-to-zero #) is empty ;
end;

registration
cluster MetrStruct(# 1,Empty^2-to-zero #) ->  Reflexive symmetric triangle Discerning ;
coherence
 ( MetrStruct(# 1,Empty^2-to-zero #) is Reflexive &amp; MetrStruct(# 1,Empty^2-to-zero #) is symmetric &amp; MetrStruct(# 1,Empty^2-to-zero #) is Discerning &amp; MetrStruct(# 1,Empty^2-to-zero #) is triangle )
proofend;
end;

definition
let M be non empty MetrStruct ;
attrM is ultra  means :Def19: :: METRIC_1:def 19
 for a, b, c being Element of M holds dist (a,c) <= max ((dist (a,b)),(dist (b,c)));
end;

:: deftheorem Def19 defines ultra METRIC_1:def_19_:_
 for M being non empty MetrStruct holds
( M is ultra iff for a, b, c being Element of M holds dist (a,c) <= max ((dist (a,b)),(dist (b,c))) );

registration
cluster non empty strict Reflexive symmetric triangle Discerning ultra for MetrStruct ;
existence
 ex b1 being non empty MetrStruct st
( b1 is strict &amp; b1 is ultra &amp; b1 is Reflexive &amp; b1 is symmetric &amp; b1 is Discerning &amp; b1 is triangle )
proofend;
end;

theorem Th26: :: METRIC_1:26
for M being non empty Reflexive Discerning MetrStruct
for a, b being Element of M holds 0 <= dist (a,b)
proofend;

definition
mode PseudoMetricSpace is non empty Reflexive symmetric triangle MetrStruct ;
mode SemiMetricSpace is non empty Reflexive symmetric Discerning MetrStruct ;
mode NonSymmetricMetricSpace is non empty Reflexive triangle Discerning MetrStruct ;
mode UltraMetricSpace is non empty Reflexive symmetric Discerning ultra MetrStruct ;
end;

registration
cluster non empty Reflexive discerning symmetric triangle  ->  non empty Discerning for MetrStruct ;
coherence
 for b1 being non empty MetrSpace holds b1 is Discerning
proofend;
end;

registration
cluster non empty Reflexive symmetric Discerning ultra  ->  discerning triangle for MetrStruct ;
coherence
 for b1 being UltraMetricSpace holds
( b1 is triangle &amp; b1 is discerning )
proofend;
end;

definition
func Set_to_zero  ->  Function of [:2,2:],REAL equals :: METRIC_1:def 20
[:2,2:] --> 0;
coherence
 [:2,2:] --> 0 is Function of [:2,2:],REAL ;
end;

:: deftheorem  defines Set_to_zero METRIC_1:def_20_:_
 Set_to_zero = [:2,2:] --> 0;

theorem Th27: :: METRIC_1:27
for x, y being Element of 2 holds Set_to_zero . (x,y) = 0
proofend;

theorem Th28: :: METRIC_1:28
for x, y being Element of 2 holds Set_to_zero . (x,y) = Set_to_zero . (y,x)
proofend;

theorem Th29: :: METRIC_1:29
for x, y, z being Element of 2 holds Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z))
proofend;

definition
func ZeroSpace  ->  MetrStruct  equals :: METRIC_1:def 21
 MetrStruct(# 2,Set_to_zero #);
coherence
 MetrStruct(# 2,Set_to_zero #) is MetrStruct ;
end;

:: deftheorem  defines ZeroSpace METRIC_1:def_21_:_
 ZeroSpace = MetrStruct(# 2,Set_to_zero #);

registration
cluster ZeroSpace  ->  non empty strict ;
coherence
 ( ZeroSpace is strict &amp; not ZeroSpace is empty ) ;
end;

registration
cluster ZeroSpace  ->  Reflexive symmetric triangle ;
coherence
 ( ZeroSpace is Reflexive &amp; ZeroSpace is symmetric &amp; ZeroSpace is triangle )
proofend;
end;

definition
let S be MetrStruct ;
let p, q, r be Element of S;
predq is_between p,r means :Def22: :: METRIC_1:def 22
( p <> q &amp; p <> r &amp; q <> r &amp; dist (p,r) = (dist (p,q)) + (dist (q,r)) );
end;

:: deftheorem Def22 defines is_between METRIC_1:def_22_:_
 for S being MetrStruct
for p, q, r being Element of S holds
( q is_between p,r iff ( p <> q &amp; p <> r &amp; q <> r &amp; dist (p,r) = (dist (p,q)) + (dist (q,r)) ) );

theorem :: METRIC_1:30
for S being non empty Reflexive symmetric triangle MetrStruct
for p, q, r being Element of S st q is_between p,r holds
q is_between r,p
proofend;

theorem :: METRIC_1:31
for S being MetrSpace
for p, q, r being Element of S st q is_between p,r holds
( not p is_between q,r &amp; not r is_between p,q )
proofend;

theorem :: METRIC_1:32
for S being MetrSpace
for p, q, r, s being Element of S st q is_between p,r &amp; r is_between p,s holds
( q is_between p,s &amp; r is_between q,s )
proofend;

definition
let M be non empty MetrStruct ;
let p, r be Element of M;
func open_dist_Segment (p,r) ->  Subset of M equals :: METRIC_1:def 23
 {  q where q is Element of M : q is_between p,r  }  ;
coherence
  {  q where q is Element of M : q is_between p,r  }  is Subset of M
proofend;
end;

:: deftheorem  defines open_dist_Segment METRIC_1:def_23_:_
 for M being non empty MetrStruct
for p, r being Element of M holds open_dist_Segment (p,r) =  {  q where q is Element of M : q is_between p,r  }  ;

theorem :: METRIC_1:33
for M being non empty MetrSpace
for p, r, x being Element of M holds
( x in open_dist_Segment (p,r) iff x is_between p,r )
proofend;

definition
let M be non empty MetrStruct ;
let p, r be Element of M;
func close_dist_Segment (p,r) ->  Subset of M equals :: METRIC_1:def 24
 {  q where q is Element of M : q is_between p,r  }  \/ {p,r};
coherence
  {  q where q is Element of M : q is_between p,r  }  \/ {p,r} is Subset of M
proofend;
end;

:: deftheorem  defines close_dist_Segment METRIC_1:def_24_:_
 for M being non empty MetrStruct
for p, r being Element of M holds close_dist_Segment (p,r) =  {  q where q is Element of M : q is_between p,r  }  \/ {p,r};

theorem :: METRIC_1:34
for M being non empty MetrStruct
for p, r, x being Element of M holds
( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )
proofend;