:: METRIC_2 semantic presentation

begin

definition
let M be non empty MetrStruct ;
let x, y be Element of M;
predx tolerates y means :Def1: :: METRIC_2:def 1
 dist (x,y) = 0 ;
end;

:: deftheorem Def1 defines tolerates METRIC_2:def_1_:_
 for M being non empty MetrStruct
for x, y being Element of M holds
( x tolerates y iff dist (x,y) = 0 );

definition
let M be non empty Reflexive MetrStruct ;
let x, y be Element of M;
:: original: tolerates
redefine predx tolerates y;
reflexivity
 for x being Element of M holds (M,b1,b1)
proof
let x be Element of M; ::_thesis: (M,x,x)
 dist (x,x) = 0 by METRIC_1:1;
hence  (M,x,x) by Def1; ::_thesis: verum
end;
end;

definition
let M be non empty symmetric MetrStruct ;
let x, y be Element of M;
:: original: tolerates
redefine predx tolerates y;
symmetry
 for x, y being Element of M st (M,b1,b2) holds
(M,b2,b1)
proof
let x, y be Element of M; ::_thesis: ( (M,x,y) implies (M,y,x) )
assume  x tolerates y ; ::_thesis: (M,y,x)
then  dist (x,y) = 0 by Def1;
hence  (M,y,x) by Def1; ::_thesis: verum
end;
end;

definition
let M be non empty MetrStruct ;
let x be Element of M;
funcx -neighbour  ->  Subset of M equals :: METRIC_2:def 2
 {  y where y is Element of M : x tolerates y  }  ;
coherence
  {  y where y is Element of M : x tolerates y  }  is Subset of M
proof
defpred S1[ Element of M] means x tolerates $1;
  {  y where y is Element of M : S1[y]  }  c= the carrier of M from FRAENKEL:sch_10();
hence   {  y where y is Element of M : x tolerates y  }  is Subset of M ; ::_thesis: verum
end;
end;

:: deftheorem  defines -neighbour METRIC_2:def_2_:_
 for M being non empty MetrStruct
for x being Element of M holds x -neighbour =  {  y where y is Element of M : x tolerates y  }  ;

definition
let M be non empty MetrStruct ;
mode equivalence_class of M ->  Subset of M means :Def3: :: METRIC_2:def 3
 ex x being Element of M st it = x -neighbour ;
existence
 ex b1 being Subset of M ex x being Element of M st b1 = x -neighbour
proof
set z = the Element of M;
 the Element of M -neighbour is Subset of M ;
hence  ex b1 being Subset of M ex x being Element of M st b1 = x -neighbour ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines equivalence_class METRIC_2:def_3_:_
 for M being non empty MetrStruct
for b2 being Subset of M holds
( b2 is equivalence_class of M iff ex x being Element of M st b2 = x -neighbour );

Lm1:  for M being non empty Reflexive MetrStruct
for x being Element of M holds x tolerates x
;

theorem Th1: :: METRIC_2:1
for M being PseudoMetricSpace
for x, y, z being Element of M st x tolerates y & y tolerates z holds
x tolerates z
proof
let M be PseudoMetricSpace; ::_thesis: for x, y, z being Element of M st x tolerates y & y tolerates z holds
x tolerates z
let x, y, z be Element of M; ::_thesis: ( x tolerates y & y tolerates z implies x tolerates z )
assume  ( x tolerates y & y tolerates z ) ; ::_thesis: x tolerates z
then  ( dist (x,y) = 0 & dist (y,z) = 0 ) by Def1;
then  dist (x,z) <= 0 + 0 by METRIC_1:4;
then  dist (x,z) = 0 by METRIC_1:5;
hence  x tolerates z by Def1; ::_thesis: verum
end;

theorem Th2: :: METRIC_2:2
for M being PseudoMetricSpace
for x, y being Element of M holds
( y in x -neighbour iff y tolerates x )
proof
let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M holds
( y in x -neighbour iff y tolerates x )
let x, y be Element of M; ::_thesis: ( y in x -neighbour iff y tolerates x )
hereby  ::_thesis: ( y tolerates x implies y in x -neighbour )
assume  y in x -neighbour ; ::_thesis: y tolerates x
then  ex q being Element of M st
( y = q & x tolerates q ) ;
hence  y tolerates x ; ::_thesis: verum
end;
assume  y tolerates x ; ::_thesis: y in x -neighbour
hence  y in x -neighbour ; ::_thesis: verum
end;

theorem :: METRIC_2:3
for M being PseudoMetricSpace
for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
p tolerates q
proof
let M be PseudoMetricSpace; ::_thesis: for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
p tolerates q
let x, p, q be Element of M; ::_thesis: ( p in x -neighbour & q in x -neighbour implies p tolerates q )
assume  ( p in x -neighbour & q in x -neighbour ) ; ::_thesis: p tolerates q
then  ( p tolerates x & q tolerates x ) by Th2;
hence  p tolerates q by Th1; ::_thesis: verum
end;

theorem Th4: :: METRIC_2:4
for M being PseudoMetricSpace
for x being Element of M holds x in x -neighbour
proof
let M be PseudoMetricSpace; ::_thesis: for x being Element of M holds x in x -neighbour
let x be Element of M; ::_thesis: x in x -neighbour
 x tolerates x by Lm1;
hence  x in x -neighbour ; ::_thesis: verum
end;

theorem :: METRIC_2:5
for M being PseudoMetricSpace
for x, y being Element of M st x in y -neighbour holds
y in x -neighbour
proof
let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M st x in y -neighbour holds
y in x -neighbour
let x, y be Element of M; ::_thesis: ( x in y -neighbour implies y in x -neighbour )
assume  x in y -neighbour ; ::_thesis: y in x -neighbour
then  x tolerates y by Th2;
hence  y in x -neighbour ; ::_thesis: verum
end;

