:: METRIC_1 semantic presentation

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 )
proof
set A = the non empty set ;
set r = the Function of [: the non empty set , the non empty set :],REAL;
take  MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) ; ::_thesis: ( not MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty & MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict )
thus  not the carrier of MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict
thus  MetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict ; ::_thesis: verum
end;
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
proof
percases ( [a,b] in dom f or not [a,b] in dom f ) ;
suppose [a,b] in dom f ; ::_thesis: f . (a,b) is Real
hence  f . (a,b) is Real by PARTFUN1:4; ::_thesis: verum
end;
suppose not [a,b] in dom f ; ::_thesis: f . (a,b) is Real
then  f . (a,b) = 0 by FUNCT_1:def_2;
hence  f . (a,b) is Real ; ::_thesis: verum
end;
end;
end;
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
proof
 0 in REAL ;
then  ( op2 is Function of [:1,1:],1 & 1 c= REAL ) by CARD_1:49, ZFMISC_1:31;
hence  Empty^2-to-zero is Function of [:1,1:],REAL by FUNCT_2:7; ::_thesis: verum
end;
end;

Lm1:  op2 . ({},{}) = 0
proof
 [{},{}] in [:{{}},{{}}:] by ZFMISC_1:28;
hence  op2 . ({},{}) = {} by FUNCT_2:50; ::_thesis: verum
end;

Lm2:  for x, y being Element of 1 holds
( op2 . (x,y) = 0 iff x = y )
proof
let x, y be Element of 1; ::_thesis: ( op2 . (x,y) = 0 iff x = y )
 x = {} by CARD_1:49, TARSKI:def_1;
hence  ( op2 . (x,y) = 0 iff x = y ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;

Lm3:  for x, y being Element of 1 holds op2 . (x,y) = op2 . (y,x)
proof
let x, y be Element of 1; ::_thesis: op2 . (x,y) = op2 . (y,x)
 ( x = {} & y = {} ) by CARD_1:49, TARSKI:def_1;
hence  op2 . (x,y) = op2 . (y,x) ; ::_thesis: verum
end;

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))
proof
let x, y, z be Element of 1; ::_thesis: op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z))
 ( x = {} & y = {} ) by CARD_1:49, TARSKI:def_1;
hence  op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z)) by Lm1; ::_thesis: verum
end;

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 & b1 is Reflexive & b1 is discerning & b1 is symmetric & b1 is triangle & not b1 is empty )
proof
reconsider M = MetrStruct(# 1,Empty^2-to-zero #) as non empty strict MetrStruct ;
take  M ; ::_thesis: ( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty )
A1: the distance of M is discerning
proof
let a, b be Element of M; :: according to METRIC_1:def_3 ::_thesis: ( the distance of M . (a,b) = 0 implies a = b )
assume  the distance of M . (a,b) = 0 ; ::_thesis: a = b
hence  a = b by Lm2; ::_thesis: verum
end;
A2: the distance of M is symmetric
proof
let a, b be Element of M; :: according to METRIC_1:def_4 ::_thesis: the distance of M . (a,b) = the distance of M . (b,a)
thus  the distance of M . (a,b) = the distance of M . (b,a) by Lm3; ::_thesis: verum
end;
A3: the distance of M is triangle
proof
let a, b, c be Element of M; :: according to METRIC_1:def_5 ::_thesis: the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c))
thus  the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) by Lm4; ::_thesis: verum
end;
 the distance of M is Reflexive
proof
let a be Element of M; :: according to METRIC_1:def_2 ::_thesis: the distance of M . (a,a) = 0
thus  the distance of M . (a,a) = 0 by Lm2; ::_thesis: verum
end;
hence  ( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty ) by A1, A2, A3, Def6, Def7, Def8, Def9; ::_thesis: verum
end;
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 )
proof
let M be MetrStruct ; ::_thesis: ( ( for a being Element of M holds dist (a,a) = 0 ) iff M is Reflexive )
hereby  ::_thesis: ( M is Reflexive implies for a being Element of M holds dist (a,a) = 0 )
assume A1: for a being Element of M holds dist (a,a) = 0 ; ::_thesis: M is Reflexive
 the distance of M is Reflexive
proof
let a be Element of M; :: according to METRIC_1:def_2 ::_thesis: the distance of M . (a,a) = 0
the distance of M . (a,a) = dist (a,a)
.= 0 by A1 ;
hence  the distance of M . (a,a) = 0 ; ::_thesis: verum
end;
hence  M is Reflexive by Def6; ::_thesis: verum
end;
assume  M is Reflexive ; ::_thesis: for a being Element of M holds dist (a,a) = 0
then  the distance of M is Reflexive by Def6;
hence  for a being Element of M holds dist (a,a) = 0 by Def2; ::_thesis: verum
end;

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 )
proof
let M be MetrStruct ; ::_thesis: ( ( for a, b being Element of M st dist (a,b) = 0 holds
a = b ) iff M is discerning )
hereby  ::_thesis: ( M is discerning implies for a, b being Element of M st dist (a,b) = 0 holds
a = b )
assume A1: for a, b being Element of M st dist (a,b) = 0 holds
a = b ; ::_thesis: M is discerning
 the distance of M is discerning
proof
let a, b be Element of M; :: according to METRIC_1:def_3 ::_thesis: ( the distance of M . (a,b) = 0 implies a = b )
assume  the distance of M . (a,b) = 0 ; ::_thesis: a = b
then  dist (a,b) = 0 ;
hence  a = b by A1; ::_thesis: verum
end;
hence  M is discerning by Def7; ::_thesis: verum
end;
assume  M is discerning ; ::_thesis: for a, b being Element of M st dist (a,b) = 0 holds
a = b
then  the distance of M is discerning by Def7;
hence  for a, b being Element of M st dist (a,b) = 0 holds
a = b by Def3; ::_thesis: verum
end;

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
proof
let M be MetrStruct ; ::_thesis: ( ( for a, b being Element of M holds dist (a,b) = dist (b,a) ) implies M is symmetric )
assume A1: for a, b being Element of M holds dist (a,b) = dist (b,a) ; ::_thesis: M is symmetric
 the distance of M is symmetric
