:: JORDAN1K semantic presentation

begin


theorem Th1: :: JORDAN1K:1
for X being set
for Y being non empty set
for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being set st
( x in X & y = f . x )
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being set st
( x in X & y = f . x )
let Y be non empty set ; ::_thesis: for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being set st
( x in X & y = f . x )
let f be Function of X,Y; ::_thesis: ( f is onto implies for y being Element of Y ex x being set st
( x in X & y = f . x ) )
assume  f is onto ; ::_thesis: for y being Element of Y ex x being set st
( x in X & y = f . x )
then A1: rng f = Y by FUNCT_2:def_3;
let y be Element of Y; ::_thesis: ex x being set st
( x in X & y = f . x )
thus  ex x being set st
( x in X & y = f . x ) by A1, FUNCT_2:11; ::_thesis: verum
end;

theorem :: JORDAN1K:2
for X being set
for Y being non empty set
for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being Element of X st y = f . x
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being Element of X st y = f . x
let Y be non empty set ; ::_thesis: for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being Element of X st y = f . x
let f be Function of X,Y; ::_thesis: ( f is onto implies for y being Element of Y ex x being Element of X st y = f . x )
assume A1: f is onto ; ::_thesis: for y being Element of Y ex x being Element of X st y = f . x
let y be Element of Y; ::_thesis: ex x being Element of X st y = f . x
 ex x being set st
( x in X & f . x = y ) by A1, Th1;
hence  ex x being Element of X st y = f . x ; ::_thesis: verum
end;

theorem Th3: :: JORDAN1K:3
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A `)
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A `)
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A `)
let f be Function of X,Y; ::_thesis: for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A `)
let A be Subset of X; ::_thesis: ( f is onto implies (f .: A) ` c= f .: (A `) )
assume A1: f is onto ; ::_thesis: (f .: A) ` c= f .: (A `)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (f .: A) ` or e in f .: (A `) )
assume A2: e in (f .: A) ` ; ::_thesis: e in f .: (A `)
then reconsider y = e as Element of Y ;
consider u being set  such that
A3: u in X and
A4: y = f . u by A1, Th1;
reconsider x = u as Element of X by A3;
now__::_thesis:_not_x_in_A
assume  x in A ; ::_thesis: contradiction
then  y in f .: A by A4, FUNCT_2:35;
hence  contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
then  x in A ` by A3, SUBSET_1:29;
hence  e in f .: (A `) by A4, FUNCT_2:35; ::_thesis: verum
end;

theorem Th4: :: JORDAN1K:4
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let f be Function of X,Y; ::_thesis: for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let A be Subset of X; ::_thesis: ( f is one-to-one implies f .: (A `) c= (f .: A) ` )
assume A1: f is one-to-one ; ::_thesis: f .: (A `) c= (f .: A) `
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f .: (A `) or e in (f .: A) ` )
assume A2: e in f .: (A `) ; ::_thesis: e in (f .: A) `
then reconsider y = e as Element of Y ;
consider x1 being set  such that
A3: x1 in X and
A4: x1 in A ` and
A5: y = f . x1 by A2, FUNCT_2:64;
assume  not e in (f .: A) ` ; ::_thesis: contradiction
then A6: ex x2 being set st
( x2 in X & x2 in A & y = f . x2 ) by FUNCT_2:64, SUBSET_1:29;
 not x1 in A by A4, XBOOLE_0:def_5;
hence  contradiction by A1, A3, A5, A6, FUNCT_2:19; ::_thesis: verum
end;

theorem Th5: :: JORDAN1K:5
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A `)
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A `)
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A `)
let f be Function of X,Y; ::_thesis: for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A `)
let A be Subset of X; ::_thesis: ( f is bijective implies (f .: A) ` = f .: (A `) )
assume  f is bijective ; ::_thesis: (f .: A) ` = f .: (A `)
then  ( (f .: A) ` c= f .: (A `) & f .: (A `) c= (f .: A) ` ) by Th3, Th4;
hence  (f .: A) ` = f .: (A `) by XBOOLE_0:def_10; ::_thesis: verum
end;

begin

theorem Th6: :: JORDAN1K:6
for T being TopSpace
for A being Subset of T holds
( A is_a_component_of {} T iff A is empty )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is_a_component_of {} T iff A is empty )
let A be Subset of T; ::_thesis: ( A is_a_component_of {} T iff A is empty )
thus  ( A is_a_component_of {} T implies A is empty ) by SPRECT_1:5, XBOOLE_1:3; ::_thesis: ( A is empty implies A is_a_component_of {} T )
assume A1: A is empty ; ::_thesis: A is_a_component_of {} T
then reconsider B = A as Subset of (T | ({} T)) by XBOOLE_1:2;
 for C being Subset of (T | ({} T)) st C is connected & B c= C holds
B = C by A1, XBOOLE_1:3;
then  B is a_component by A1, CONNSP_1:def_5;
hence  A is_a_component_of {} T by CONNSP_1:def_6; ::_thesis: verum
end;

theorem Th7: :: JORDAN1K:7
for T being non empty TopSpace
for A, B, C being Subset of T st A c= B & A is_a_component_of C & B is_a_component_of C holds
A = B
proof
let T be non empty TopSpace; ::_thesis: for A, B, C being Subset of T st A c= B & A is_a_component_of C & B is_a_component_of C holds
A = B
let A, B, C be Subset of T; ::_thesis: ( A c= B & A is_a_component_of C & B is_a_component_of C implies A = B )
assume that
A1: A c= B and
A2: A is_a_component_of C and
A3: B is_a_component_of C ; ::_thesis: A = B
percases ( C = {} or not C is empty ) ;
suppose C = {} ; ::_thesis: A = B
then A4: C = {} T ;
then  A = {} by A2, Th6;
hence  A = B by A3, A4, Th6; ::_thesis: verum
end;
suppose not C is empty ; ::_thesis: A = B
then  A <> {} by A2, SPRECT_1:4;
hence  A = B by A1, A2, A3, GOBOARD9:1, XBOOLE_1:69; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN1K:8
for n being Element of NAT st n >= 1 holds
for P being Subset of (Euclid n) st P is bounded holds
not P ` is bounded
proof
let n be Element of NAT ; ::_thesis: ( n >= 1 implies for P being Subset of (Euclid n) st P is bounded holds
not P ` is bounded )
assume A1: n >= 1 ; ::_thesis: for P being Subset of (Euclid n) st P is bounded holds
not P ` is bounded
 REAL n c= the carrier of (Euclid n) ;
then reconsider W = REAL n as Subset of (Euclid n) ;
let P be Subset of (Euclid n); ::_thesis: ( P is bounded implies not P ` is bounded )
A2: P \/ (P `) = [#] (Euclid n) by PRE_TOPC:2
.= W ;
assume  ( P is bounded & P ` is bounded ) ; ::_thesis: contradiction
hence  contradiction by A1, A2, JORDAN2C:33, TBSP_1:13; ::_thesis: verum
end;