theorem :: METRIC_2:6
for M being PseudoMetricSpace
for p, x, y being Element of M st p in x -neighbour & x tolerates y holds
p in y -neighbour
proof
let M be PseudoMetricSpace; ::_thesis: for p, x, y being Element of M st p in x -neighbour & x tolerates y holds
p in y -neighbour
let p, x, y be Element of M; ::_thesis: ( p in x -neighbour & x tolerates y implies p in y -neighbour )
assume that
A1: p in x -neighbour and
A2: x tolerates y ; ::_thesis: p in y -neighbour
 p tolerates x by A1, Th2;
then  p tolerates y by A2, Th1;
hence  p in y -neighbour ; ::_thesis: verum
end;

theorem Th7: :: METRIC_2:7
for M being PseudoMetricSpace
for x, y being Element of M st y in x -neighbour holds
x -neighbour = y -neighbour
proof
let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M st y in x -neighbour holds
x -neighbour = y -neighbour
let x, y be Element of M; ::_thesis: ( y in x -neighbour implies x -neighbour = y -neighbour )
assume A1: y in x -neighbour ; ::_thesis: x -neighbour = y -neighbour
 for p being Element of M st p in y -neighbour holds
p in x -neighbour
proof
let p be Element of M; ::_thesis: ( p in y -neighbour implies p in x -neighbour )
assume  p in y -neighbour ; ::_thesis: p in x -neighbour
then A2: p tolerates y by Th2;
 y tolerates x by A1, Th2;
then  p tolerates x by A2, Th1;
hence  p in x -neighbour ; ::_thesis: verum
end;
then A3: y -neighbour c= x -neighbour by SUBSET_1:2;
 for p being Element of M st p in x -neighbour holds
p in y -neighbour
proof
let p be Element of M; ::_thesis: ( p in x -neighbour implies p in y -neighbour )
assume  p in x -neighbour ; ::_thesis: p in y -neighbour
then A4: p tolerates x by Th2;
 x tolerates y by A1, Th2;
then  p tolerates y by A4, Th1;
hence  p in y -neighbour ; ::_thesis: verum
end;
then  x -neighbour c= y -neighbour by SUBSET_1:2;
hence  x -neighbour = y -neighbour by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th8: :: METRIC_2:8
for M being PseudoMetricSpace
for x, y being Element of M holds
( x -neighbour = y -neighbour iff x tolerates y )
proof
let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M holds
( x -neighbour = y -neighbour iff x tolerates y )
let x, y be Element of M; ::_thesis: ( x -neighbour = y -neighbour iff x tolerates y )
hereby  ::_thesis: ( x tolerates y implies x -neighbour = y -neighbour )
assume  x -neighbour = y -neighbour ; ::_thesis: x tolerates y
then  x in y -neighbour by Th4;
hence  x tolerates y by Th2; ::_thesis: verum
end;
assume  x tolerates y ; ::_thesis: x -neighbour = y -neighbour
then  x in y -neighbour ;
hence  x -neighbour = y -neighbour by Th7; ::_thesis: verum
end;

theorem :: METRIC_2:9
for M being PseudoMetricSpace
for x, y being Element of M holds
( x -neighbour meets y -neighbour iff x tolerates y )
proof
let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M holds
( x -neighbour meets y -neighbour iff x tolerates y )
let x, y be Element of M; ::_thesis: ( x -neighbour meets y -neighbour iff x tolerates y )
hereby  ::_thesis: ( x tolerates y implies x -neighbour meets y -neighbour )
assume  x -neighbour meets y -neighbour ; ::_thesis: x tolerates y
then consider p being set  such that
A1: p in x -neighbour and
A2: p in y -neighbour by XBOOLE_0:3;
A3: ex q being Element of M st
( q = p & x tolerates q ) by A1;
reconsider p = p as Element of M by A1;
 ex s being Element of M st
( s = p & y tolerates s ) by A2;
hence  x tolerates y by A3, Th1; ::_thesis: verum
end;
assume  x tolerates y ; ::_thesis: x -neighbour meets y -neighbour
then A4: x in y -neighbour ;
 x in x -neighbour by Th4;
hence  x -neighbour meets y -neighbour by A4, XBOOLE_0:3; ::_thesis: verum
end;

Lm2:  for M being PseudoMetricSpace
for V being equivalence_class of M holds V is non empty set
proof
let M be PseudoMetricSpace; ::_thesis: for V being equivalence_class of M holds V is non empty set
let V be equivalence_class of M; ::_thesis: V is non empty set
 ex x being Element of M st V = x -neighbour by Def3;
hence  V is non empty set by Th4; ::_thesis: verum
end;

registration
let M be PseudoMetricSpace;
cluster  ->  non empty for equivalence_class of M;
coherence
 for b1 being equivalence_class of M holds not b1 is empty by Lm2;
end;

theorem Th10: :: METRIC_2:10
for M being PseudoMetricSpace
for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
dist (p,q) = 0
proof
let M be PseudoMetricSpace; ::_thesis: for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
dist (p,q) = 0
let x, p, q be Element of M; ::_thesis: ( p in x -neighbour & q in x -neighbour implies dist (p,q) = 0 )
assume  ( p in x -neighbour & q in x -neighbour ) ; ::_thesis: dist (p,q) = 0
then  ( p tolerates x & q tolerates x ) by Th2;
then  p tolerates q by Th1;
hence  dist (p,q) = 0 by Def1; ::_thesis: verum
end;

theorem Th11: :: METRIC_2:11
for M being non empty Reflexive discerning MetrStruct
for x, y being Element of M holds
( x tolerates y iff x = y )
proof
let M be non empty Reflexive discerning MetrStruct ; ::_thesis: for x, y being Element of M holds
( x tolerates y iff x = y )
let x, y be Element of M; ::_thesis: ( x tolerates y iff x = y )
 ( x tolerates y implies x = y )
proof
assume  x tolerates y ; ::_thesis: x = y
then  dist (x,y) = 0 by Def1;
hence  x = y by METRIC_1:2; ::_thesis: verum
end;
hence  ( x tolerates y iff x = y ) ; ::_thesis: verum
end;