proof
let a, b be Element of M; :: according to METRIC_1:def_4 ::_thesis: the distance of M . (a,b) = the distance of M . (b,a)
thus  the distance of M . (a,b) = dist (a,b)
.= dist (b,a) by A1
.= the distance of M . (b,a) ; ::_thesis: verum
end;
hence  M is symmetric by Def8; ::_thesis: verum
end;

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 )
proof
let M be MetrStruct ; ::_thesis: ( ( for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) iff M is triangle )
hereby  ::_thesis: ( M is triangle implies for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
assume A1: for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ; ::_thesis: M is triangle
 the distance of M is triangle
proof
let a, b, c be Element of M; :: according to METRIC_1:def_5 ::_thesis: the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c))
A2: the distance of M . (b,c) = dist (b,c) ;
 ( the distance of M . (a,b) = dist (a,b) & the distance of M . (a,c) = dist (a,c) ) ;
hence  the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) by A1, A2; ::_thesis: verum
end;
hence  M is triangle by Def9; ::_thesis: verum
end;
assume A3: M is triangle ; ::_thesis: for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c))
let a, b, c be Element of M; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
 the distance of M is triangle by A3, Def9;
hence  dist (a,c) <= (dist (a,b)) + (dist (b,c)) by Def5; ::_thesis: verum
end;

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)
proof
 the distance of M is symmetric by Def8;
hence  for a, b being Element of M holds dist (a,b) = dist (b,a) by Def4; ::_thesis: verum
end;
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)
proof
let M be Reflexive symmetric triangle MetrStruct ; ::_thesis: for a, b being Element of M holds 0 <= dist (a,b)
let a, b be Element of M; ::_thesis: 0 <= dist (a,b)
A1: (1 / 2) * (dist (a,a)) = (1 / 2) * 0 by Th1;
 ( dist (a,a) <= (dist (a,b)) + (dist (b,a)) & dist (a,b) = (1 / 2) * ((1 * (dist (a,b))) + (1 * (dist (a,b)))) ) by Th4;
hence  0 <= dist (a,b) by A1, XREAL_1:64; ::_thesis: verum
end;

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 ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ) holds
M is MetrSpace
proof
let M be MetrStruct ; ::_thesis: ( ( for a, b, c being Element of M holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ) implies M is MetrSpace )
assume A1: for a, b, c being Element of M holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ; ::_thesis: M is MetrSpace
A2: the distance of M is symmetric
proof
let a, b be Element of M; :: according to METRIC_1:def_4 ::_thesis: the distance of M . (a,b) = the distance of M . (b,a)
the distance of M . (a,b) = dist (a,b)
.= dist (b,a) by A1
.= the distance of M . (b,a) ;
hence  the distance of M . (a,b) = the distance of M . (b,a) ; ::_thesis: verum
end;
A3: the distance of M is triangle
proof
let a, b, c be Element of M; :: according to METRIC_1:def_5 ::_thesis: the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c))
A4: the distance of M . (b,c) = dist (b,c) ;
 ( the distance of M . (a,c) = dist (a,c) & the distance of M . (a,b) = dist (a,b) ) ;
hence  the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c)) by A1, A4; ::_thesis: verum
end;
A5: the distance of M is discerning
proof
let a, b be Element of M; :: according to METRIC_1:def_3 ::_thesis: ( the distance of M . (a,b) = 0 implies a = b )
assume  the distance of M . (a,b) = 0 ; ::_thesis: a = b
then  dist (a,b) = 0 ;
hence  a = b by A1; ::_thesis: verum
end;
 the distance of M is Reflexive
proof
let a be Element of M; :: according to METRIC_1:def_2 ::_thesis: the distance of M . (a,a) = 0
the distance of M . (a,a) = dist (a,a)
.= 0 by A1 ;
hence  the distance of M . (a,a) = 0 ; ::_thesis: verum
end;
hence  M is MetrSpace by A5, A2, A3, Def6, Def7, Def8, Def9; ::_thesis: verum
end;

theorem Th7: :: METRIC_1:7
for M being MetrSpace
for x, y being Element of M st x <> y holds
0 < dist (x,y)
proof
let M be MetrSpace; ::_thesis: for x, y being Element of M st x <> y holds
0 < dist (x,y)
let x, y be Element of M; ::_thesis: ( x <> y implies 0 < dist (x,y) )
A1: dist (x,y) >= 0 by Th5;
assume  x <> y ; ::_thesis: 0 < dist (x,y)
then  dist (x,y) <> 0 by Th2;
hence  0 < dist (x,y) by A1, XXREAL_0:1; ::_thesis: verum
end;

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 & ( 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 & ( x <> y implies b1 . (x,y) = 1 ) )
proof
percases ( A is empty or not A is empty ) ;
supposeA1: A is empty ; ::_thesis: ex b1 being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) )
then  [:A,A:] = {} by ZFMISC_1:90;
then reconsider f = {} as Function of [:A,A:],REAL by RELSET_1:12;
take  f ; ::_thesis: for x, y being Element of A holds
( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) )
let x, y be Element of A; ::_thesis: ( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) )
thus  f . (x,x) = 0 ; ::_thesis: ( x <> y implies f . (x,y) = 1 )
x = {} by A1, SUBSET_1:def_1
.= y by A1, SUBSET_1:def_1 ;
hence  ( x <> y implies f . (x,y) = 1 ) ; ::_thesis: verum
end;
supposeA2: not A is empty ; ::_thesis: ex b1 being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) )
 ( {0,1} c= REAL & rng (chi (([:A,A:] \ (id A)),[:A,A:])) c= {0,1} ) by FUNCT_3:39, ZFMISC_1:32;
then A3: rng (chi (([:A,A:] \ (id A)),[:A,A:])) c= REAL by XBOOLE_1:1;
 dom (chi (([:A,A:] \ (id A)),[:A,A:])) = [:A,A:] by FUNCT_3:def_3;