theorem Th9: :: JORDAN1K:9
for M being non empty MetrSpace
for C being non empty Subset of (TopSpaceMetr M)
for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0
proof
let M be non empty MetrSpace; ::_thesis: for C being non empty Subset of (TopSpaceMetr M)
for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0
let C be non empty Subset of (TopSpaceMetr M); ::_thesis: for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0
let p be Point of (TopSpaceMetr M); ::_thesis: (dist_min C) . p >= 0
A1: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider x = p as Point of M ;
set B = [#] ((dist x) .: C);
A2: [#] ((dist x) .: C) = (dist x) .: C by WEIERSTR:def_1;
A3: for r being real number st r in [#] ((dist x) .: C) holds
0 <= r
proof
let r be real number ; ::_thesis: ( r in [#] ((dist x) .: C) implies 0 <= r )
assume  r in [#] ((dist x) .: C) ; ::_thesis: 0 <= r
then consider y being set  such that
 y in dom (dist x) and
A4: y in C and
A5: r = (dist x) . y by A2, FUNCT_1:def_6;
reconsider y9 = y as Point of M by A1, A4;
 r = dist (x,y9) by A5, WEIERSTR:def_4;
hence  0 <= r by METRIC_1:5; ::_thesis: verum
end;
 dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  lower_bound ([#] ((dist x) .: C)) >= 0 by A2, A3, SEQ_4:43;
then  lower_bound ((dist x) .: C) >= 0 by WEIERSTR:def_3;
hence  (dist_min C) . p >= 0 by WEIERSTR:def_6; ::_thesis: verum
end;

theorem Th10: :: JORDAN1K:10
for r being Real
for M being non empty MetrSpace
for C being non empty Subset of (TopSpaceMetr M)
for p being Point of M st ( for q being Point of M st q in C holds
dist (p,q) >= r ) holds
(dist_min C) . p >= r
proof
let r be Real; ::_thesis: for M being non empty MetrSpace
for C being non empty Subset of (TopSpaceMetr M)
for p being Point of M st ( for q being Point of M st q in C holds
dist (p,q) >= r ) holds
(dist_min C) . p >= r
let M be non empty MetrSpace; ::_thesis: for C being non empty Subset of (TopSpaceMetr M)
for p being Point of M st ( for q being Point of M st q in C holds
dist (p,q) >= r ) holds
(dist_min C) . p >= r
let C be non empty Subset of (TopSpaceMetr M); ::_thesis: for p being Point of M st ( for q being Point of M st q in C holds
dist (p,q) >= r ) holds
(dist_min C) . p >= r
let p be Point of M; ::_thesis: ( ( for q being Point of M st q in C holds
dist (p,q) >= r ) implies (dist_min C) . p >= r )
assume A1: for q being Point of M st q in C holds
dist (p,q) >= r ; ::_thesis: (dist_min C) . p >= r
set B = [#] ((dist p) .: C);
A2: [#] ((dist p) .: C) = (dist p) .: C by WEIERSTR:def_1;
A3: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
A4: for s being real number st s in [#] ((dist p) .: C) holds
r <= s
proof
let s be real number ; ::_thesis: ( s in [#] ((dist p) .: C) implies r <= s )
assume  s in [#] ((dist p) .: C) ; ::_thesis: r <= s
then consider y being set  such that
 y in dom (dist p) and
A5: y in C and
A6: s = (dist p) . y by A2, FUNCT_1:def_6;
reconsider y9 = y as Point of M by A3, A5;
 s = dist (p,y9) by A6, WEIERSTR:def_4;
hence  r <= s by A1, A5; ::_thesis: verum
end;
 dom (dist p) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  lower_bound ([#] ((dist p) .: C)) >= r by A2, A4, SEQ_4:43;
then  lower_bound ((dist p) .: C) >= r by WEIERSTR:def_3;
hence  (dist_min C) . p >= r by WEIERSTR:def_6; ::_thesis: verum
end;

theorem Th11: :: JORDAN1K:11
for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) holds min_dist_min (A,B) >= 0
proof
let M be non empty MetrSpace; ::_thesis: for A, B being non empty Subset of (TopSpaceMetr M) holds min_dist_min (A,B) >= 0
let A, B be non empty Subset of (TopSpaceMetr M); ::_thesis: min_dist_min (A,B) >= 0
set X = [#] ((dist_min A) .: B);
A1: [#] ((dist_min A) .: B) = (dist_min A) .: B by WEIERSTR:def_1;
A2: for r being real number st r in [#] ((dist_min A) .: B) holds
0 <= r
proof
let r be real number ; ::_thesis: ( r in [#] ((dist_min A) .: B) implies 0 <= r )
assume  r in [#] ((dist_min A) .: B) ; ::_thesis: 0 <= r
then consider y being set  such that
 y in dom (dist_min A) and
A3: y in B and
A4: r = (dist_min A) . y by A1, FUNCT_1:def_6;
reconsider y = y as Point of (TopSpaceMetr M) by A3;
 (dist_min A) . y >= 0 by Th9;
hence  0 <= r by A4; ::_thesis: verum
end;
 dom (dist_min A) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  lower_bound ([#] ((dist_min A) .: B)) >= 0 by A1, A2, SEQ_4:43;
then  lower_bound ((dist_min A) .: B) >= 0 by WEIERSTR:def_3;
hence  min_dist_min (A,B) >= 0 by WEIERSTR:def_7; ::_thesis: verum
end;

theorem Th12: :: JORDAN1K:12
for M being non empty MetrSpace
for A, B being compact Subset of (TopSpaceMetr M) st A meets B holds
min_dist_min (A,B) = 0
proof
let M be non empty MetrSpace; ::_thesis: for A, B being compact Subset of (TopSpaceMetr M) st A meets B holds
min_dist_min (A,B) = 0
let A, B be compact Subset of (TopSpaceMetr M); ::_thesis: ( A meets B implies min_dist_min (A,B) = 0 )
assume  A meets B ; ::_thesis: min_dist_min (A,B) = 0
then consider p being set  such that
A1: p in A and
A2: p in B by XBOOLE_0:3;
 TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider p = p as Point of M by A1;
 ( min_dist_min (A,B) >= 0 & min_dist_min (A,B) <= dist (p,p) ) by A1, A2, Th11, WEIERSTR:34;
hence  min_dist_min (A,B) = 0 by METRIC_1:1; ::_thesis: verum
end;

theorem Th13: :: JORDAN1K:13
for r being Real
for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) holds
min_dist_min (A,B) >= r
proof
let r be Real; ::_thesis: for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) holds
min_dist_min (A,B) >= r
let M be non empty MetrSpace; ::_thesis: for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) holds
min_dist_min (A,B) >= r
let A, B be non empty Subset of (TopSpaceMetr M); ::_thesis: ( ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) implies min_dist_min (A,B) >= r )
assume A1: for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ; ::_thesis: min_dist_min (A,B) >= r
set X = [#] ((dist_min A) .: B);
A2: [#] ((dist_min A) .: B) = (dist_min A) .: B by WEIERSTR:def_1;
A3: for s being real number st s in [#] ((dist_min A) .: B) holds
r <= s
proof
let s be real number ; ::_thesis: ( s in [#] ((dist_min A) .: B) implies r <= s )
assume  s in [#] ((dist_min A) .: B) ; ::_thesis: r <= s
then consider y being set  such that
 y in dom (dist_min A) and
A4: y in B and
A5: s = (dist_min A) . y by A2, FUNCT_1:def_6;
reconsider y = y as Point of (TopSpaceMetr M) by A4;
reconsider p = y as Point of M by TOPMETR:12;
 for q being Point of M st q in A holds
dist (p,q) >= r by A1, A4;
hence  r <= s by A5, Th10; ::_thesis: verum
end;
 dom (dist_min A) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  lower_bound ([#] ((dist_min A) .: B)) >= r by A2, A3, SEQ_4:43;
then  lower_bound ((dist_min A) .: B) >= r by WEIERSTR:def_3;
hence  min_dist_min (A,B) >= r by WEIERSTR:def_7; ::_thesis: verum
end;

begin

theorem Th14: :: JORDAN1K:14
for n being Element of NAT
for P, Q being Subset of (TOP-REAL n) holds
( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q )
proof
let n be Element of NAT ; ::_thesis: for P, Q being Subset of (TOP-REAL n) holds
( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q )
let P, Q be Subset of (TOP-REAL n); ::_thesis: ( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q )
thus  ( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q ) by JORDAN2C:def_2, JORDAN2C:def_3; ::_thesis: verum
end;

theorem :: JORDAN1K:15
for n being Element of NAT st n >= 1 holds
BDD ({} (TOP-REAL n)) = {} (TOP-REAL n)
proof
let n be Element of NAT ; ::_thesis: ( n >= 1 implies BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) )
set X =  {  B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n)  }  ;
assume  n >= 1 ; ::_thesis: BDD ({} (TOP-REAL n)) = {} (TOP-REAL n)
then A1: not [#] (TOP-REAL n) is bounded by JORDAN2C:35;
now__::_thesis:_not__{__B_where_B_is_Subset_of_(TOP-REAL_n)_:_B_is_inside_component_of_{}_(TOP-REAL_n)__}__<>_{}
 [#] (TOP-REAL n) is a_component ;
then A2: [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is a_component by CONNSP_1:45;
 (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
then A3: [#] (TOP-REAL n) is_a_component_of [#] (TOP-REAL n) by A2, CONNSP_1:def_6;
assume   {  B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n)  }  <> {} ; ::_thesis: contradiction
then consider x being set  such that
A4: x in  {  B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n)  }  by XBOOLE_0:def_1;
consider B being Subset of (TOP-REAL n) such that
 x = B and
A5: B is_inside_component_of {} (TOP-REAL n) by A4;
 B is_a_component_of ({} (TOP-REAL n)) ` by A5, JORDAN2C:def_2;
then  B = [#] (TOP-REAL n) by A3, Th7;
hence  contradiction by A1, A5, JORDAN2C:def_2; ::_thesis: verum
end;
hence  BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) by JORDAN2C:def_4, ZFMISC_1:2; ::_thesis: verum
end;

theorem :: JORDAN1K:16
for n being Element of NAT holds BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n)
proof
let n be Element of NAT ; ::_thesis: BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n)
 BDD ([#] (TOP-REAL n)) c= ([#] (TOP-REAL n)) ` by JORDAN2C:25;
then  BDD ([#] (TOP-REAL n)) c= {} (TOP-REAL n) by XBOOLE_1:37;
hence  BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n) by XBOOLE_1:3; ::_thesis: verum
end;

theorem :: JORDAN1K:17
for n being Element of NAT st n >= 1 holds
UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n)
proof
let n be Element of NAT ; ::_thesis: ( n >= 1 implies UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n) )
set X =  {  B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n)  }  ;
assume  n >= 1 ; ::_thesis: UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n)
then A1: not [#] (TOP-REAL n) is bounded by JORDAN2C:35;
thus  UBD ({} (TOP-REAL n)) c= [#] (TOP-REAL n) ; :: according to XBOOLE_0:def_10 ::_thesis: [#] (TOP-REAL n) c= UBD ({} (TOP-REAL n))
 [#] (TOP-REAL n) is a_component ;
then A2: [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is a_component by CONNSP_1:45;
 (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
then A3: [#] (TOP-REAL n) is_a_component_of [#] (TOP-REAL n) by A2, CONNSP_1:def_6;
 [#] (TOP-REAL n) = ({} (TOP-REAL n)) ` ;
then  [#] (TOP-REAL n) is_outside_component_of {} (TOP-REAL n) by A1, A3, JORDAN2C:def_3;
then  [#] (TOP-REAL n) in  {  B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n)  }  ;
then  [#] (TOP-REAL n) c= union  {  B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n)  }  by ZFMISC_1:74;
hence  [#] (TOP-REAL n) c= UBD ({} (TOP-REAL n)) by JORDAN2C:def_5; ::_thesis: verum
end;

theorem :: JORDAN1K:18
for n being Element of NAT holds UBD ([#] (TOP-REAL n)) = {} (TOP-REAL n)
proof
let n be Element of NAT ; ::_thesis: UBD ([#] (TOP-REAL n)) = {} (TOP-REAL n)
 UBD ([#] (TOP-REAL n)) c= ([#] (TOP-REAL n)) ` by JORDAN2C:26;
then  UBD ([#] (TOP-REAL n)) c= {} (TOP-REAL n) by XBOOLE_1:37;
hence  UBD ([#] (TOP-REAL n)) = {} (TOP-REAL n) by XBOOLE_1:3; ::_thesis: verum
end;

theorem :: JORDAN1K:19
for n being Element of NAT
for P being connected Subset of (TOP-REAL n)
for Q being Subset of (TOP-REAL n) holds
( not P misses Q or P c= UBD Q or P c= BDD Q )
proof
let n be Element of NAT ; ::_thesis: for P being connected Subset of (TOP-REAL n)
for Q being Subset of (TOP-REAL n) holds
( not P misses Q or P c= UBD Q or P c= BDD Q )
let P be connected Subset of (TOP-REAL n); ::_thesis: for Q being Subset of (TOP-REAL n) holds
( not P misses Q or P c= UBD Q or P c= BDD Q )
let Q be Subset of (TOP-REAL n); ::_thesis: ( not P misses Q or P c= UBD Q or P c= BDD Q )
assume A1: P misses Q ; ::_thesis: ( P c= UBD Q or P c= BDD Q )
percases ( P is empty or Q = [#] (TOP-REAL n) or ( not P is empty & Q <> [#] (TOP-REAL n) ) ) ;
suppose P is empty ; ::_thesis: ( P c= UBD Q or P c= BDD Q )
hence  ( P c= UBD Q or P c= BDD Q ) by XBOOLE_1:2; ::_thesis: verum
end;
suppose Q = [#] (TOP-REAL n) ; ::_thesis: ( P c= UBD Q or P c= BDD Q )
then  P = {} by A1, XBOOLE_1:67;
hence  ( P c= UBD Q or P c= BDD Q ) by XBOOLE_1:2; ::_thesis: verum
end;
supposethat A2: not P is empty and
A3: Q <> [#] (TOP-REAL n) ; ::_thesis: ( P c= UBD Q or P c= BDD Q )
 (Q `) ` <> [#] (TOP-REAL n) by A3;
then A4: Q ` <> {} (TOP-REAL n) ;
 P c= Q ` by A1, SUBSET_1:23;
then consider C being Subset of (TOP-REAL n) such that
A5: C is_a_component_of Q ` and
A6: P c= C by A2, A4, GOBOARD9:3;
 ( C is_inside_component_of Q or C is_outside_component_of Q ) by A5, Th14;
then  ( C c= UBD Q or C c= BDD Q ) by JORDAN2C:22, JORDAN2C:23;
hence  ( P c= UBD Q or P c= BDD Q ) by A6, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;

begin


theorem Th20: :: JORDAN1K:20
for q being Point of (TOP-REAL 2)
for r being Real holds dist (|[0,0]|,(r * q)) = (abs r) * (dist (|[0,0]|,q))
proof
let q be Point of (TOP-REAL 2); ::_thesis: for r being Real holds dist (|[0,0]|,(r * q)) = (abs r) * (dist (|[0,0]|,q))
let r be Real; ::_thesis: dist (|[0,0]|,(r * q)) = (abs r) * (dist (|[0,0]|,q))
A1: ( r ^2 >= 0 & (q `1) ^2 >= 0 ) by XREAL_1:63;
A2: (q `2) ^2 >= 0 by XREAL_1:63;
A3: ( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 ) by EUCLID:52;
then A4: dist (|[0,0]|,q) = sqrt (((0 - (q `1)) ^2) + ((0 - (q `2)) ^2)) by TOPREAL6:92
.= sqrt (((q `1) ^2) + ((q `2) ^2)) ;
thus  dist (|[0,0]|,(r * q)) = sqrt (((0 - ((r * q) `1)) ^2) + ((0 - ((r * q) `2)) ^2)) by A3, TOPREAL6:92
.= sqrt ((((r * q) `1) ^2) + ((- ((r * q) `2)) ^2))
.= sqrt (((r * (q `1)) ^2) + (((r * q) `2) ^2)) by TOPREAL3:4
.= sqrt (((r ^2) * ((q `1) ^2)) + ((r * (q `2)) ^2)) by TOPREAL3:4
.= sqrt ((r ^2) * (((q `1) ^2) + ((q `2) ^2)))
.= (sqrt (r ^2)) * (sqrt (((q `1) ^2) + ((q `2) ^2))) by A1, A2, SQUARE_1:29
.= (abs r) * (dist (|[0,0]|,q)) by A4, COMPLEX1:72 ; ::_thesis: verum
end;

theorem Th21: :: JORDAN1K:21
for q1, q, q2 being Point of (TOP-REAL 2) holds dist ((q1 + q),(q2 + q)) = dist (q1,q2)
proof
let q1, q, q2 be Point of (TOP-REAL 2); ::_thesis: dist ((q1 + q),(q2 + q)) = dist (q1,q2)
A1: ((q1 + q) `1) - ((q2 + q) `1) = ((q1 `1) + (q `1)) - ((q2 + q) `1) by TOPREAL3:2
.= ((q1 `1) + (q `1)) - ((q2 `1) + (q `1)) by TOPREAL3:2
.= ((q1 `1) - (q2 `1)) + 0 ;
A2: ((q1 + q) `2) - ((q2 + q) `2) = ((q1 `2) + (q `2)) - ((q2 + q) `2) by TOPREAL3:2
.= ((q1 `2) + (q `2)) - ((q2 `2) + (q `2)) by TOPREAL3:2
.= ((q1 `2) - (q2 `2)) + 0 ;
thus  dist ((q1 + q),(q2 + q)) = sqrt (((((q1 + q) `1) - ((q2 + q) `1)) ^2) + ((((q1 + q) `2) - ((q2 + q) `2)) ^2)) by TOPREAL6:92
.= dist (q1,q2) by A1, A2, TOPREAL6:92 ; ::_thesis: verum
end;

theorem Th22: :: JORDAN1K:22
for p, q being Point of (TOP-REAL 2) st p <> q holds
dist (p,q) > 0
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q implies dist (p,q) > 0 )
 ex p9, q9 being Point of (Euclid 2) st
( p9 = p & q9 = q & dist (p,q) = dist (p9,q9) ) by TOPREAL6:def_1;
hence  ( p <> q implies dist (p,q) > 0 ) by METRIC_1:7; ::_thesis: verum
end;

theorem Th23: :: JORDAN1K:23
for q1, q, q2 being Point of (TOP-REAL 2) holds dist ((q1 - q),(q2 - q)) = dist (q1,q2)
proof
let q1, q, q2 be Point of (TOP-REAL 2); ::_thesis: dist ((q1 - q),(q2 - q)) = dist (q1,q2)
 ( q1 - q = q1 + (- q) & q2 - q = q2 + (- q) ) by EUCLID:41;
hence  dist ((q1 - q),(q2 - q)) = dist (q1,q2) by Th21; ::_thesis: verum
end;

theorem Th24: :: JORDAN1K:24
for p, q being Point of (TOP-REAL 2) holds dist (p,q) = dist ((- p),(- q))
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: dist (p,q) = dist ((- p),(- q))
thus  dist (p,q) = dist ((q - q),(p - q)) by Th23
.= dist ((q - q),(p + (- q))) by EUCLID:41
.= dist (|[0,0]|,(p + (- q))) by EUCLID:42, EUCLID:54
.= dist ((p - p),(p + (- q))) by EUCLID:42, EUCLID:54
.= dist ((p + (- p)),(p + (- q))) by EUCLID:41
.= dist ((- p),(- q)) by Th21 ; ::_thesis: verum
end;

theorem Th25: :: JORDAN1K:25
for q, q1, q2 being Point of (TOP-REAL 2) holds dist ((q - q1),(q - q2)) = dist (q1,q2)
proof
let q, q1, q2 be Point of (TOP-REAL 2); ::_thesis: dist ((q - q1),(q - q2)) = dist (q1,q2)
 ( - (q - q1) = q1 - q & - (q - q2) = q2 - q ) by EUCLID:44;
hence  dist ((q - q1),(q - q2)) = dist ((q1 - q),(q2 - q)) by Th24
.= dist (q1,q2) by Th23 ;
::_thesis: verum
end;

theorem Th26: :: JORDAN1K:26
for p, q being Point of (TOP-REAL 2)
for r being Real holds dist ((r * p),(r * q)) = (abs r) * (dist (p,q))
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: for r being Real holds dist ((r * p),(r * q)) = (abs r) * (dist (p,q))
let r be Real; ::_thesis: dist ((r * p),(r * q)) = (abs r) * (dist (p,q))
thus  dist ((r * p),(r * q)) = dist (((r * p) - (r * p)),((r * p) - (r * q))) by Th25
.= dist (|[0,0]|,((r * p) - (r * q))) by EUCLID:42, EUCLID:54
.= dist (|[0,0]|,(r * (p - q))) by EUCLID:49
.= (abs r) * (dist (|[0,0]|,(p - q))) by Th20
.= (abs r) * (dist ((p - p),(p - q))) by EUCLID:42, EUCLID:54
.= (abs r) * (dist (p,q)) by Th25 ; ::_thesis: verum
end;

theorem Th27: :: JORDAN1K:27
for p, q being Point of (TOP-REAL 2)
for r being Real st r <= 1 holds
dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q))
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: for r being Real st r <= 1 holds
dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q))
let r be Real; ::_thesis: ( r <= 1 implies dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q)) )
assume  r <= 1 ; ::_thesis: dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q))
then  1 + r <= 1 + 1 by XREAL_1:6;
then  1 - r >= 1 - 1 by XREAL_1:21;
then A1: abs (1 - r) = 1 - r by ABSVALUE:def_1;
thus  dist (p,((r * p) + ((1 - r) * q))) = dist (((r + (1 - r)) * p),((r * p) + ((1 - r) * q))) by EUCLID:29
.= dist (((r * p) + ((1 - r) * p)),((r * p) + ((1 - r) * q))) by EUCLID:33
.= dist (((1 - r) * p),((1 - r) * q)) by Th21
.= (1 - r) * (dist (p,q)) by A1, Th26 ; ::_thesis: verum
end;

theorem Th28: :: JORDAN1K:28
for q, p being Point of (TOP-REAL 2)
for r being Real st 0 <= r holds
dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q))
proof
let q, p be Point of (TOP-REAL 2); ::_thesis: for r being Real st 0 <= r holds
dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q))
let r be Real; ::_thesis: ( 0 <= r implies dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q)) )
assume  0 <= r ; ::_thesis: dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q))
then A1: abs r = r by ABSVALUE:def_1;
thus  dist (q,((r * p) + ((1 - r) * q))) = dist (((r * p) + ((1 - r) * q)),((r + (1 - r)) * q)) by EUCLID:29
.= dist (((r * q) + ((1 - r) * q)),((r * p) + ((1 - r) * q))) by EUCLID:33
.= dist ((r * q),(r * p)) by Th21
.= r * (dist (p,q)) by A1, Th26 ; ::_thesis: verum
end;

theorem Th29: :: JORDAN1K:29
for p, q1, q2 being Point of (TOP-REAL 2) st p in LSeg (q1,q2) holds
(dist (q1,p)) + (dist (p,q2)) = dist (q1,q2)
proof
let p, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg (q1,q2) implies (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) )
assume  p in LSeg (q1,q2) ; ::_thesis: (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2)
then consider r being Real such that
A1: ( p = ((1 - r) * q1) + (r * q2) & 0 <= r & r <= 1 ) ;
 ( dist (q1,p) = r * (dist (q1,q2)) & dist (q2,p) = (1 - r) * (dist (q1,q2)) ) by A1, Th27, Th28;
hence  (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) ; ::_thesis: verum
end;

theorem :: JORDAN1K:30
for q1, q2, p being Point of (TOP-REAL 2) st q1 in LSeg (q2,p) & q1 <> q2 holds
dist (q1,p) < dist (q2,p)
proof
let q1, q2, p be Point of (TOP-REAL 2); ::_thesis: ( q1 in LSeg (q2,p) & q1 <> q2 implies dist (q1,p) < dist (q2,p) )
assume that
A1: q1 in LSeg (q2,p) and
A2: q1 <> q2 ; ::_thesis: dist (q1,p) < dist (q2,p)
 (dist (q2,q1)) + (dist (q1,p)) = dist (q2,p) by A1, Th29;
hence  dist (q1,p) < dist (q2,p) by A2, Th22, XREAL_1:29; ::_thesis: verum
end;

theorem Th31: :: JORDAN1K:31
for r being Real
for y being Point of (Euclid 2) st y = |[0,0]| holds
Ball (y,r) =  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }
proof
let r be Real; ::_thesis: for y being Point of (Euclid 2) st y = |[0,0]| holds
Ball (y,r) =  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }
let y be Point of (Euclid 2); ::_thesis: ( y = |[0,0]| implies Ball (y,r) =  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  )
set X =  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }  ;
set Y =  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  ;
A1:  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }  c=  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }  or u in  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  )
assume  u in  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }  ; ::_thesis: u in  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }
then consider q being Point of (TOP-REAL 2) such that
A2: ( u = q & |.(|[0,0]| - q).| < r ) ;
|.(|[0,0]| - q).| = |.(q - |[0,0]|).| by TOPRNS_1:27
.= |.q.| by EUCLID:54, RLVECT_1:13 ;
hence  u in  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  by A2; ::_thesis: verum
end;
A3:  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  c=  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  or u in  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }  )
assume  u in  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  ; ::_thesis: u in  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }
then consider q being Point of (TOP-REAL 2) such that
A4: ( u = q & |.q.| < r ) ;
|.(|[0,0]| - q).| = |.(q - |[0,0]|).| by TOPRNS_1:27
.= |.q.| by EUCLID:54, RLVECT_1:13 ;
hence  u in  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }  by A4; ::_thesis: verum
end;
assume  y = |[0,0]| ; ::_thesis: Ball (y,r) =  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }
hence  Ball (y,r) =  {  q where q is Point of (TOP-REAL 2) : |.(|[0,0]| - q).| < r  }  by JGRAPH_2:2
.=  {  q where q is Point of (TOP-REAL 2) : |.q.| < r  }  by A1, A3, XBOOLE_0:def_10 ;
::_thesis: verum
end;

begin

theorem Th32: :: JORDAN1K:32
for p being Point of (TOP-REAL 2)
for r, s1, s2 being Real holds (AffineMap (r,s1,r,s2)) . p = (r * p) + |[s1,s2]|
proof
let p be Point of (TOP-REAL 2); ::_thesis: for r, s1, s2 being Real holds (AffineMap (r,s1,r,s2)) . p = (r * p) + |[s1,s2]|
let r, s1, s2 be Real; ::_thesis: (AffineMap (r,s1,r,s2)) . p = (r * p) + |[s1,s2]|
thus (AffineMap (r,s1,r,s2)) . p = |[((r * (p `1)) + s1),((r * (p `2)) + s2)]| by JGRAPH_2:def_2
.= |[(((r * p) `1) + s1),((r * (p `2)) + s2)]| by TOPREAL3:4
.= |[(((r * p) `1) + s1),(((r * p) `2) + s2)]| by TOPREAL3:4
.= |[((r * p) `1),((r * p) `2)]| + |[s1,s2]| by EUCLID:56
.= (r * p) + |[s1,s2]| by EUCLID:53 ; ::_thesis: verum
end;

theorem Th33: :: JORDAN1K:33
for q, p being Point of (TOP-REAL 2)
for r being Real holds (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q
proof
let q, p be Point of (TOP-REAL 2); ::_thesis: for r being Real holds (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q
let r be Real; ::_thesis: (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q
thus (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + |[(q `1),(q `2)]| by Th32
.= (r * p) + q by EUCLID:53 ; ::_thesis: verum
end;

theorem Th34: :: JORDAN1K:34
for s1, s2, t1, t2 being Real st s1 > 0 & s2 > 0 holds
(AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2)
proof
let s1, s2, t1, t2 be Real; ::_thesis: ( s1 > 0 & s2 > 0 implies (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) )
 the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
then reconsider f = id (REAL 2) as Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) ;
assume that
A1: s1 > 0 and
A2: s2 > 0 ; ::_thesis: (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2)
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_((AffineMap_(s1,t1,s2,t2))_*_(AffineMap_((1_/_s1),(-_(t1_/_s1)),(1_/_s2),(-_(t2_/_s2)))))_._p_=_f_._p
let p be Point of (TOP-REAL 2); ::_thesis: ((AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))))) . p = f . p
set q = |[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]|;
A3: |[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2 = ((1 / s2) * (p `2)) - (t2 / s2) by EUCLID:52;
 p in the carrier of (TOP-REAL 2) ;
then A4: p in REAL 2 by EUCLID:22;
A5: s1 * (1 / s1) = 1 by A1, XCMPLX_1:106;
thus ((AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))))) . p = (AffineMap (s1,t1,s2,t2)) . ((AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) . p) by FUNCT_2:15
.= (AffineMap (s1,t1,s2,t2)) . |[(((1 / s1) * (p `1)) + (- (t1 / s1))),(((1 / s2) * (p `2)) + (- (t2 / s2)))]| by JGRAPH_2:def_2
.= |[((s1 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `1)) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by JGRAPH_2:def_2
.= |[((s1 * (((1 / s1) * (p `1)) - (t1 / s1))) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by EUCLID:52
.= |[((((s1 * (1 / s1)) * (p `1)) - (s1 * (t1 / s1))) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]|
.= |[(((1 * (p `1)) - (1 * t1)) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by A1, A5, XCMPLX_1:87
.= |[(p `1),(((s2 * ((1 / s2) * (p `2))) - (s2 * (t2 / s2))) + t2)]| by A3
.= |[(p `1),((((s2 * (1 / s2)) * (p `2)) - t2) + t2)]| by A2, XCMPLX_1:87
.= |[(p `1),(((1 * (p `2)) - (1 * t2)) + t2)]| by A2, XCMPLX_1:106
.= p by EUCLID:53
.= f . p by A4, FUNCT_1:18 ; ::_thesis: verum
end;
hence  (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th35: :: JORDAN1K:35
for q being Point of (TOP-REAL 2)
for r being Real
for y, x being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds
(AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
proof
let q be Point of (TOP-REAL 2); ::_thesis: for r being Real
for y, x being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds
(AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
let r be Real; ::_thesis: for y, x being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds
(AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
let y, x be Point of (Euclid 2); ::_thesis: ( y = |[0,0]| & x = q & r > 0 implies (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) )
assume that
A1: y = |[0,0]| and
A2: x = q and
A3: r > 0 ; ::_thesis: (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
reconsider A = Ball (y,1), B = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:8;
A4: B c= (AffineMap (r,(q `1),r,(q `2))) .: A
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in B or u in (AffineMap (r,(q `1),r,(q `2))) .: A )
assume A5: u in B ; ::_thesis: u in (AffineMap (r,(q `1),r,(q `2))) .: A
then reconsider q1 = u as Point of (TOP-REAL 2) ;
reconsider x1 = q1 as Element of (Euclid 2) by TOPREAL3:8;
set q2 = (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1;
consider z1, z2 being Point of (Euclid 2) such that
A6: z1 = q and
A7: z2 = (r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q and
A8: dist (q,((r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q)) = dist (z1,z2) by TOPREAL6:def_1;
consider z3, z4 being Point of (Euclid 2) such that
A9: z3 = |[0,0]| and
A10: z4 = (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1 and
A11: dist (|[0,0]|,((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) = dist (z3,z4) by TOPREAL6:def_1;
z2 = (AffineMap (r,(q `1),r,(q `2))) . ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1) by A7, Th33
.= ((AffineMap (r,(q `1),r,(q `2))) * (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r))))) . q1 by FUNCT_2:15
.= (id (REAL 2)) . q1 by A3, Th34
.= x1 by FUNCT_1:18 ;
then  dist (x,x1) = dist ((|[0,0]| + q),((r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q)) by A2, A6, A8, EUCLID:27, EUCLID:54
.= dist (|[0,0]|,(r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1))) by Th21
.= (abs r) * (dist (|[0,0]|,((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1))) by Th20
.= r * (dist (y,z4)) by A1, A3, A9, A11, ABSVALUE:def_1 ;
then  r * (dist (y,z4)) < 1 * r by A5, METRIC_1:11;
then  dist (y,z4) < 1 by A3, XREAL_1:64;
then A12: (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1 in A by A10, METRIC_1:11;
(AffineMap (r,(q `1),r,(q `2))) . ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1) = ((AffineMap (r,(q `1),r,(q `2))) * (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r))))) . q1 by FUNCT_2:15
.= (id (REAL 2)) . q1 by A3, Th34
.= (id (TOP-REAL 2)) . q1 by EUCLID:22
.= q1 by FUNCT_1:18 ;
hence  u in (AffineMap (r,(q `1),r,(q `2))) .: A by A12, FUNCT_2:35; ::_thesis: verum
end;
 (AffineMap (r,(q `1),r,(q `2))) .: A c= B
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (AffineMap (r,(q `1),r,(q `2))) .: A or u in B )
assume A13: u in (AffineMap (r,(q `1),r,(q `2))) .: A ; ::_thesis: u in B
then reconsider q1 = u as Point of (TOP-REAL 2) ;
consider q2 being Point of (TOP-REAL 2) such that
A14: q2 in A and
A15: q1 = (AffineMap (r,(q `1),r,(q `2))) . q2 by A13, FUNCT_2:65;
reconsider x1 = q1, x2 = q2 as Element of (Euclid 2) by TOPREAL3:8;
A16: dist (y,x2) < 1 by A14, METRIC_1:11;
A17: ex z3, z4 being Point of (Euclid 2) st
( z3 = |[0,0]| & z4 = q2 & dist (|[0,0]|,q2) = dist (z3,z4) ) by TOPREAL6:def_1;
A18: ex z1, z2 being Point of (Euclid 2) st
( z1 = q & z2 = (r * q2) + q & dist (q,((r * q2) + q)) = dist (z1,z2) ) by TOPREAL6:def_1;
 q1 = (r * q2) + q by A15, Th33;
then  dist (x,x1) = dist ((|[0,0]| + q),((r * q2) + q)) by A2, A18, EUCLID:27, EUCLID:54
.= dist (|[0,0]|,(r * q2)) by Th21
.= (abs r) * (dist (|[0,0]|,q2)) by Th20
.= r * (dist (y,x2)) by A1, A3, A17, ABSVALUE:def_1 ;
then  dist (x,x1) < r by A3, A16, XREAL_1:157;
hence  u in B by METRIC_1:11; ::_thesis: verum
end;
hence  (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th36: :: JORDAN1K:36
for A, B, C, D being Real st A > 0 & C > 0 holds
AffineMap (A,B,C,D) is onto
proof
let A, B, C, D be Real; ::_thesis: ( A > 0 & C > 0 implies AffineMap (A,B,C,D) is onto )
assume A1: ( A > 0 & C > 0 ) ; ::_thesis: AffineMap (A,B,C,D) is onto
thus  rng (AffineMap (A,B,C,D)) c= the carrier of (TOP-REAL 2) ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of (TOP-REAL 2) c= rng (AffineMap (A,B,C,D))
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the carrier of (TOP-REAL 2) or e in rng (AffineMap (A,B,C,D)) )
assume  e in the carrier of (TOP-REAL 2) ; ::_thesis: e in rng (AffineMap (A,B,C,D))
then reconsider q1 = e as Point of (TOP-REAL 2) ;
set q2 = (AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))) . q1;
A2: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
(AffineMap (A,B,C,D)) . ((AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))) . q1) = ((AffineMap (A,B,C,D)) * (AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C))))) . q1 by FUNCT_2:15
.= (id (REAL 2)) . q1 by A1, Th34
.= q1 by A2, FUNCT_1:18 ;
hence  e in rng (AffineMap (A,B,C,D)) by FUNCT_2:4; ::_thesis: verum
end;

theorem :: JORDAN1K:37
for r being Real
for x being Point of (Euclid 2) holds (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)
proof
let r be Real; ::_thesis: for x being Point of (Euclid 2) holds (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)
let x be Point of (Euclid 2); ::_thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)
set C = (Ball (x,r)) ` ;
percases ( r <= 0 or r > 0 ) ;
suppose r <= 0 ; ::_thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)
then  Ball (x,r) = {} (TOP-REAL 2) by TBSP_1:12;
then A1: (Ball (x,r)) ` = [#] (TOP-REAL 2) by TOPREAL3:8;
thus  (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) by A1; ::_thesis: verum
end;
supposeA2: r > 0 ; ::_thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)
reconsider q = x as Point of (TOP-REAL 2) by TOPREAL3:8;
reconsider y = |[0,0]| as Point of (Euclid 2) by TOPREAL3:8;
reconsider Q = Ball (x,r), J = Ball (y,1) as Subset of (TOP-REAL 2) by TOPREAL3:8;
A3: Q = (AffineMap (r,(q `1),r,(q `2))) .: J by A2, Th35;
reconsider P = Q ` , K = J ` as Subset of (TOP-REAL 2) ;
A4: K = (REAL 2) \ (Ball (y,1)) by TOPREAL3:8
.= (REAL 2) \  {  q1 where q1 is Point of (TOP-REAL 2) : |.q1.| < 1  }  by Th31 ;
 ( AffineMap (r,(q `1),r,(q `2)) is one-to-one & AffineMap (r,(q `1),r,(q `2)) is onto ) by A2, Th36, JGRAPH_2:44;
then  ( the carrier of (TOP-REAL 2) = the carrier of (Euclid 2) & P = (AffineMap (r,(q `1),r,(q `2))) .: K ) by A3, Th5, TOPREAL3:8;
hence  (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) by A4, JORDAN2C:53, TOPS_2:61; ::_thesis: verum
end;
end;
end;

begin

definition
let n be Element of NAT ;
let A, B be Subset of (TOP-REAL n);
func dist_min (A,B) ->  Real means :Def1: :: JORDAN1K:def 1
 ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & it = min_dist_min (A9,B9) );
existence
 ex b1 being Real ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b1 = min_dist_min (A9,B9) )
proof
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider A9 = A, B9 = B as Subset of (TopSpaceMetr (Euclid n)) ;
take  min_dist_min (A9,B9) ; ::_thesis: ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) )
take  A9 ; ::_thesis: ex B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) )
take  B9 ; ::_thesis: ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) )
thus  ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b1 = min_dist_min (A9,B9) ) & ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b2 = min_dist_min (A9,B9) ) holds
b1 = b2 ;
end;

:: deftheorem Def1 defines dist_min JORDAN1K:def_1_:_
 for n being Element of NAT
for A, B being Subset of (TOP-REAL n)
for b4 being Real holds
( b4 = dist_min (A,B) iff ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b4 = min_dist_min (A9,B9) ) );

definition
let M be non empty MetrSpace;
let P, Q be non empty compact Subset of (TopSpaceMetr M);
:: original: min_dist_min
redefine func min_dist_min (P,Q) ->  Element of REAL ;
commutativity
 for P, Q being non empty compact Subset of (TopSpaceMetr M) holds min_dist_min (P,Q) = min_dist_min (Q,P)
proof
let P, Q be non empty compact Subset of (TopSpaceMetr M); ::_thesis: min_dist_min (P,Q) = min_dist_min (Q,P)
consider y1, y2 being Point of M such that
A1: ( y1 in Q & y2 in P ) and
A2: dist (y1,y2) = min_dist_min (Q,P) by WEIERSTR:30;
consider x1, x2 being Point of M such that
A3: ( x1 in P & x2 in Q ) and
A4: dist (x1,x2) = min_dist_min (P,Q) by WEIERSTR:30;
 ( dist (x1,x2) <= dist (y1,y2) & dist (y1,y2) <= dist (x1,x2) ) by A1, A2, A3, A4, WEIERSTR:34;
hence  min_dist_min (P,Q) = min_dist_min (Q,P) by A2, A4, XXREAL_0:1; ::_thesis: verum
end;
:: original: max_dist_max
redefine func max_dist_max (P,Q) ->  Element of REAL ;
commutativity
 for P, Q being non empty compact Subset of (TopSpaceMetr M) holds max_dist_max (P,Q) = max_dist_max (Q,P)
proof
let P, Q be non empty compact Subset of (TopSpaceMetr M); ::_thesis: max_dist_max (P,Q) = max_dist_max (Q,P)
consider y1, y2 being Point of M such that
A5: ( y1 in Q & y2 in P ) and
A6: dist (y1,y2) = max_dist_max (Q,P) by WEIERSTR:33;
consider x1, x2 being Point of M such that
A7: ( x1 in P & x2 in Q ) and
A8: dist (x1,x2) = max_dist_max (P,Q) by WEIERSTR:33;
 ( dist (x1,x2) <= dist (y1,y2) & dist (y1,y2) <= dist (x1,x2) ) by A5, A6, A7, A8, WEIERSTR:34;
hence  max_dist_max (P,Q) = max_dist_max (Q,P) by A6, A8, XXREAL_0:1; ::_thesis: verum
end;
end;

definition
let n be Element of NAT ;
let A, B be non empty compact Subset of (TOP-REAL n);
:: original: dist_min
redefine func dist_min (A,B) ->  Real;
commutativity
 for A, B being non empty compact Subset of (TOP-REAL n) holds dist_min (A,B) = dist_min (B,A)
proof
let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: dist_min (A,B) = dist_min (B,A)
consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that
A1: ( A = A9 & B = B9 ) and
A2: dist_min (A,B) = min_dist_min (A9,B9) by Def1;
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider A9 = A9, B9 = B9 as non empty compact Subset of (TopSpaceMetr (Euclid n)) by A1, COMPTS_1:23;
 dist_min (A,B) = min_dist_min (B9,A9) by A2;
hence  dist_min (A,B) = dist_min (B,A) by A1, Def1; ::_thesis: verum
end;
end;

theorem Th38: :: JORDAN1K:38
for n being Element of NAT
for A, B being non empty Subset of (TOP-REAL n) holds dist_min (A,B) >= 0
proof
let n be Element of NAT ; ::_thesis: for A, B being non empty Subset of (TOP-REAL n) holds dist_min (A,B) >= 0
let A, B be non empty Subset of (TOP-REAL n); ::_thesis: dist_min (A,B) >= 0
 ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & dist_min (A,B) = min_dist_min (A9,B9) ) by Def1;
hence  dist_min (A,B) >= 0 by Th11; ::_thesis: verum
end;

theorem Th39: :: JORDAN1K:39
for n being Element of NAT
for A, B being compact Subset of (TOP-REAL n) st A meets B holds
dist_min (A,B) = 0
proof
let n be Element of NAT ; ::_thesis: for A, B being compact Subset of (TOP-REAL n) st A meets B holds
dist_min (A,B) = 0
let A, B be compact Subset of (TOP-REAL n); ::_thesis: ( A meets B implies dist_min (A,B) = 0 )
assume A1: A meets B ; ::_thesis: dist_min (A,B) = 0
consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that
A2: ( A = A9 & B = B9 ) and
A3: dist_min (A,B) = min_dist_min (A9,B9) by Def1;
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then  ( A9 is compact & B9 is compact ) by A2, COMPTS_1:23;
hence  dist_min (A,B) = 0 by A1, A2, A3, Th12; ::_thesis: verum
end;

theorem Th40: :: JORDAN1K:40
for n being Element of NAT
for r being Real
for A, B being non empty Subset of (TOP-REAL n) st ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) holds
dist_min (A,B) >= r
proof
let n be Element of NAT ; ::_thesis: for r being Real
for A, B being non empty Subset of (TOP-REAL n) st ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) holds
dist_min (A,B) >= r
let r be Real; ::_thesis: for A, B being non empty Subset of (TOP-REAL n) st ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) holds
dist_min (A,B) >= r
let A, B be non empty Subset of (TOP-REAL n); ::_thesis: ( ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) implies dist_min (A,B) >= r )
assume A1: for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ; ::_thesis: dist_min (A,B) >= r
A2: for p, q being Point of (Euclid n) st p in A & q in B holds
dist (p,q) >= r
proof
let a, b be Point of (Euclid n); ::_thesis: ( a in A & b in B implies dist (a,b) >= r )
assume A3: ( a in A & b in B ) ; ::_thesis: dist (a,b) >= r
reconsider p = a, q = b as Point of (TOP-REAL n) by TOPREAL3:8;
 ex a, b being Point of (Euclid n) st
( p = a & q = b & dist (p,q) = dist (a,b) ) by TOPREAL6:def_1;
hence  dist (a,b) >= r by A1, A3; ::_thesis: verum
end;
 ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & dist_min (A,B) = min_dist_min (A9,B9) ) by Def1;
hence  dist_min (A,B) >= r by A2, Th13; ::_thesis: verum
end;

theorem Th41: :: JORDAN1K:41
for n being Element of NAT
for D being Subset of (TOP-REAL n)
for A, C being non empty Subset of (TOP-REAL n) st C c= D holds
dist_min (A,D) <= dist_min (A,C)
proof
let n be Element of NAT ; ::_thesis: for D being Subset of (TOP-REAL n)
for A, C being non empty Subset of (TOP-REAL n) st C c= D holds
dist_min (A,D) <= dist_min (A,C)
let D be Subset of (TOP-REAL n); ::_thesis: for A, C being non empty Subset of (TOP-REAL n) st C c= D holds
dist_min (A,D) <= dist_min (A,C)
let A, C be non empty Subset of (TOP-REAL n); ::_thesis: ( C c= D implies dist_min (A,D) <= dist_min (A,C) )
assume A1: C c= D ; ::_thesis: dist_min (A,D) <= dist_min (A,C)
consider A9, D9 being Subset of (TopSpaceMetr (Euclid n)) such that
A2: A = A9 and
A3: ( D = D9 & dist_min (A,D) = min_dist_min (A9,D9) ) by Def1;
reconsider f = dist_min A9 as Function of the carrier of (TopSpaceMetr (Euclid n)),REAL by TOPMETR:17;
reconsider Y = f .: D9 as Subset of REAL ;
A4: Y is bounded_below
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of Y
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Y or 0 <= r )
assume  r in Y ; ::_thesis: 0 <= r
then  ex c being Element of (TopSpaceMetr (Euclid n)) st
( c in D9 & r = f . c ) by FUNCT_2:65;
hence  0 <= r by A2, Th9; ::_thesis: verum
end;
A5: lower_bound Y = lower_bound ([#] ((dist_min A9) .: D9)) by WEIERSTR:def_1
.= lower_bound ((dist_min A9) .: D9) by WEIERSTR:def_3
.= min_dist_min (A9,D9) by WEIERSTR:def_7 ;
consider A99, C9 being Subset of (TopSpaceMetr (Euclid n)) such that
A6: A = A99 and
A7: C = C9 and
A8: dist_min (A,C) = min_dist_min (A99,C9) by Def1;
 dom f = the carrier of (TopSpaceMetr (Euclid n)) by FUNCT_2:def_1;
then reconsider X = f .: C9 as non empty Subset of REAL by A7;
lower_bound X = lower_bound ([#] ((dist_min A9) .: C9)) by WEIERSTR:def_1
.= lower_bound ((dist_min A9) .: C9) by WEIERSTR:def_3
.= min_dist_min (A9,C9) by WEIERSTR:def_7 ;
hence  dist_min (A,D) <= dist_min (A,C) by A1, A2, A3, A6, A7, A8, A5, A4, RELAT_1:123, SEQ_4:47; ::_thesis: verum
end;

theorem Th42: :: JORDAN1K:42
for n being Element of NAT
for A, B being non empty compact Subset of (TOP-REAL n) ex p, q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )
proof
let n be Element of NAT ; ::_thesis: for A, B being non empty compact Subset of (TOP-REAL n) ex p, q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )
let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: ex p, q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )
consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that
A1: ( A = A9 & B = B9 ) and
A2: dist_min (A,B) = min_dist_min (A9,B9) by Def1;
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then  ( A9 is compact & B9 is compact ) by A1, COMPTS_1:23;
then consider x1, x2 being Point of (Euclid n) such that
A3: ( x1 in A9 & x2 in B9 ) and
A4: dist (x1,x2) = min_dist_min (A9,B9) by A1, WEIERSTR:30;
reconsider p = x1, q = x2 as Point of (TOP-REAL n) by TOPREAL3:8;
take  p ; ::_thesis: ex q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )
take  q ; ::_thesis: ( p in A & q in B & dist_min (A,B) = dist (p,q) )
thus  ( p in A & q in B ) by A1, A3; ::_thesis: dist_min (A,B) = dist (p,q)
thus  dist_min (A,B) = dist (p,q) by A2, A4, TOPREAL6:def_1; ::_thesis: verum
end;

theorem Th43: :: JORDAN1K:43
for n being Element of NAT
for p, q being Point of (TOP-REAL n) holds dist_min ({p},{q}) = dist (p,q)
proof
let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) holds dist_min ({p},{q}) = dist (p,q)
let p, q be Point of (TOP-REAL n); ::_thesis: dist_min ({p},{q}) = dist (p,q)
consider p9, q9 being Point of (TOP-REAL n) such that
A1: p9 in {p} and
A2: ( q9 in {q} & dist_min ({p},{q}) = dist (p9,q9) ) by Th42;
 p = p9 by A1, TARSKI:def_1;
hence  dist_min ({p},{q}) = dist (p,q) by A2, TARSKI:def_1; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let p be Point of (TOP-REAL n);
let B be Subset of (TOP-REAL n);
func dist (p,B) ->  Real equals :: JORDAN1K:def 2
 dist_min ({p},B);
coherence
 dist_min ({p},B) is Real ;
end;

:: deftheorem  defines dist JORDAN1K:def_2_:_
 for n being Element of NAT
for p being Point of (TOP-REAL n)
for B being Subset of (TOP-REAL n) holds dist (p,B) = dist_min ({p},B);

theorem :: JORDAN1K:44
for n being Element of NAT
for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds dist (p,A) >= 0 by Th38;

theorem :: JORDAN1K:45
for n being Element of NAT
for A being compact Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st p in A holds
dist (p,A) = 0 by Th39, ZFMISC_1:48;

theorem Th46: :: JORDAN1K:46
for n being Element of NAT
for A being non empty compact Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )
proof
let n be Element of NAT ; ::_thesis: for A being non empty compact Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )
let A be non empty compact Subset of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n) ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )
let p be Point of (TOP-REAL n); ::_thesis: ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )
consider q, p9 being Point of (TOP-REAL n) such that
A1: q in A and
A2: ( p9 in {p} & dist_min (A,{p}) = dist (q,p9) ) by Th42;
take  q ; ::_thesis: ( q in A & dist (p,A) = dist (p,q) )
thus  q in A by A1; ::_thesis: dist (p,A) = dist (p,q)
thus  dist (p,A) = dist (p,q) by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem :: JORDAN1K:47
for n being Element of NAT
for C being non empty Subset of (TOP-REAL n)
for D being Subset of (TOP-REAL n) st C c= D holds
for q being Point of (TOP-REAL n) holds dist (q,D) <= dist (q,C) by Th41;

theorem :: JORDAN1K:48
for n being Element of NAT
for r being Real
for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) st q in A holds
dist (p,q) >= r ) holds
dist (p,A) >= r
proof
let n be Element of NAT ; ::_thesis: for r being Real
for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) st q in A holds
dist (p,q) >= r ) holds
dist (p,A) >= r
let r be Real; ::_thesis: for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) st q in A holds
dist (p,q) >= r ) holds
dist (p,A) >= r
let A be non empty Subset of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) st q in A holds
dist (p,q) >= r ) holds
dist (p,A) >= r
let p9 be Point of (TOP-REAL n); ::_thesis: ( ( for q being Point of (TOP-REAL n) st q in A holds
dist (p9,q) >= r ) implies dist (p9,A) >= r )
assume A1: for q being Point of (TOP-REAL n) st q in A holds
dist (p9,q) >= r ; ::_thesis: dist (p9,A) >= r
 for p, q being Point of (TOP-REAL n) st p in {p9} & q in A holds
dist (p,q) >= r
proof
let p, q be Point of (TOP-REAL n); ::_thesis: ( p in {p9} & q in A implies dist (p,q) >= r )
assume that
A2: p in {p9} and
A3: q in A ; ::_thesis: dist (p,q) >= r
 p = p9 by A2, TARSKI:def_1;
hence  dist (p,q) >= r by A1, A3; ::_thesis: verum
end;
hence  dist (p9,A) >= r by Th40; ::_thesis: verum
end;

theorem :: JORDAN1K:49
for n being Element of NAT
for p, q being Point of (TOP-REAL n) holds dist (p,{q}) = dist (p,q) by Th43;

theorem Th50: :: JORDAN1K:50
for n being Element of NAT
for A being non empty Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st q in A holds
dist (p,A) <= dist (p,q)
proof
let n be Element of NAT ; ::_thesis: for A being non empty Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st q in A holds
dist (p,A) <= dist (p,q)
let A be non empty Subset of (TOP-REAL n); ::_thesis: for p, q being Point of (TOP-REAL n) st q in A holds
dist (p,A) <= dist (p,q)
let p, q be Point of (TOP-REAL n); ::_thesis: ( q in A implies dist (p,A) <= dist (p,q) )
assume  q in A ; ::_thesis: dist (p,A) <= dist (p,q)
then  {q} c= A by ZFMISC_1:31;
then  dist (p,A) <= dist (p,{q}) by Th41;
hence  dist (p,A) <= dist (p,q) by Th43; ::_thesis: verum
end;

theorem :: JORDAN1K:51
for A being non empty compact Subset of (TOP-REAL 2)
for B being open Subset of (TOP-REAL 2) st A c= B holds
for p being Point of (TOP-REAL 2) st not p in B holds
dist (p,B) < dist (p,A)
proof
let A be non empty compact Subset of (TOP-REAL 2); ::_thesis: for B being open Subset of (TOP-REAL 2) st A c= B holds
for p being Point of (TOP-REAL 2) st not p in B holds
dist (p,B) < dist (p,A)
let B be open Subset of (TOP-REAL 2); ::_thesis: ( A c= B implies for p being Point of (TOP-REAL 2) st not p in B holds
dist (p,B) < dist (p,A) )
assume A1: A c= B ; ::_thesis: for p being Point of (TOP-REAL 2) st not p in B holds
dist (p,B) < dist (p,A)
 TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8;
then reconsider P = B as open Subset of (TopSpaceMetr (Euclid 2)) by PRE_TOPC:30;
let p be Point of (TOP-REAL 2); ::_thesis: ( not p in B implies dist (p,B) < dist (p,A) )
assume A2: not p in B ; ::_thesis: dist (p,B) < dist (p,A)
assume A3: dist (p,B) >= dist (p,A) ; ::_thesis: contradiction
 dist (p,B) <= dist (p,A) by A1, Th41;
then A4: dist (p,B) = dist (p,A) by A3, XXREAL_0:1;
consider q being Point of (TOP-REAL 2) such that
A5: q in A and
A6: dist (p,A) = dist (p,q) by Th46;
reconsider a = q as Point of (Euclid 2) by TOPREAL3:8;
consider r being real number  such that
A7: r > 0 and
A8: Ball (a,r) c= P by A1, A5, TOPMETR:15;
reconsider r = r as Element of REAL by XREAL_0:def_1;
set s = r / (2 * (dist (p,q)));
set q9 = ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p);
 a in P by A1, A5;