theorem Th12: :: METRIC_2:12
for M being non empty MetrSpace
for x, y being Element of M holds
( y in x -neighbour iff y = x )
proof
let M be non empty MetrSpace; ::_thesis: for x, y being Element of M holds
( y in x -neighbour iff y = x )
let x, y be Element of M; ::_thesis: ( y in x -neighbour iff y = x )
hereby  ::_thesis: ( y = x implies y in x -neighbour )
assume  y in x -neighbour ; ::_thesis: y = x
then  ex q being Element of M st
( y = q & x tolerates q ) ;
hence  y = x by Th11; ::_thesis: verum
end;
assume  y = x ; ::_thesis: y in x -neighbour
then  x tolerates y by Th11;
hence  y in x -neighbour ; ::_thesis: verum
end;

theorem Th13: :: METRIC_2:13
for M being non empty MetrSpace
for x being Element of M holds x -neighbour = {x}
proof
let M be non empty MetrSpace; ::_thesis: for x being Element of M holds x -neighbour = {x}
let x be Element of M; ::_thesis: x -neighbour = {x}
 for p being Element of M st p in {x} holds
p in x -neighbour
proof
let p be Element of M; ::_thesis: ( p in {x} implies p in x -neighbour )
assume  p in {x} ; ::_thesis: p in x -neighbour
then  p = x by TARSKI:def_1;
hence  p in x -neighbour by Th12; ::_thesis: verum
end;
then A1: {x} c= x -neighbour by SUBSET_1:2;
 for p being Element of M st p in x -neighbour holds
p in {x}
proof
let p be Element of M; ::_thesis: ( p in x -neighbour implies p in {x} )
assume  p in x -neighbour ; ::_thesis: p in {x}
then  p = x by Th12;
hence  p in {x} by TARSKI:def_1; ::_thesis: verum
end;
then  x -neighbour c= {x} by SUBSET_1:2;
hence  x -neighbour = {x} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: METRIC_2:14
for M being non empty MetrSpace
for V being Subset of M holds
( V is equivalence_class of M iff ex x being Element of M st V = {x} )
proof
let M be non empty MetrSpace; ::_thesis: for V being Subset of M holds
( V is equivalence_class of M iff ex x being Element of M st V = {x} )
let V be Subset of M; ::_thesis: ( V is equivalence_class of M iff ex x being Element of M st V = {x} )
A1: ( V is equivalence_class of M implies ex x being Element of M st V = {x} )
proof
assume  V is equivalence_class of M ; ::_thesis: ex x being Element of M st V = {x}
then consider x being Element of M such that
A2: V = x -neighbour by Def3;
 x -neighbour = {x} by Th13;
hence  ex x being Element of M st V = {x} by A2; ::_thesis: verum
end;
 ( ex x being Element of M st V = {x} implies V is equivalence_class of M )
proof
given x being Element of M such that A3: V = {x} ; ::_thesis: V is equivalence_class of M
 {x} = x -neighbour by Th13;
hence  V is equivalence_class of M by A3, Def3; ::_thesis: verum
end;
hence  ( V is equivalence_class of M iff ex x being Element of M st V = {x} ) by A1; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
funcM -neighbour  ->  set  equals :: METRIC_2:def 4
 {  s where s is Subset of M : ex x being Element of M st x -neighbour = s  }  ;
coherence
  {  s where s is Subset of M : ex x being Element of M st x -neighbour = s  }  is set ;
end;

:: deftheorem  defines -neighbour METRIC_2:def_4_:_
 for M being non empty MetrStruct holds M -neighbour =  {  s where s is Subset of M : ex x being Element of M st x -neighbour = s  }  ;

registration
let M be non empty MetrStruct ;
clusterM -neighbour  ->  non empty ;
coherence
 not M -neighbour is empty
proof
set y = the Element of M;
 the Element of M -neighbour in  {  s where s is Subset of M : ex x being Element of M st x -neighbour = s  }  ;
hence  not M -neighbour is empty ; ::_thesis: verum
end;
end;

theorem Th15: :: METRIC_2:15
for V being set
for M being non empty MetrStruct holds
( V in M -neighbour iff ex x being Element of M st V = x -neighbour )
proof
let V be set ; ::_thesis: for M being non empty MetrStruct holds
( V in M -neighbour iff ex x being Element of M st V = x -neighbour )
let M be non empty MetrStruct ; ::_thesis: ( V in M -neighbour iff ex x being Element of M st V = x -neighbour )
 ( V in M -neighbour implies ex x being Element of M st V = x -neighbour )
proof
assume  V in M -neighbour ; ::_thesis: ex x being Element of M st V = x -neighbour
then  ex q being Subset of M st
( q = V & ex x being Element of M st q = x -neighbour ) ;
hence  ex x being Element of M st V = x -neighbour ; ::_thesis: verum
end;
hence  ( V in M -neighbour iff ex x being Element of M st V = x -neighbour ) ; ::_thesis: verum
end;

theorem :: METRIC_2:16
for M being non empty MetrStruct
for x being Element of M holds x -neighbour in M -neighbour ;

theorem Th17: :: METRIC_2:17
for V being set
for M being non empty MetrStruct holds
( V in M -neighbour iff V is equivalence_class of M )
proof
let V be set ; ::_thesis: for M being non empty MetrStruct holds
( V in M -neighbour iff V is equivalence_class of M )
let M be non empty MetrStruct ; ::_thesis: ( V in M -neighbour iff V is equivalence_class of M )
A1: ( V is equivalence_class of M implies V in M -neighbour )
proof
assume  V is equivalence_class of M ; ::_thesis: V in M -neighbour
then  ex x being Element of M st V = x -neighbour by Def3;
hence  V in M -neighbour ; ::_thesis: verum
end;
 ( V in M -neighbour implies V is equivalence_class of M )
proof
assume  V in M -neighbour ; ::_thesis: V is equivalence_class of M
then  ex x being Element of M st V = x -neighbour by Th15;
hence  V is equivalence_class of M by Def3; ::_thesis: verum
end;
hence  ( V in M -neighbour iff V is equivalence_class of M ) by A1; ::_thesis: verum
end;