then reconsider char = chi (([:A,A:] \ (id A)),[:A,A:]) as Function of [:A,A:],REAL by A3, RELSET_1:4;
take  char ; ::_thesis: for x, y being Element of A holds
( char . (x,x) = 0 & ( x <> y implies char . (x,y) = 1 ) )
let x, y be Element of A; ::_thesis: ( char . (x,x) = 0 & ( x <> y implies char . (x,y) = 1 ) )
[:A,A:] \ ([:A,A:] \ (id A)) = [:A,A:] /\ (id A) by XBOOLE_1:48
.= id A by XBOOLE_1:28 ;
then  [x,x] in [:A,A:] \ ([:A,A:] \ (id A)) by A2, RELAT_1:def_10;
hence  char . (x,x) = 0 by FUNCT_3:37; ::_thesis: ( x <> y implies char . (x,y) = 1 )
assume  x <> y ; ::_thesis: char . (x,y) = 1
then A4: not [x,y] in id A by RELAT_1:def_10;
 [x,y] in [:A,A:] by A2, ZFMISC_1:def_2;
then  [x,y] in [:A,A:] \ (id A) by A4, XBOOLE_0:def_5;
hence  char . (x,y) = 1 by FUNCT_3:def_3; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being Function of [:A,A:],REAL st ( for x, y being Element of A holds
( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds
( b2 . (x,x) = 0 & ( x <> y implies b2 . (x,y) = 1 ) ) ) holds
b1 = b2
proof
let f, f9 be Function of [:A,A:],REAL; ::_thesis: ( ( for x, y being Element of A holds
( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds
( f9 . (x,x) = 0 & ( x <> y implies f9 . (x,y) = 1 ) ) ) implies f = f9 )
assume that
A5: for x, y being Element of A holds
( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) and
A6: for x, y being Element of A holds
( f9 . (x,x) = 0 & ( x <> y implies f9 . (x,y) = 1 ) ) ; ::_thesis: f = f9
now__::_thesis:_for_x,_y_being_Element_of_A_holds_f_._(x,y)_=_f9_._(x,y)
let x, y be Element of A; ::_thesis: f . (x,y) = f9 . (x,y)
now__::_thesis:_f_._(x,y)_=_f9_._(x,y)
percases ( x = y or x <> y ) ;
supposeA7: x = y ; ::_thesis: f . (x,y) = f9 . (x,y)
hence f . (x,y) = 0 by A5
.= f9 . (x,y) by A6, A7 ;
::_thesis: verum
end;
supposeA8: x <> y ; ::_thesis: f . (x,y) = f9 . (x,y)
hence f . (x,y) = 1 by A5
.= f9 . (x,y) by A6, A8 ;
::_thesis: verum
end;
end;
end;
hence  f . (x,y) = f9 . (x,y) ; ::_thesis: verum
end;
hence  f = f9 by BINOP_1:2; ::_thesis: verum
end;
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 & ( 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 & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle )
proof
set M = MetrStruct(# A,(discrete_dist A) #);
A1: the distance of MetrStruct(# A,(discrete_dist A) #) is discerning
proof
let a, b be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_3 ::_thesis: ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 0 implies a = b )
assume  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 0 ; ::_thesis: a = b
hence  a = b by Def10; ::_thesis: verum
end;
A2: the distance of MetrStruct(# A,(discrete_dist A) #) is symmetric
proof
let a, b be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_4 ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a)
now__::_thesis:_the_distance_of_MetrStruct(#_A,(discrete_dist_A)_#)_._(a,b)_=_the_distance_of_MetrStruct(#_A,(discrete_dist_A)_#)_._(b,a)
percases ( a <> b or a = b ) ;
supposeA3: a <> b ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a)
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 1 by Def10
.= the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) by A3, Def10 ;
::_thesis: verum
end;
suppose a = b ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a)
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) ; ::_thesis: verum
end;
end;
end;
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) ; ::_thesis: verum
end;
A4: the distance of MetrStruct(# A,(discrete_dist A) #) is triangle
proof
let a, b, c be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_5 ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
A5: ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 0 iff a = b ) by Def10;
percases ( ( a = b & a = c ) or ( a = b & a <> c ) or ( a = c & a <> b ) or ( b = c & a <> c ) or ( a <> b & a <> c & b <> c ) ) ;
suppose ( a = b & a = c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A5; ::_thesis: verum
end;
suppose ( a = b & a <> c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A5; ::_thesis: verum
end;
supposeA6: ( a = c & a <> b ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
then A7: the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c) = 1 by Def10;
 ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) = 0 & the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 1 ) by A6, Def10;
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A7; ::_thesis: verum
end;
supposeA8: ( b = c & a <> c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
then  the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c) = 0 by Def10;
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A8; ::_thesis: verum
end;
supposeA9: ( a <> b & a <> c & b <> c ) ; ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
then A10: the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c) = 1 by Def10;
 ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) = 1 & the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = 1 ) by A9, Def10;
hence  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c)) by A10; ::_thesis: verum
end;
end;
end;
 the distance of MetrStruct(# A,(discrete_dist A) #) is Reflexive
proof
let a be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def_2 ::_thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,a) = 0
thus  the distance of MetrStruct(# A,(discrete_dist A) #) . (a,a) = 0 by Def10; ::_thesis: verum
end;
hence  ( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle ) by A1, A2, A4, Def6, Def7, Def8, Def9; ::_thesis: verum
end;
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)
proof
deffunc H1( Element of REAL , Element of REAL ) ->  Element of REAL = abs ($1 - $2);
consider F being Function of [:REAL,REAL:],REAL such that
A1: for x, y being Element of REAL holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  F ; ::_thesis: for x, y being Element of REAL holds F . (x,y) = abs (x - y)
let x, y be Element of REAL ; ::_thesis: F . (x,y) = abs (x - y)
thus  F . (x,y) = abs (x - y) by A1; ::_thesis: verum
end;
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) ) & ( for x, y being Element of REAL holds b2 . (x,y) = abs (x - y) ) holds
b1 = b2
proof
let F1, F2 be Function of [:REAL,REAL:],REAL; ::_thesis: ( ( for x, y being Element of REAL holds F1 . (x,y) = abs (x - y) ) & ( for x, y being Element of REAL holds F2 . (x,y) = abs (x - y) ) implies F1 = F2 )
assume that
A2: for x, y being Element of REAL holds F1 . (x,y) = abs (x - y) and
A3: for x, y being Element of REAL holds F2 . (x,y) = abs (x - y) ; ::_thesis: F1 = F2
 for x, y being Element of REAL holds F1 . (x,y) = F2 . (x,y)