then A9: dist (p,q) > 0 by A2, Th22;
then A10: 2 * (dist (p,q)) > 0 by XREAL_1:129;
then  0 < r / (2 * (dist (p,q))) by A7, XREAL_1:139;
then A11: 1 - (r / (2 * (dist (p,q)))) < 1 - 0 by XREAL_1:10;
A12: ex p1, q1 being Point of (Euclid 2) st
( p1 = q & q1 = ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p) & dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) = dist (p1,q1) ) by TOPREAL6:def_1;
dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) = ((1 * r) / (2 * (dist (p,q)))) * (dist (p,q)) by A7, A9, Th28
.= ((r / 2) / ((dist (p,q)) / 1)) * (dist (p,q)) by XCMPLX_1:84
.= r / 2 by A9, XCMPLX_1:87 ;
then  dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) < r / 1 by A7, XREAL_1:76;
then A13: ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p) in Ball (a,r) by A12, METRIC_1:11;
now__::_thesis:_not_r_>_dist_(p,q)
A14: ex p1, q1 being Point of (Euclid 2) st
( p1 = p & q1 = q & dist (p,q) = dist (p1,q1) ) by TOPREAL6:def_1;
assume  r > dist (p,q) ; ::_thesis: contradiction
then  p in Ball (a,r) by A14, METRIC_1:11;
hence  contradiction by A2, A8; ::_thesis: verum
end;
then  1 * r < 2 * (dist (p,q)) by A7, XREAL_1:98;
then  r / (2 * (dist (p,q))) < 1 by A10, XREAL_1:191;
then  dist (p,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) = (1 - (r / (2 * (dist (p,q))))) * (dist (p,q)) by Th27;
hence  contradiction by A4, A6, A8, A9, A13, A11, Th50, XREAL_1:157; ::_thesis: verum
end;