theorem :: METRIC_2:18
for M being non empty MetrSpace
for x being Element of M holds {x} in M -neighbour
proof
let M be non empty MetrSpace; ::_thesis: for x being Element of M holds {x} in M -neighbour
let x be Element of M; ::_thesis: {x} in M -neighbour
 x -neighbour = {x} by Th13;
hence  {x} in M -neighbour ; ::_thesis: verum
end;

theorem :: METRIC_2:19
for V being set
for M being non empty MetrSpace holds
( V in M -neighbour iff ex x being Element of M st V = {x} )
proof
let V be set ; ::_thesis: for M being non empty MetrSpace holds
( V in M -neighbour iff ex x being Element of M st V = {x} )
let M be non empty MetrSpace; ::_thesis: ( V in M -neighbour iff ex x being Element of M st V = {x} )
A1: ( V in M -neighbour implies ex x being Element of M st V = {x} )
proof
assume  V in M -neighbour ; ::_thesis: ex x being Element of M st V = {x}
then consider x being Element of M such that
A2: V = x -neighbour by Th15;
 x -neighbour = {x} by Th13;
hence  ex x being Element of M st V = {x} by A2; ::_thesis: verum
end;
 ( ex x being Element of M st V = {x} implies V in M -neighbour )
proof
given x being Element of M such that A3: V = {x} ; ::_thesis: V in M -neighbour
 x -neighbour = {x} by Th13;
hence  V in M -neighbour by A3; ::_thesis: verum
end;
hence  ( V in M -neighbour iff ex x being Element of M st V = {x} ) by A1; ::_thesis: verum
end;

theorem Th20: :: METRIC_2:20
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds
dist (p1,q1) = dist (p2,q2)
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour
for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds
dist (p1,q1) = dist (p2,q2)
let V, Q be Element of M -neighbour ; ::_thesis: for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds
dist (p1,q1) = dist (p2,q2)
let p1, p2, q1, q2 be Element of M; ::_thesis: ( p1 in V & q1 in Q & p2 in V & q2 in Q implies dist (p1,q1) = dist (p2,q2) )
assume that
A1: p1 in V and
A2: q1 in Q and
A3: p2 in V and
A4: q2 in Q ; ::_thesis: dist (p1,q1) = dist (p2,q2)
 V is equivalence_class of M by Th17;
then  ex x being Element of M st V = x -neighbour by Def3;
then A5: dist (p1,p2) = 0 by A1, A3, Th10;
 Q is equivalence_class of M by Th17;
then  ex y being Element of M st Q = y -neighbour by Def3;
then A6: dist (q1,q2) = 0 by A2, A4, Th10;
 ( dist (p2,q2) <= (dist (p2,p1)) + (dist (p1,q2)) & dist (p1,q2) <= (dist (p1,q1)) + (dist (q1,q2)) ) by METRIC_1:4;
then A7: dist (p2,q2) <= dist (p1,q1) by A5, A6, XXREAL_0:2;
 ( dist (p1,q1) <= (dist (p1,p2)) + (dist (p2,q1)) & dist (p2,q1) <= (dist (p2,q2)) + (dist (q2,q1)) ) by METRIC_1:4;
then  dist (p1,q1) <= dist (p2,q2) by A5, A6, XXREAL_0:2;
hence  dist (p1,q1) = dist (p2,q2) by A7, XXREAL_0:1; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
let V, Q be Element of M -neighbour ;
let v be Element of REAL ;
predV,Q is_dst v means :Def5: :: METRIC_2:def 5
 for p, q being Element of M st p in V & q in Q holds
dist (p,q) = v;
end;

:: deftheorem Def5 defines is_dst METRIC_2:def_5_:_
 for M being non empty MetrStruct
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff for p, q being Element of M st p in V & q in Q holds
dist (p,q) = v );

theorem Th21: :: METRIC_2:21
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
let V, Q be Element of M -neighbour ; ::_thesis: for v being Element of REAL holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
let v be Element of REAL ; ::_thesis: ( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
A1: ( V,Q is_dst v implies ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
proof
consider q being Element of M such that
A2: Q = q -neighbour by Th15;
A3: q in Q by A2, Th4;
assume A4: V,Q is_dst v ; ::_thesis: ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v )
consider p being Element of M such that
A5: V = p -neighbour by Th15;
 p in V by A5, Th4;
then  dist (p,q) = v by A4, A3, Def5;
hence  ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) by A5, A3, Th4; ::_thesis: verum
end;
 ( ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) implies V,Q is_dst v )
proof
assume  ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) ; ::_thesis: V,Q is_dst v
then  for p1, q1 being Element of M st p1 in V & q1 in Q holds
dist (p1,q1) = v by Th20;
hence  V,Q is_dst v by Def5; ::_thesis: verum
end;
hence  ( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) ) by A1; ::_thesis: verum
end;

theorem Th22: :: METRIC_2:22
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL st V,Q is_dst v holds
Q,V is_dst v
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour
for v being Element of REAL st V,Q is_dst v holds
Q,V is_dst v
let V, Q be Element of M -neighbour ; ::_thesis: for v being Element of REAL st V,Q is_dst v holds
Q,V is_dst v
let v be Element of REAL ; ::_thesis: ( V,Q is_dst v implies Q,V is_dst v )
assume  V,Q is_dst v ; ::_thesis: Q,V is_dst v
then  for q, p being Element of M st q in Q & p in V holds
dist (q,p) = v by Def5;
hence  Q,V is_dst v by Def5; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
let V, Q be Element of M -neighbour ;
func ev_eq_1 (V,Q) ->  Subset of REAL equals :: METRIC_2:def 6
 {  v where v is Element of REAL : V,Q is_dst v  }  ;
coherence
  {  v where v is Element of REAL : V,Q is_dst v  }  is Subset of REAL
proof
defpred S1[ Element of REAL ] means V,Q is_dst $1;
  {  v where v is Element of REAL : S1[v]  }  c= REAL from FRAENKEL:sch_10();