proof
let x, y be Element of REAL ; ::_thesis: F1 . (x,y) = F2 . (x,y)
thus F1 . (x,y) = abs (x - y) by A2
.= F2 . (x,y) by A3 ; ::_thesis: verum
end;
hence  F1 = F2 by BINOP_1:2; ::_thesis: verum
end;
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 )
proof
let x, y be Element of REAL ; ::_thesis: ( real_dist . (x,y) = 0 iff x = y )
thus  ( real_dist . (x,y) = 0 implies x = y ) ::_thesis: ( x = y implies real_dist . (x,y) = 0 )
proof
assume  real_dist . (x,y) = 0 ; ::_thesis: x = y
then  0 = abs (x - y) by Def12;
then  x - y = 0 by ABSVALUE:2;
hence  x = y ; ::_thesis: verum
end;
assume  x = y ; ::_thesis: real_dist . (x,y) = 0
then  abs (x - y) = 0 by ABSVALUE:2;
hence  real_dist . (x,y) = 0 by Def12; ::_thesis: verum
end;

theorem Th9: :: METRIC_1:9
for x, y being Element of REAL holds real_dist . (x,y) = real_dist . (y,x)
proof
let x, y be Element of REAL ; ::_thesis: real_dist . (x,y) = real_dist . (y,x)
thus real_dist . (x,y) = abs (x - y) by Def12
.= abs (- (x - y)) by COMPLEX1:52
.= abs (y - x)
.= real_dist . (y,x) by Def12 ; ::_thesis: verum
end;

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))
proof
let x, y, z be Element of REAL ; ::_thesis: real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y))
 abs (x - y) = abs ((x - z) + (z - y)) ;
then A1: abs (x - y) <= (abs (x - z)) + (abs (z - y)) by COMPLEX1:56;
 ( real_dist . (x,y) = abs (x - y) & real_dist . (x,z) = abs (x - z) ) by Def12;
hence  real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y)) by A1, Def12; ::_thesis: verum
end;

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 & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle )
proof
reconsider M = MetrStruct(# REAL,real_dist #) as non empty MetrStruct ;
 for a, b, c being Element of M holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) by Th8, Th9, Th10;
hence  ( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle ) by Th6; ::_thesis: verum
end;
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  }  ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof
reconsider X = {} as Subset of M by XBOOLE_1:2;
thus  ( not M is empty implies ex X being Subset of M st X =  {  q where q is Element of M : dist (p,q) < r  }  ) ::_thesis: ( M is empty implies ex b1 being Subset of M st b1 is empty )
proof
assume  not M is empty ; ::_thesis: ex X being Subset of M st X =  {  q where q is Element of M : dist (p,q) < r  }
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
defpred S1[ Element of M9] means  dist (p9,$1) < r;
set X =  {  q where q is Element of M9 : S1[q]  }  ;
  {  q where q is Element of M9 : S1[q]  }  c= the carrier of M9 from FRAENKEL:sch_10();
then reconsider X =  {  q where q is Element of M9 : S1[q]  }  as Subset of M ;
take  X ; ::_thesis: X =  {  q where q is Element of M : dist (p,q) < r  }
thus  X =  {  q where q is Element of M : dist (p,q) < r  }  ; ::_thesis: verum
end;
assume  M is empty ; ::_thesis: ex b1 being Subset of M st b1 is empty
take  X ; ::_thesis: X is empty
thus  X is empty ; ::_thesis: verum
end;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & b1 =  {  q where q is Element of M : dist (p,q) < r  }  & b2 =  {  q where q is Element of M : dist (p,q) < r  }  implies b1 = b2 ) & ( M is empty & b1 is empty & 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  }  ) ) & ( 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  }  ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof
reconsider X = {} as Subset of M by XBOOLE_1:2;
thus  ( not M is empty implies ex X being Subset of M st X =  {  q where q is Element of M : dist (p,q) <= r  }  ) ::_thesis: ( M is empty implies ex b1 being Subset of M st b1 is empty )
proof
assume  not M is empty ; ::_thesis: ex X being Subset of M st X =  {  q where q is Element of M : dist (p,q) <= r  }
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
defpred S1[ Element of M9] means  dist (p9,$1) <= r;
set X =  {  q where q is Element of M9 : S1[q]  }  ;
  {  q where q is Element of M9 : S1[q]  }  c= the carrier of M9 from FRAENKEL:sch_10();
then reconsider X =  {  q where q is Element of M9 : S1[q]  }  as Subset of M ;
take  X ; ::_thesis: X =  {  q where q is Element of M : dist (p,q) <= r  }
thus  X =  {  q where q is Element of M : dist (p,q) <= r  }  ; ::_thesis: verum
end;
assume  M is empty ; ::_thesis: ex b1 being Subset of M st b1 is empty
take  X ; ::_thesis: X is empty
thus  X is empty ; ::_thesis: verum
end;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & b1 =  {  q where q is Element of M : dist (p,q) <= r  }  & b2 =  {  q where q is Element of M : dist (p,q) <= r  }  implies b1 = b2 ) & ( M is empty & b1 is empty & 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  }  ) ) & ( 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  }  ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof
reconsider X = {} as Subset of M by XBOOLE_1:2;
thus  ( not M is empty implies ex X being Subset of M st X =  {  q where q is Element of M : dist (p,q) = r  }  ) ::_thesis: ( M is empty implies ex b1 being Subset of M st b1 is empty )
proof
assume  not M is empty ; ::_thesis: ex X being Subset of M st X =  {  q where q is Element of M : dist (p,q) = r  }
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
defpred S1[ Element of M9] means  dist (p9,$1) = r;
set X =  {  q where q is Element of M9 : S1[q]  }  ;
  {  q where q is Element of M9 : S1[q]  }  c= the carrier of M9 from FRAENKEL:sch_10();
then reconsider X =  {  q where q is Element of M9 : S1[q]  }  as Subset of M ;
take  X ; ::_thesis: X =  {  q where q is Element of M : dist (p,q) = r  }
thus  X =  {  q where q is Element of M : dist (p,q) = r  }  ; ::_thesis: verum
end;
assume  M is empty ; ::_thesis: ex b1 being Subset of M st b1 is empty
take  X ; ::_thesis: X is empty
thus  X is empty ; ::_thesis: verum
end;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & b1 =  {  q where q is Element of M : dist (p,q) = r  }  & b2 =  {  q where q is Element of M : dist (p,q) = r  }  implies b1 = b2 ) & ( M is empty & b1 is empty & 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  }  ) ) & ( 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 & dist (p,x) < r ) )
proof
let r be real number ; ::_thesis: for M being MetrStruct
for p, x being Element of M holds
( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) )
let M be MetrStruct ; ::_thesis: for p, x being Element of M holds
( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) )
let p, x be Element of M; ::_thesis: ( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) )
hereby  ::_thesis: ( not M is empty & dist (p,x) < r implies x in Ball (p,r) )
assume A1: x in Ball (p,r) ; ::_thesis: ( not M is empty & dist (p,x) < r )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
 x in  {  q where q is Element of M9 : dist (p9,q) < r  }  by A1, Def14;
then  ex q being Element of M st
( x = q & dist (p,q) < r ) ;
hence  ( not M is empty & dist (p,x) < r ) by A1; ::_thesis: verum
end;
assume  not M is empty ; ::_thesis: ( not dist (p,x) < r or x in Ball (p,r) )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
assume  dist (p,x) < r ; ::_thesis: x in Ball (p,r)
then  x in  {  q where q is Element of M9 : dist (p9,q) < r  }  ;
hence  x in Ball (p,r) by Def14; ::_thesis: verum
end;

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 & dist (p,x) <= r ) )
proof
let r be real number ; ::_thesis: for M being MetrStruct
for p, x being Element of M holds
( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) )
let M be MetrStruct ; ::_thesis: for p, x being Element of M holds
( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) )
let p, x be Element of M; ::_thesis: ( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) )
hereby  ::_thesis: ( not M is empty & dist (p,x) <= r implies x in cl_Ball (p,r) )
assume A1: x in cl_Ball (p,r) ; ::_thesis: ( not M is empty & dist (p,x) <= r )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
 x in  {  q where q is Element of M9 : dist (p9,q) <= r  }  by A1, Def15;
then  ex q being Element of M st
( x = q & dist (p,q) <= r ) ;
hence  ( not M is empty & dist (p,x) <= r ) by A1; ::_thesis: verum
end;
assume  not M is empty ; ::_thesis: ( not dist (p,x) <= r or x in cl_Ball (p,r) )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
assume  dist (p,x) <= r ; ::_thesis: x in cl_Ball (p,r)
then  x in  {  q where q is Element of M9 : dist (p9,q) <= r  }  ;
hence  x in cl_Ball (p,r) by Def15; ::_thesis: verum
end;

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 & dist (p,x) = r ) )
proof
let r be real number ; ::_thesis: for M being MetrStruct
for p, x being Element of M holds
( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )
let M be MetrStruct ; ::_thesis: for p, x being Element of M holds
( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )
let p, x be Element of M; ::_thesis: ( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )
hereby  ::_thesis: ( not M is empty & dist (p,x) = r implies x in Sphere (p,r) )
assume A1: x in Sphere (p,r) ; ::_thesis: ( not M is empty & dist (p,x) = r )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
 x in  {  q where q is Element of M9 : dist (p9,q) = r  }  by A1, Def16;