hence   {  v where v is Element of REAL : V,Q is_dst v  }  is Subset of REAL ; ::_thesis: verum
end;
end;

:: deftheorem  defines ev_eq_1 METRIC_2:def_6_:_
 for M being non empty MetrStruct
for V, Q being Element of M -neighbour holds ev_eq_1 (V,Q) =  {  v where v is Element of REAL : V,Q is_dst v  }  ;

theorem :: METRIC_2:23
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( v in ev_eq_1 (V,Q) iff V,Q is_dst v )
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour
for v being Element of REAL holds
( v in ev_eq_1 (V,Q) iff V,Q is_dst v )
let V, Q be Element of M -neighbour ; ::_thesis: for v being Element of REAL holds
( v in ev_eq_1 (V,Q) iff V,Q is_dst v )
let v be Element of REAL ; ::_thesis: ( v in ev_eq_1 (V,Q) iff V,Q is_dst v )
 ( v in ev_eq_1 (V,Q) implies V,Q is_dst v )
proof
assume  v in ev_eq_1 (V,Q) ; ::_thesis: V,Q is_dst v
then  ex r being Element of REAL st
( r = v & V,Q is_dst r ) ;
hence  V,Q is_dst v ; ::_thesis: verum
end;
hence  ( v in ev_eq_1 (V,Q) iff V,Q is_dst v ) ; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
let v be Element of REAL ;
func ev_eq_2 (v,M) ->  Subset of [:(M -neighbour),(M -neighbour):] equals :: METRIC_2:def 7
 {  W where W is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )  }  ;
coherence
  {  W where W is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )  }  is Subset of [:(M -neighbour),(M -neighbour):]
proof
defpred S1[ Element of [:(M -neighbour),(M -neighbour):]] means  ex V, Q being Element of M -neighbour st
( $1 = [V,Q] & V,Q is_dst v );
  {  W where W is Element of [:(M -neighbour),(M -neighbour):] : S1[W]  }  c= [:(M -neighbour),(M -neighbour):] from FRAENKEL:sch_10();
hence   {  W where W is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )  }  is Subset of [:(M -neighbour),(M -neighbour):] ; ::_thesis: verum
end;
end;

:: deftheorem  defines ev_eq_2 METRIC_2:def_7_:_
 for M being non empty MetrStruct
for v being Element of REAL holds ev_eq_2 (v,M) =  {  W where W is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )  }  ;

theorem :: METRIC_2:24
for M being PseudoMetricSpace
for v being Element of REAL
for W being Element of [:(M -neighbour),(M -neighbour):] holds
( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
proof
let M be PseudoMetricSpace; ::_thesis: for v being Element of REAL
for W being Element of [:(M -neighbour),(M -neighbour):] holds
( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
let v be Element of REAL ; ::_thesis: for W being Element of [:(M -neighbour),(M -neighbour):] holds
( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
let W be Element of [:(M -neighbour),(M -neighbour):]; ::_thesis: ( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
 ( W in ev_eq_2 (v,M) implies ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
proof
assume  W in ev_eq_2 (v,M) ; ::_thesis: ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )
then  ex S being Element of [:(M -neighbour),(M -neighbour):] st
( W = S & ex V, Q being Element of M -neighbour st
( S = [V,Q] & V,Q is_dst v ) ) ;
hence  ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) ; ::_thesis: verum
end;
hence  ( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) ) ; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
func real_in_rel M ->  Subset of REAL equals :: METRIC_2:def 8
 {  v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v  }  ;
coherence
  {  v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v  }  is Subset of REAL
proof
defpred S1[ Element of REAL ] means  ex V, Q being Element of M -neighbour st V,Q is_dst $1;
  {  v where v is Element of REAL : S1[v]  }  c= REAL from FRAENKEL:sch_10();
hence   {  v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v  }  is Subset of REAL ; ::_thesis: verum
end;
end;

:: deftheorem  defines real_in_rel METRIC_2:def_8_:_
 for M being non empty MetrStruct holds real_in_rel M =  {  v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v  }  ;

theorem :: METRIC_2:25
for M being PseudoMetricSpace
for v being Element of REAL holds
( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v )
proof
let M be PseudoMetricSpace; ::_thesis: for v being Element of REAL holds
( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v )
let v be Element of REAL ; ::_thesis: ( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v )
 ( v in real_in_rel M implies ex V, Q being Element of M -neighbour st V,Q is_dst v )
proof
assume  v in real_in_rel M ; ::_thesis: ex V, Q being Element of M -neighbour st V,Q is_dst v
then  ex r being Element of REAL st
( v = r & ex V, Q being Element of M -neighbour st V,Q is_dst r ) ;
hence  ex V, Q being Element of M -neighbour st V,Q is_dst v ; ::_thesis: verum
end;
hence  ( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v ) ; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
func elem_in_rel_1 M ->  Subset of (M -neighbour) equals :: METRIC_2:def 9
 {  V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;
coherence
  {  V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  is Subset of (M -neighbour)
proof
defpred S1[ Element of M -neighbour ] means  ex Q being Element of M -neighbour ex v being Element of REAL st $1,Q is_dst v;
  {  V where V is Element of M -neighbour : S1[V]  }  c= M -neighbour from FRAENKEL:sch_10();
hence   {  V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  is Subset of (M -neighbour) ; ::_thesis: verum
end;
end;

:: deftheorem  defines elem_in_rel_1 METRIC_2:def_9_:_
 for M being non empty MetrStruct holds elem_in_rel_1 M =  {  V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;

theorem Th26: :: METRIC_2:26
for M being PseudoMetricSpace
for V being Element of M -neighbour holds
( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proof
let M be PseudoMetricSpace; ::_thesis: for V being Element of M -neighbour holds
( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
let V be Element of M -neighbour ; ::_thesis: ( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
 ( V in elem_in_rel_1 M implies ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proof
assume  V in elem_in_rel_1 M ; ::_thesis: ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v
then  ex S being Element of M -neighbour st
( S = V & ex Q being Element of M -neighbour ex v being Element of REAL st S,Q is_dst v ) ;
hence  ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ; ::_thesis: verum
end;
hence  ( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) ; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
func elem_in_rel_2 M ->  Subset of (M -neighbour) equals :: METRIC_2:def 10
 {  Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;
coherence
  {  Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  is Subset of (M -neighbour)
proof
defpred S1[ Element of M -neighbour ] means  ex V being Element of M -neighbour ex v being Element of REAL st V,$1 is_dst v;
  {  Q where Q is Element of M -neighbour : S1[Q]  }  c= M -neighbour from FRAENKEL:sch_10();
hence   {  Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  is Subset of (M -neighbour) ; ::_thesis: verum
end;
end;

:: deftheorem  defines elem_in_rel_2 METRIC_2:def_10_:_
 for M being non empty MetrStruct holds elem_in_rel_2 M =  {  Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;

theorem Th27: :: METRIC_2:27
for M being PseudoMetricSpace
for Q being Element of M -neighbour holds
( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proof
let M be PseudoMetricSpace; ::_thesis: for Q being Element of M -neighbour holds
( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
let Q be Element of M -neighbour ; ::_thesis: ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
 ( Q in elem_in_rel_2 M implies ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proof
assume  Q in elem_in_rel_2 M ; ::_thesis: ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v
then  ex S being Element of M -neighbour st
( S = Q & ex V being Element of M -neighbour ex v being Element of REAL st V,S is_dst v ) ;
hence  ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ; ::_thesis: verum
end;
hence  ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) ; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
func elem_in_rel M ->  Subset of [:(M -neighbour),(M -neighbour):] equals :: METRIC_2:def 11
 {  VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )  }  ;
coherence
  {  VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )  }  is Subset of [:(M -neighbour),(M -neighbour):]
proof
defpred S1[ Element of [:(M -neighbour),(M -neighbour):]] means  ex V, Q being Element of M -neighbour ex v being Element of REAL st
( $1 = [V,Q] & V,Q is_dst v );
  {  VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : S1[VQ]  }  c= [:(M -neighbour),(M -neighbour):] from FRAENKEL:sch_10();
hence   {  VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )  }  is Subset of [:(M -neighbour),(M -neighbour):] ; ::_thesis: verum
end;
end;

:: deftheorem  defines elem_in_rel METRIC_2:def_11_:_
 for M being non empty MetrStruct holds elem_in_rel M =  {  VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )  }  ;

theorem :: METRIC_2:28
for M being PseudoMetricSpace
for VQ being Element of [:(M -neighbour),(M -neighbour):] holds
( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
proof
let M be PseudoMetricSpace; ::_thesis: for VQ being Element of [:(M -neighbour),(M -neighbour):] holds
( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
let VQ be Element of [:(M -neighbour),(M -neighbour):]; ::_thesis: ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
 ( VQ in elem_in_rel M implies ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
proof
assume  VQ in elem_in_rel M ; ::_thesis: ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )
then  ex S being Element of [:(M -neighbour),(M -neighbour):] st
( VQ = S & ex V, Q being Element of M -neighbour ex v being Element of REAL st
( S = [V,Q] & V,Q is_dst v ) ) ;
hence  ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) ; ::_thesis: verum
end;
hence  ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) ) ; ::_thesis: verum
end;

definition
let M be non empty MetrStruct ;
func set_in_rel M ->  Subset of [:(M -neighbour),(M -neighbour),REAL:] equals :: METRIC_2:def 12
 {  VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )  }  ;
coherence
  {  VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )  }  is Subset of [:(M -neighbour),(M -neighbour),REAL:]
proof
defpred S1[ Element of [:(M -neighbour),(M -neighbour),REAL:]] means  ex V, Q being Element of M -neighbour ex v being Element of REAL st
( $1 = [V,Q,v] & V,Q is_dst v );
  {  VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : S1[VQv]  }  c= [:(M -neighbour),(M -neighbour),REAL:] from FRAENKEL:sch_10();
hence   {  VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )  }  is Subset of [:(M -neighbour),(M -neighbour),REAL:] ; ::_thesis: verum
end;
end;

:: deftheorem  defines set_in_rel METRIC_2:def_12_:_
 for M being non empty MetrStruct holds set_in_rel M =  {  VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )  }  ;

theorem Th29: :: METRIC_2:29
for M being PseudoMetricSpace
for VQv being Element of [:(M -neighbour),(M -neighbour),REAL:] holds
( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) )
proof
let M be PseudoMetricSpace; ::_thesis: for VQv being Element of [:(M -neighbour),(M -neighbour),REAL:] holds
( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) )
let VQv be Element of [:(M -neighbour),(M -neighbour),REAL:]; ::_thesis: ( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) )
 ( VQv in set_in_rel M implies ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) )
proof
assume  VQv in set_in_rel M ; ::_thesis: ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )
then  ex S being Element of [:(M -neighbour),(M -neighbour),REAL:] st
( VQv = S & ex V, Q being Element of M -neighbour ex v being Element of REAL st
( S = [V,Q,v] & V,Q is_dst v ) ) ;
hence  ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) ; ::_thesis: verum
end;
hence  ( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) ) ; ::_thesis: verum
end;

theorem :: METRIC_2:30
for M being PseudoMetricSpace holds elem_in_rel_1 M = elem_in_rel_2 M
proof
let M be PseudoMetricSpace; ::_thesis: elem_in_rel_1 M = elem_in_rel_2 M
 for V being Element of M -neighbour st V in elem_in_rel_2 M holds
V in elem_in_rel_1 M
proof
let V be Element of M -neighbour ; ::_thesis: ( V in elem_in_rel_2 M implies V in elem_in_rel_1 M )
assume  V in elem_in_rel_2 M ; ::_thesis: V in elem_in_rel_1 M
then consider Q being Element of M -neighbour , v being Element of REAL  such that
A1: Q,V is_dst v by Th27;
 V,Q is_dst v by A1, Th22;