then  ex q being Element of M st
( x = q & dist (p,q) = r ) ;
hence  ( not M is empty & dist (p,x) = r ) by A1; ::_thesis: verum
end;
assume  not M is empty ; ::_thesis: ( not dist (p,x) = r or x in Sphere (p,r) )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
assume  dist (p,x) = r ; ::_thesis: x in Sphere (p,r)
then  x in  {  q where q is Element of M9 : dist (p9,q) = r  }  ;
hence  x in Sphere (p,r) by Def16; ::_thesis: verum
end;

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)
proof
let r be real number ; ::_thesis: for M being MetrStruct
for p being Element of M holds Ball (p,r) c= cl_Ball (p,r)
let M be MetrStruct ; ::_thesis: for p being Element of M holds Ball (p,r) c= cl_Ball (p,r)
let p be Element of M; ::_thesis: Ball (p,r) c= cl_Ball (p,r)
percases ( not M is empty or M is empty ) ;
supposeA1: not M is empty ; ::_thesis: Ball (p,r) c= cl_Ball (p,r)
now__::_thesis:_for_x_being_Element_of_M_st_x_in_Ball_(p,r)_holds_
x_in_cl_Ball_(p,r)
let x be Element of M; ::_thesis: ( x in Ball (p,r) implies x in cl_Ball (p,r) )
assume  x in Ball (p,r) ; ::_thesis: x in cl_Ball (p,r)
then  dist (p,x) <= r by Th11;
then  x in  {  q where q is Element of M : dist (p,q) <= r  }  ;
hence  x in cl_Ball (p,r) by A1, Def15; ::_thesis: verum
end;
hence  Ball (p,r) c= cl_Ball (p,r) by SUBSET_1:2; ::_thesis: verum
end;
supposeA2: M is empty ; ::_thesis: Ball (p,r) c= cl_Ball (p,r)
then  Ball (p,r) is empty by Def14;
hence  Ball (p,r) c= cl_Ball (p,r) by A2, Def15; ::_thesis: verum
end;
end;
end;

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)
proof
let r be real number ; ::_thesis: for M being MetrStruct
for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)
let M be MetrStruct ; ::_thesis: for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)
let p be Element of M; ::_thesis: Sphere (p,r) c= cl_Ball (p,r)
percases ( not M is empty or M is empty ) ;
supposeA1: not M is empty ; ::_thesis: Sphere (p,r) c= cl_Ball (p,r)
now__::_thesis:_for_x_being_Element_of_M_st_x_in_Sphere_(p,r)_holds_
x_in_cl_Ball_(p,r)
let x be Element of M; ::_thesis: ( x in Sphere (p,r) implies x in cl_Ball (p,r) )
assume  x in Sphere (p,r) ; ::_thesis: x in cl_Ball (p,r)
then  dist (p,x) = r by Th13;
then  x in  {  q where q is Element of M : dist (p,q) <= r  }  ;
hence  x in cl_Ball (p,r) by Def15, A1; ::_thesis: verum
end;
hence  Sphere (p,r) c= cl_Ball (p,r) by SUBSET_1:2; ::_thesis: verum
end;
supposeA2: M is empty ; ::_thesis: Sphere (p,r) c= cl_Ball (p,r)
then  Sphere (p,r) is empty by Def16;
hence  Sphere (p,r) c= cl_Ball (p,r) by A2, Def15; ::_thesis: verum
end;
end;
end;

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)
proof
let r be real number ; ::_thesis: for M being MetrStruct
for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)
let M be MetrStruct ; ::_thesis: for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)
let p be Element of M; ::_thesis: (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)
 ( Sphere (p,r) c= cl_Ball (p,r) & Ball (p,r) c= cl_Ball (p,r) ) by Th14, Th15;
hence  (Sphere (p,r)) \/ (Ball (p,r)) c= cl_Ball (p,r) by XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r))
percases ( not M is empty or M is empty ) ;
supposeA1: not M is empty ; ::_thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r))
now__::_thesis:_for_x_being_Element_of_M_st_x_in_cl_Ball_(p,r)_holds_
x_in_(Sphere_(p,r))_\/_(Ball_(p,r))
let x be Element of M; ::_thesis: ( x in cl_Ball (p,r) implies x in (Sphere (p,r)) \/ (Ball (p,r)) )
assume  x in cl_Ball (p,r) ; ::_thesis: x in (Sphere (p,r)) \/ (Ball (p,r))
then A2: dist (p,x) <= r by Th12;
now__::_thesis:_(_(_dist_(p,x)_<_r_&_x_in_Ball_(p,r)_)_or_(_dist_(p,x)_=_r_&_x_in_Sphere_(p,r)_)_)
percases ( dist (p,x) < r or dist (p,x) = r ) by A2, XXREAL_0:1;
case dist (p,x) < r ; ::_thesis: x in Ball (p,r)
hence  x in Ball (p,r) by A1, Th11; ::_thesis: verum
end;
case dist (p,x) = r ; ::_thesis: x in Sphere (p,r)
hence  x in Sphere (p,r) by A1, Th13; ::_thesis: verum
end;
end;
end;
hence  x in (Sphere (p,r)) \/ (Ball (p,r)) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) by SUBSET_1:2; ::_thesis: verum
end;
supposeA3: M is empty ; ::_thesis: cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r))
then  ( Ball (p,r) is empty & cl_Ball (p,r) is empty ) by Def14, Def15;
hence  cl_Ball (p,r) c= (Sphere (p,r)) \/ (Ball (p,r)) by A3, Def16; ::_thesis: verum
end;
end;
end;

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
proof
let x be set ; ::_thesis: Empty^2-to-zero . (x,x) = 0
percases ( [x,x] in [:1,1:] or not [x,x] in [:1,1:] ) ;
suppose [x,x] in [:1,1:] ; ::_thesis: Empty^2-to-zero . (x,x) = 0
hence  Empty^2-to-zero . (x,x) = 0 by CARD_1:49, FUNCT_2:50; ::_thesis: verum
end;
suppose not [x,x] in [:1,1:] ; ::_thesis: Empty^2-to-zero . (x,x) = 0
then  not [x,x] in dom Empty^2-to-zero by FUNCT_2:def_1;
hence  Empty^2-to-zero . (x,x) = 0 by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;

theorem Th21: :: METRIC_1:21
for x, y being Element of 1 st x <> y holds
0 < Empty^2-to-zero . (x,y)
proof
let x, y be Element of 1; ::_thesis: ( x <> y implies 0 < Empty^2-to-zero . (x,y) )
 x = {} by CARD_1:49, TARSKI:def_1;
hence  ( x <> y implies 0 < Empty^2-to-zero . (x,y) ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;

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)))
proof
let x, y, z be Element of 1; ::_thesis: Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z)))
A1: z = {} by CARD_1:49, TARSKI:def_1;
 ( x = {} & y = {} ) by CARD_1:49, TARSKI:def_1;
hence  Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z))) by A1; ::_thesis: verum
end;

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 )
proof
let M be non empty MetrStruct ; ::_thesis: ( ( for a, b being Element of M st a <> b holds
0 < dist (a,b) ) iff M is Discerning )
hereby  ::_thesis: ( M is Discerning implies for a, b being Element of M st a <> b holds
0 < dist (a,b) )
assume A1: for a, b being Element of M st a <> b holds
0 < dist (a,b) ; ::_thesis: M is Discerning
 the distance of M is Discerning