hence  V in elem_in_rel_1 M ; ::_thesis: verum
end;
then A2: elem_in_rel_2 M c= elem_in_rel_1 M by SUBSET_1:2;
 for V being Element of M -neighbour st V in elem_in_rel_1 M holds
V in elem_in_rel_2 M
proof
let V be Element of M -neighbour ; ::_thesis: ( V in elem_in_rel_1 M implies V in elem_in_rel_2 M )
assume  V in elem_in_rel_1 M ; ::_thesis: V in elem_in_rel_2 M
then consider Q being Element of M -neighbour , v being Element of REAL  such that
A3: V,Q is_dst v by Th26;
 Q,V is_dst v by A3, Th22;
hence  V in elem_in_rel_2 M ; ::_thesis: verum
end;
then  elem_in_rel_1 M c= elem_in_rel_2 M by SUBSET_1:2;
hence  elem_in_rel_1 M = elem_in_rel_2 M by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: METRIC_2:31
for M being PseudoMetricSpace holds set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
proof
let M be PseudoMetricSpace; ::_thesis: set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
 for VQv being Element of [:(M -neighbour),(M -neighbour),REAL:] st VQv in set_in_rel M holds
VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
proof
let VQv be Element of [:(M -neighbour),(M -neighbour),REAL:]; ::_thesis: ( VQv in set_in_rel M implies VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] )
assume  VQv in set_in_rel M ; ::_thesis: VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
then consider V, Q being Element of M -neighbour , v being Element of REAL  such that
A1: VQv = [V,Q,v] and
A2: V,Q is_dst v by Th29;
A3: v in real_in_rel M by A2;
 ( V in elem_in_rel_1 M & Q in elem_in_rel_2 M ) by A2;
hence  VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] by A1, A3, MCART_1:69; ::_thesis: verum
end;
hence  set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] by SUBSET_1:2; ::_thesis: verum
end;

theorem :: METRIC_2:32
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds
v1 = v2
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour
for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds
v1 = v2
let V, Q be Element of M -neighbour ; ::_thesis: for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds
v1 = v2
let v1, v2 be Element of REAL ; ::_thesis: ( V,Q is_dst v1 & V,Q is_dst v2 implies v1 = v2 )
assume that
A1: V,Q is_dst v1 and
A2: V,Q is_dst v2 ; ::_thesis: v1 = v2
consider p1 being Element of M such that
A3: V = p1 -neighbour by Th15;
consider q1 being Element of M such that
A4: Q = q1 -neighbour by Th15;
A5: q1 in Q by A4, Th4;
A6: p1 in V by A3, Th4;
then  dist (p1,q1) = v1 by A1, A5, Def5;
hence  v1 = v2 by A2, A6, A5, Def5; ::_thesis: verum
end;

theorem Th33: :: METRIC_2:33
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v
let V, Q be Element of M -neighbour ; ::_thesis: ex v being Element of REAL st V,Q is_dst v
consider p being Element of M such that
A1: V = p -neighbour by Th15;
consider q being Element of M such that
A2: Q = q -neighbour by Th15;
A3: q in Q by A2, Th4;
 p in V by A1, Th4;
then  V,Q is_dst dist (p,q) by A3, Th21;
hence  ex v being Element of REAL st V,Q is_dst v ; ::_thesis: verum
end;

definition
let M be PseudoMetricSpace;
func nbourdist M ->  Function of [:(M -neighbour),(M -neighbour):],REAL means :Def13: :: METRIC_2:def 13
 for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
it . (V,Q) = dist (p,q);
existence
 ex b1 being Function of [:(M -neighbour),(M -neighbour):],REAL st
for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b1 . (V,Q) = dist (p,q)
proof
defpred S1[ Element of M -neighbour , Element of M -neighbour , Element of REAL ] means $1,$2 is_dst $3;
A1: for V, Q being Element of M -neighbour ex v being Element of REAL st S1[V,Q,v] by Th33;
consider F being Function of [:(M -neighbour),(M -neighbour):],REAL such that
A2: for V, Q being Element of M -neighbour holds S1[V,Q,F . (V,Q)] from BINOP_1:sch_3(A1);
take  F ; ::_thesis: for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F . (V,Q) = dist (p,q)
let V, Q be Element of M -neighbour ; ::_thesis: for p, q being Element of M st p in V & q in Q holds
F . (V,Q) = dist (p,q)
let p, q be Element of M; ::_thesis: ( p in V & q in Q implies F . (V,Q) = dist (p,q) )
assume A3: ( p in V & q in Q ) ; ::_thesis: F . (V,Q) = dist (p,q)
 V,Q is_dst F . (V,Q) by A2;
hence  F . (V,Q) = dist (p,q) by A3, Def5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:(M -neighbour),(M -neighbour):],REAL st ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b1 . (V,Q) = dist (p,q) ) & ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b2 . (V,Q) = dist (p,q) ) holds
b1 = b2
proof
let F1, F2 be Function of [:(M -neighbour),(M -neighbour):],REAL; ::_thesis: ( ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F1 . (V,Q) = dist (p,q) ) & ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F2 . (V,Q) = dist (p,q) ) implies F1 = F2 )
assume that
A4: for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F1 . (V,Q) = dist (p,q) and
A5: for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F2 . (V,Q) = dist (p,q) ; ::_thesis: F1 = F2
 for V, Q being Element of M -neighbour holds F1 . (V,Q) = F2 . (V,Q)
proof
let V, Q be Element of M -neighbour ; ::_thesis: F1 . (V,Q) = F2 . (V,Q)
consider p being Element of M such that
A6: V = p -neighbour by Th15;
consider q being Element of M such that
A7: Q = q -neighbour by Th15;
A8: q in Q by A7, Th4;
A9: p in V by A6, Th4;
then F1 . (V,Q) = dist (p,q) by A4, A8
.= F2 . (V,Q) by A5, A9, A8 ;
hence  F1 . (V,Q) = F2 . (V,Q) ; ::_thesis: verum
end;
hence  F1 = F2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines nbourdist METRIC_2:def_13_:_
 for M being PseudoMetricSpace
for b2 being Function of [:(M -neighbour),(M -neighbour):],REAL holds
( b2 = nbourdist M iff for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b2 . (V,Q) = dist (p,q) );

theorem Th34: :: METRIC_2:34
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour holds
( (nbourdist M) . (V,Q) = 0 iff V = Q )
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour holds
( (nbourdist M) . (V,Q) = 0 iff V = Q )
let V, Q be Element of M -neighbour ; ::_thesis: ( (nbourdist M) . (V,Q) = 0 iff V = Q )
A1: ( V = Q implies (nbourdist M) . (V,Q) = 0 )
proof
consider p being Element of M such that
A2: V = p -neighbour by Th15;
A3: p in V by A2, Th4;
consider q being Element of M such that
A4: Q = q -neighbour by Th15;
assume  V = Q ; ::_thesis: (nbourdist M) . (V,Q) = 0
then A5: p tolerates q by A3, A4, Th2;
 q in Q by A4, Th4;
then (nbourdist M) . (V,Q) = dist (p,q) by A3, Def13
.= 0 by A5, Def1 ;
hence  (nbourdist M) . (V,Q) = 0 ; ::_thesis: verum
end;
 ( (nbourdist M) . (V,Q) = 0 implies V = Q )
proof
assume A6: (nbourdist M) . (V,Q) = 0 ; ::_thesis: V = Q
consider p being Element of M such that
A7: V = p -neighbour by Th15;
consider q being Element of M such that
A8: Q = q -neighbour by Th15;
A9: q in Q by A8, Th4;
 p in V by A7, Th4;
then  dist (p,q) = 0 by A6, A9, Def13;
then  p tolerates q by Def1;
hence  V = Q by A7, A8, Th8; ::_thesis: verum
end;
hence  ( (nbourdist M) . (V,Q) = 0 iff V = Q ) by A1; ::_thesis: verum
end;

theorem Th35: :: METRIC_2:35
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour holds (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V)
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour holds (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V)
let V, Q be Element of M -neighbour ; ::_thesis: (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V)
consider p being Element of M such that
A1: V = p -neighbour by Th15;
consider q being Element of M such that
A2: Q = q -neighbour by Th15;
A3: q in Q by A2, Th4;
A4: p in V by A1, Th4;
then (nbourdist M) . (V,Q) = dist (q,p) by A3, Def13
.= (nbourdist M) . (Q,V) by A4, A3, Def13 ;
hence  (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V) ; ::_thesis: verum
end;

theorem Th36: :: METRIC_2:36
for M being PseudoMetricSpace
for V, Q, W being Element of M -neighbour holds (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W))
proof
let M be PseudoMetricSpace; ::_thesis: for V, Q, W being Element of M -neighbour holds (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W))
let V, Q, W be Element of M -neighbour ; ::_thesis: (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W))
consider p being Element of M such that
A1: V = p -neighbour by Th15;
consider w being Element of M such that
A2: W = w -neighbour by Th15;
A3: w in W by A2, Th4;
consider q being Element of M such that
A4: Q = q -neighbour by Th15;
A5: q in Q by A4, Th4;
then A6: (nbourdist M) . (Q,W) = dist (q,w) by A3, Def13;
A7: p in V by A1, Th4;
then A8: (nbourdist M) . (V,W) = dist (p,w) by A3, Def13;
 (nbourdist M) . (V,Q) = dist (p,q) by A7, A5, Def13;
hence  (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W)) by A8, A6, METRIC_1:4; ::_thesis: verum
end;

definition
let M be PseudoMetricSpace;
func Eq_classMetricSpace M ->  MetrSpace equals :: METRIC_2:def 14
 MetrStruct(# (M -neighbour),(nbourdist M) #);
coherence
 MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace
proof
set Z = MetrStruct(# (M -neighbour),(nbourdist M) #);
now__::_thesis:_for_V,_Q,_W_being_Element_of_MetrStruct(#_(M_-neighbour),(nbourdist_M)_#)_holds_
(_(_dist_(V,Q)_=_0_implies_V_=_Q_)_&_(_V_=_Q_implies_dist_(V,Q)_=_0_)_&_dist_(V,Q)_=_dist_(Q,V)_&_dist_(V,W)_<=_(dist_(V,Q))_+_(dist_(Q,W))_)
let V, Q, W be Element of MetrStruct(# (M -neighbour),(nbourdist M) #); ::_thesis: ( ( dist (V,Q) = 0 implies V = Q ) & ( V = Q implies dist (V,Q) = 0 ) & dist (V,Q) = dist (Q,V) & dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) )
reconsider V9 = V, Q9 = Q, W9 = W as Element of M -neighbour ;
A1: dist (V,Q) = (nbourdist M) . (V9,Q9) by METRIC_1:def_1;
hence  ( dist (V,Q) = 0 iff V = Q ) by Th34; ::_thesis: ( dist (V,Q) = dist (Q,V) & dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) )
 dist (Q,V) = (nbourdist M) . (Q9,V9) by METRIC_1:def_1;
hence  dist (V,Q) = dist (Q,V) by A1, Th35; ::_thesis: dist (V,W) <= (dist (V,Q)) + (dist (Q,W))
 ( dist (V,W) = (nbourdist M) . (V9,W9) & dist (Q,W) = (nbourdist M) . (Q9,W9) ) by METRIC_1:def_1;
hence  dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) by A1, Th36; ::_thesis: verum
end;
hence  MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace by METRIC_1:6; ::_thesis: verum
end;
end;

:: deftheorem  defines Eq_classMetricSpace METRIC_2:def_14_:_
 for M being PseudoMetricSpace holds Eq_classMetricSpace M = MetrStruct(# (M -neighbour),(nbourdist M) #);

registration
let M be PseudoMetricSpace;
cluster Eq_classMetricSpace M ->  non empty strict ;
coherence
 ( Eq_classMetricSpace M is strict & not Eq_classMetricSpace M is empty ) ;
end;