proof
let a, b be Element of M; :: according to METRIC_1:def_17 ::_thesis: ( a <> b implies 0 < the distance of M . (a,b) )
assume  a <> b ; ::_thesis: 0 < the distance of M . (a,b)
then  0 < dist (a,b) by A1;
hence  0 < the distance of M . (a,b) ; ::_thesis: verum
end;
hence  M is Discerning by Def18; ::_thesis: verum
end;
assume  M is Discerning ; ::_thesis: for a, b being Element of M st a <> b holds
0 < dist (a,b)
then  the distance of M is Discerning by Def18;
hence  for a, b being Element of M st a <> b holds
0 < dist (a,b) by Def17; ::_thesis: verum
end;

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 & MetrStruct(# 1,Empty^2-to-zero #) is symmetric & MetrStruct(# 1,Empty^2-to-zero #) is Discerning & MetrStruct(# 1,Empty^2-to-zero #) is triangle )
proof
A1: for x being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,x) = 0 by Lm2;
A2: for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,y) = dist (y,x) by Th22;
A3: for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) st x <> y holds
0 < dist (x,y) by Th21;
 for x, y, z being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,z) <= (dist (x,y)) + (dist (y,z)) by Th23;
hence  ( MetrStruct(# 1,Empty^2-to-zero #) is Reflexive & MetrStruct(# 1,Empty^2-to-zero #) is symmetric & MetrStruct(# 1,Empty^2-to-zero #) is Discerning & MetrStruct(# 1,Empty^2-to-zero #) is triangle ) by A2, A1, A3, Th25, Th1, Th3, Th4; ::_thesis: verum
end;
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 & b1 is ultra & b1 is Reflexive & b1 is symmetric & b1 is Discerning & b1 is triangle )
proof
take M0 = MetrStruct(# 1,Empty^2-to-zero #); ::_thesis: ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle )
 M0 is ultra
proof
let x, y, z be Element of M0; :: according to METRIC_1:def_19 ::_thesis: dist (x,z) <= max ((dist (x,y)),(dist (y,z)))
thus  dist (x,z) <= max ((dist (x,y)),(dist (y,z))) by Th24; ::_thesis: verum
end;
hence  ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle ) ; ::_thesis: verum
end;
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)
proof
let M be non empty Reflexive Discerning MetrStruct ; ::_thesis: for a, b being Element of M holds 0 <= dist (a,b)
let a, b be Element of M; ::_thesis: 0 <= dist (a,b)
now__::_thesis:_0_<=_dist_(a,b)
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: 0 <= dist (a,b)
hence  0 <= dist (a,b) by Th1; ::_thesis: verum
end;
suppose a <> b ; ::_thesis: 0 <= dist (a,b)
hence  0 <= dist (a,b) by Th25; ::_thesis: verum
end;
end;
end;
hence  0 <= dist (a,b) ; ::_thesis: verum
end;

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
proof
let M be non empty MetrSpace; ::_thesis: M is Discerning
 for a, b being Element of M st a <> b holds
0 < dist (a,b) by Th7;
hence  M is Discerning by Th25; ::_thesis: verum
end;
end;

registration
cluster non empty Reflexive symmetric Discerning ultra  ->  discerning triangle for MetrStruct ;
coherence
 for b1 being UltraMetricSpace holds
( b1 is triangle & b1 is discerning )
proof
let M be UltraMetricSpace; ::_thesis: ( M is triangle & M is discerning )
now__::_thesis:_for_x,_y,_z_being_Element_of_M_holds_
(_(_dist_(x,y)_=_0_implies_x_=_y_)_&_(_x_=_y_implies_dist_(x,y)_=_0_)_&_dist_(x,y)_=_dist_(y,x)_&_dist_(x,z)_<=_(dist_(x,y))_+_(dist_(y,z))_)
let x, y, z be Element of M; ::_thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
thus  ( dist (x,y) = 0 iff x = y ) by Th25, Th1; ::_thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
thus  dist (x,y) = dist (y,x) ; ::_thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
 ( 0 <= dist (x,y) & 0 <= dist (y,z) ) by Th26;
then A1: max ((dist (x,y)),(dist (y,z))) <= (dist (x,y)) + (dist (y,z)) by SQUARE_1:2;
 dist (x,z) <= max ((dist (x,y)),(dist (y,z))) by Def19;
hence  dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, XXREAL_0:2; ::_thesis: verum
end;
hence  ( M is triangle & M is discerning ) by Th6; ::_thesis: verum
end;
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
proof
let x, y be Element of 2; ::_thesis: Set_to_zero . (x,y) = 0
A1: [x,y] in [:2,2:] by ZFMISC_1:87;
thus Set_to_zero . (x,y) = Set_to_zero . [x,y]
.= 0 by A1, FUNCOP_1:7 ; ::_thesis: verum
end;

theorem Th28: :: METRIC_1:28
for x, y being Element of 2 holds Set_to_zero . (x,y) = Set_to_zero . (y,x)
proof
let x, y be Element of 2; ::_thesis: Set_to_zero . (x,y) = Set_to_zero . (y,x)
Set_to_zero . (x,y) = 0 by Th27
.= Set_to_zero . (y,x) by Th27 ;
hence  Set_to_zero . (x,y) = Set_to_zero . (y,x) ; ::_thesis: verum
end;

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))
proof
let x, y, z be Element of 2; ::_thesis: Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z))
 ( Set_to_zero . (x,y) = 0 & Set_to_zero . (y,z) = 0 ) by Th27;
hence  Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z)) by Th27; ::_thesis: verum
end;

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 & not ZeroSpace is empty ) ;
end;

registration
cluster ZeroSpace  ->  Reflexive symmetric triangle ;
coherence
 ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle )
proof
set M = MetrStruct(# 2,Set_to_zero #);
A1: for x, y, z being Element of MetrStruct(# 2,Set_to_zero #) holds
( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) ) by Th28, Th29;
 for x being Element of MetrStruct(# 2,Set_to_zero #) holds dist (x,x) = 0 by Th27;
hence  ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle ) by A1, Th1, Th3, Th4; ::_thesis: verum
end;
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 & p <> r & q <> r & 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 & p <> r & q <> r & 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
proof
let S be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for p, q, r being Element of S st q is_between p,r holds
q is_between r,p
let p, q, r be Element of S; ::_thesis: ( q is_between p,r implies q is_between r,p )
assume A1: q is_between p,r ; ::_thesis: q is_between r,p
hence  ( r <> q & r <> p & q <> p ) by Def22; :: according to METRIC_1:def_22 ::_thesis: dist (r,p) = (dist (r,q)) + (dist (q,p))
 dist (p,r) = (dist (p,q)) + (dist (q,r)) by A1, Def22;
hence  dist (r,p) = (dist (r,q)) + (dist (q,p)) ; ::_thesis: verum
end;

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 & not r is_between p,q )
proof
let S be MetrSpace; ::_thesis: for p, q, r being Element of S st q is_between p,r holds
( not p is_between q,r & not r is_between p,q )
let p, q, r be Element of S; ::_thesis: ( q is_between p,r implies ( not p is_between q,r & not r is_between p,q ) )
assume A1: q is_between p,r ; ::_thesis: ( not p is_between q,r & not r is_between p,q )
then A2: dist (p,r) = (dist (p,q)) + (dist (q,r)) by Def22;
A3: p <> q by A1, Def22;
thus  not p is_between q,r ::_thesis: not r is_between p,q
proof
assume  p is_between q,r ; ::_thesis: contradiction
then  dist (p,r) = (dist (p,q)) + ((dist (q,p)) + (dist (p,r))) by A2, Def22;
hence  contradiction by A3, Th7; ::_thesis: verum
end;
assume  r is_between p,q ; ::_thesis: contradiction
then A4: dist (p,q) = ((dist (p,q)) + (dist (q,r))) + (dist (r,q)) by A2, Def22;
 q <> r by A1, Def22;
hence  contradiction by A4, Th7; ::_thesis: verum
end;

theorem :: METRIC_1:32
for S being MetrSpace
for p, q, r, s being Element of S st q is_between p,r & r is_between p,s holds
( q is_between p,s & r is_between q,s )
proof
let S be MetrSpace; ::_thesis: for p, q, r, s being Element of S st q is_between p,r & r is_between p,s holds
( q is_between p,s & r is_between q,s )
let p, q, r, s be Element of S; ::_thesis: ( q is_between p,r & r is_between p,s implies ( q is_between p,s & r is_between q,s ) )
assume A1: q is_between p,r ; ::_thesis: ( not r is_between p,s or ( q is_between p,s & r is_between q,s ) )
then A2: p <> q by Def22;
assume A3: r is_between p,s ; ::_thesis: ( q is_between p,s & r is_between q,s )
then A4: ( p <> s & r <> s ) by Def22;
 dist (p,r) = (dist (p,q)) + (dist (q,r)) by A1, Def22;
then A5: dist (p,s) = ((dist (p,q)) + (dist (q,r))) + (dist (r,s)) by A3, Def22;
 ( dist (p,s) <= (dist (p,q)) + (dist (q,s)) & (dist (p,q)) + (dist (q,s)) <= ((dist (q,r)) + (dist (r,s))) + (dist (p,q)) ) by Th4, XREAL_1:6;
then A6: (dist (p,q)) + (dist (q,s)) = (dist (p,q)) + ((dist (q,r)) + (dist (r,s))) by A5, XXREAL_0:1;
A7: q <> r by A1, Def22;
then  q <> s by A5, Th7;
hence  ( q is_between p,s & r is_between q,s ) by A2, A7, A4, A5, A6, Def22; ::_thesis: verum
end;

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
proof
defpred S1[ Element of M] means $1 is_between p,r;
  {  q where q is Element of M : S1[q]  }  c= the carrier of M from FRAENKEL:sch_10();
hence   {  q where q is Element of M : q is_between p,r  }  is Subset of M ; ::_thesis: verum
end;
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 )
proof
let M be non empty MetrSpace; ::_thesis: for p, r, x being Element of M holds
( x in open_dist_Segment (p,r) iff x is_between p,r )
let p, r, x be Element of M; ::_thesis: ( x in open_dist_Segment (p,r) iff x is_between p,r )
 ( x in open_dist_Segment (p,r) implies x is_between p,r )
proof
assume  x in open_dist_Segment (p,r) ; ::_thesis: x is_between p,r
then  ex q being Element of M st
( x = q & q is_between p,r ) ;
hence  x is_between p,r ; ::_thesis: verum
end;
hence  ( x in open_dist_Segment (p,r) iff x is_between p,r ) ; ::_thesis: verum
end;

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
proof
defpred S1[ Element of M] means $1 is_between p,r;
A1: {p,r} c= the carrier of M by ZFMISC_1:32;
  {  q where q is Element of M : S1[q]  }  c= the carrier of M from FRAENKEL:sch_10();
hence   {  q where q is Element of M : q is_between p,r  }  \/ {p,r} is Subset of M by A1, XBOOLE_1:8; ::_thesis: verum
end;
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 ) )
proof
let M be non empty MetrStruct ; ::_thesis: 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 ) )
let p, r, x be Element of M; ::_thesis: ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )
A1: ( not x in close_dist_Segment (p,r) or x is_between p,r or x = p or x = r )
proof
assume  x in close_dist_Segment (p,r) ; ::_thesis: ( x is_between p,r or x = p or x = r )
then  ( x in  {  q where q is Element of M : q is_between p,r  }  or x in {p,r} ) by XBOOLE_0:def_3;
then  ( ex q being Element of M st
( x = q & q is_between p,r ) or x = p or x = r ) by TARSKI:def_2;
hence  ( x is_between p,r or x = p or x = r ) ; ::_thesis: verum
end;
now__::_thesis:_(_(_x_is_between_p,r_or_x_=_p_or_x_=_r_)_implies_x_in_close_dist_Segment_(p,r)_)
assume  ( x is_between p,r or x = p or x = r ) ; ::_thesis: x in close_dist_Segment (p,r)
then  ( x in  {  q where q is Element of M : q is_between p,r  }  or x in {p,r} ) by TARSKI:def_2;
hence  x in close_dist_Segment (p,r) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  ( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) ) by A1; ::_thesis: verum
end;