:: On the Decompositions of Intervals and Simple Closed Curves
::  by Adam Grabowski
::
:: Received August 7, 2002
:: Copyright (c) 2002 Association of Mizar Users

environ

 vocabularies NUMBERS, ZFMISC_1, TOPREAL2, PRE_TOPC, EUCLID, XBOOLE_0,
      SUBSET_1, TARSKI, STRUCT_0, FUNCT_1, RELAT_1, FUNCT_4, PARTFUN1,
      TOPREAL1, XREAL_0, ORDINAL1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1,
      BORSUK_1, XXREAL_1, TOPMETR, CONNSP_1, INTEGRA1, REAL_1, RELAT_2,
      RCOMP_1, XXREAL_2, ORDINAL2, SEQ_4, T_0TOPSP, TOPS_2, RLTOPSP1, TREAL_1,
      VALUED_1, MEMBERED, JORDAN2C, BORSUK_4;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, REALSET1,
      MEMBERED, DOMAIN_1, RCOMP_1, FUNCT_4, XXREAL_0, STRUCT_0, PRE_TOPC,
      COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, SEQ_4, TREAL_1, CONNSP_1,
      BORSUK_1, BORSUK_3, TSEP_1, TOPMETR, MEASURE6, INTEGRA1, TOPS_2,
      JORDAN2C;
 constructors FUNCT_4, CONNSP_1, TOPS_2, COMPTS_1, REALSET2, TSEP_1, TOPREAL1,
      TOPREAL2, TREAL_1, JORDAN1, MEASURE6, JORDAN2C, BORSUK_3, INTEGRA1,
      XXREAL_2, SEQ_4, CONVEX1, BINOP_2, RVSUM_1;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED,
      RCOMP_1, REALSET1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, TEX_2,
      EUCLID, TOPREAL1, TOPREAL2, BORSUK_2, REVROT_1, TOPREAL6, INTEGRA1,
      XXREAL_2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions XBOOLE_0, TARSKI, CONNSP_1, PARTFUN1, JORDAN1, SUBSET_1, STRUCT_0,
      RELAT_1;
 theorems TOPS_2, T_0TOPSP, BORSUK_1, PRE_TOPC, COMPTS_1, TARSKI, TOPMETR,
      TOPREAL1, RCOMP_1, CONNSP_1, ZFMISC_1, JORDAN5A, XREAL_0, STRUCT_0,
      TOPREAL6, MEASURE6, TREAL_1, XBOOLE_0, XBOOLE_1, JORDAN6, SEQ_4,
      INTEGRA1, INTEGRA2, TSEP_1, TOPREAL2, JORDAN5B, FUNCT_2, FUNCT_1,
      GOBOARD9, RELAT_1, PARTFUN1, RFUNCT_2, BORSUK_3, FUNCT_4, JGRAPH_2,
      TOPMETR2, TEX_2, REALSET1, XREAL_1, FRECHET, ENUMSET1, JORDAN2C,
      XXREAL_0, XXREAL_1, XXREAL_2;

begin :: Preliminaries

registration
  cluster -> non trivial Simple_closed_curve;
  coherence
  proof
    let D be Simple_closed_curve;
    ex p1,p2 being Point of TOP-REAL 2 st p1 <> p2 & p1 in D & p2 in D by
TOPREAL2:5;
    hence thesis by REALSET1:14;
  end;
end;

theorem Th1:
  for X being non empty set, A, B being non empty Subset of X st A
  c< B holds ex p being Element of X st p in B & A c= B \ {p}
proof
  let X be non empty set, A, B be non empty Subset of X;
  assume
A1: A c< B;
  then B \ A <> {} by XBOOLE_1:105;
  then consider p being set such that
A2: p in B \ A by XBOOLE_0:def 1;
A3: not p in A by A2,XBOOLE_0:def 5;
  reconsider p as Element of X by A2;
  take p;
  A c= B by A1,XBOOLE_0:def 8;
  hence thesis by A2,A3,XBOOLE_0:def 5,ZFMISC_1:40;
end;

theorem Th2:
  for X being non empty set, A being non empty Subset of X holds A
  is trivial implies ex x being Element of X st A = {x}
proof
  let X be non empty set, A be non empty Subset of X;
  assume
  A is trivial;
  then ex s being Element of A st A = {s} by TEX_2:def 1;
  hence thesis;
end;

registration
  let T be non trivial 1-sorted;
  cluster non trivial Subset of T;
  existence
  proof
    consider x, y being Element of T such that
A1: x <> y by STRUCT_0:def 10;
    take X = {x, y};
A2: y in X by TARSKI:def 2;
    x in X by TARSKI:def 2;
    hence thesis by A1,A2,REALSET1:15;
  end;
end;

theorem Th3:
  for X being non trivial set, p being set ex q being Element of X
  st q <> p
proof
  let X be non trivial set, p be set;
  X \ { p } is non empty by REALSET1:4;
  then consider q being set such that
A1: q in X \ { p } by XBOOLE_0:def 1;
  reconsider q as Element of X by A1;
  take q;
  thus thesis by A1,ZFMISC_1:64;
end;

registration
  let X be non trivial set;
  cluster non trivial Subset of X;
  existence
  proof
    take [#]X;
    thus thesis;
  end;
end;

theorem Th4:
  for T being non trivial set, X being non trivial Subset of T, p
  being set ex q being Element of T st q in X & q <> p
proof
  let T be non trivial set, X be non trivial Subset of T, p be set;
  set p9 = p;
  X \ { p9 } is non empty by REALSET1:4;
  then consider q being set such that
A1: q in X \ { p9 } by XBOOLE_0:def 1;
  reconsider q as Element of T by A1;
  take q;
  thus thesis by A1,ZFMISC_1:64;
end;

theorem Th5:
  for f, g being Function, a being set st f is one-to-one & g is
one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } holds f +* g is
  one-to-one
proof
  let f, g be Function, a be set;
  assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: dom f /\ dom g = { a } and
A4: rng f /\ rng g = { f.a };
  for x1,x2 being set st x1 in dom g & x2 in dom f \ dom g holds g.x1 <> f
  .x2
  proof
    { a } c= dom g by A3,XBOOLE_1:17;
    then
A5: a in dom g by ZFMISC_1:37;
    { a } c= dom f by A3,XBOOLE_1:17;
    then
A6: a in dom f by ZFMISC_1:37;
    let x1,x2 be set;
    assume that
A7: x1 in dom g and
A8: x2 in dom f \ dom g;
A9: f.x2 in rng f by A8,FUNCT_1:12;
    assume
A10: g.x1 = f.x2;
    g.x1 in rng g by A7,FUNCT_1:12;
    then f.x2 in rng f /\ rng g by A9,A10,XBOOLE_0:def 4;
    then f.x2 = f.a by A4,TARSKI:def 1;
    then x2 = a by A1,A8,A6,FUNCT_1:def 8;
    then dom g meets (dom f \ dom g) by A8,A5,XBOOLE_0:3;
    hence thesis by XBOOLE_1:79;
  end;
  hence thesis by A1,A2,TOPMETR2:2;
end;

theorem Th6:
  for f, g being Function, a being set st f is one-to-one & g is
  one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } & f.a = g.a
  holds (f +* g)" = f" +* g"
proof
  let f, g be Function, a be set;
  assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: dom f /\ dom g = { a } and
A4: rng f /\ rng g = { f.a } and
A5: f.a = g.a;
A6: dom (g") = rng g by A2,FUNCT_1:55;
A7: dom (f") = rng f by A1,FUNCT_1:55;
  for x being set st x in dom (f") /\ dom (g") holds f".x = g".x
  proof
    let x be set;
    { a } c= dom f by A3,XBOOLE_1:17;
    then
A8: a in dom f by ZFMISC_1:37;
    assume
A9: x in dom (f") /\ dom (g");
    then x = f.a by A4,A7,A6,TARSKI:def 1;
    then
A10: a = f".x by A1,A8,FUNCT_1:54;
    { a } c= dom g by A3,XBOOLE_1:17;
    then
A11: a in dom g by ZFMISC_1:37;
    x = g.a by A4,A5,A7,A6,A9,TARSKI:def 1;
    hence thesis by A2,A11,A10,FUNCT_1:54;
  end;
  then
A12: f" tolerates g" by PARTFUN1:def 6;
  set gf = f" +* g", F = f +* g;
  for x being set st x in dom f /\ dom g holds f.x = g.x
  proof
    let x be set;
    assume
    x in dom f /\ dom g;
    then x = a by A3,TARSKI:def 1;
    hence thesis by A5;
  end;
  then
A13: f tolerates g by PARTFUN1:def 6;
  dom gf = (dom (f")) \/ (dom (g")) by FUNCT_4:def 1
    .= (rng f) \/ (dom (g")) by A1,FUNCT_1:55
    .= (rng f) \/ (rng g) by A2,FUNCT_1:55;
  then
A14: dom gf = rng F by A13,FRECHET:39;
A15: dom F = (dom f) \/ (dom g) by FUNCT_4:def 1;
  then
A16: dom f c= dom F by XBOOLE_1:7;
A17: dom g c= dom F by A15,XBOOLE_1:7;
A18: rng F = (rng f) \/ (rng g) by A13,FRECHET:39;
A19: for y,x being set holds y in rng F & x = gf.y iff x in dom F & y = F.x
  proof
    let y,x be set;
    hereby
      assume that
A20:  y in rng F and
A21:  x = gf.y;
      per cases by A14,A20,FUNCT_4:13;
      suppose
A22:    y in dom (f");
        then
A23:    y in rng f by A1,FUNCT_1:55;
A24:    x = f".y by A12,A21,A22,FUNCT_4:16;
        then
A25:    y = f.x by A1,A23,FUNCT_1:54;
        x in dom f by A1,A23,A24,FUNCT_1:54;
        hence x in dom F & y = F.x by A13,A16,A25,FUNCT_4:16;
      end;
      suppose
A26:    y in dom (g");
        then
A27:    x = g".y by A21,FUNCT_4:14;
A28:    y in rng g by A2,A26,FUNCT_1:55;
        then
A29:    y = g.x by A2,A27,FUNCT_1:54;
        x in dom g by A2,A28,A27,FUNCT_1:54;
        hence x in dom F & y = F.x by A17,A29,FUNCT_4:14;
      end;
    end;
    assume that
A30: x in dom F and
A31: y = F.x;
    per cases by A30,FUNCT_4:13;
    suppose
A32:  x in dom f;
      then
A33:  y = f.x by A13,A31,FUNCT_4:16;
      then
A34:  x = f".y by A1,A32,FUNCT_1:54;
      rng F = (rng f) \/ (rng g) by A13,FRECHET:39;
      then
A35:  rng f c= rng F by XBOOLE_1:7;
A36:  y in rng f by A32,A33,FUNCT_1:12;
      then y in dom (f") by A1,FUNCT_1:55;
      hence thesis by A12,A34,A36,A35,FUNCT_4:16;
    end;
    suppose
A37:  x in dom g;
      then
A38:  y = g.x by A31,FUNCT_4:14;
      then
A39:  x = g".y by A2,A37,FUNCT_1:54;
A40:  rng g c= rng F by A18,XBOOLE_1:7;
A41:  y in rng g by A37,A38,FUNCT_1:12;
      then y in dom (g") by A2,FUNCT_1:55;
      hence thesis by A39,A41,A40,FUNCT_4:14;
    end;
  end;
  F is one-to-one by A1,A2,A3,A4,Th5;
  hence thesis by A14,A19,FUNCT_1:54;
end;

theorem Th7:
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
  being Point of TOP-REAL n st A is_an_arc_of p, q holds A \ {p} is non empty
proof
  let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
  TOP-REAL n;
  assume
  A is_an_arc_of p, q;
  then
A1: A \ { p, q } <> {} by JORDAN6:56;
  { p } c= { p, q } by ZFMISC_1:12;
  hence thesis by A1,XBOOLE_1:3,34;
end;

canceled;

theorem
  for s1, s3, s4, l being real number st s1 <= s3 & s1 < s4 & 0 <= l & l
  <= 1 holds s1 <= (1-l) * s3+l*s4
proof
  let s1, s3, s4, l be real number;
  assume that
A1: s1 <= s3 and
A2: s1 < s4 and
A3: 0 <= l and
A4: l <= 1;
  now
    per cases;
    suppose
      l=0;
      hence thesis by A1;
    end;
    suppose
      l=1;
      hence thesis by A2;
    end;
    suppose
A5:   not(l=0 or l=1);
      then l<1 by A4,XXREAL_0:1;
      then 1-l>0 by XREAL_1:52;
      then
A6:   (1-l)*s1<=(1-l)*s3 by A1,XREAL_1:66;
A7:   (1-l)*s1+l*s1=1 * s1;
      l*s1<l*s4 by A2,A3,A5,XREAL_1:70;
      hence thesis by A6,A7,XREAL_1:10;
    end;
  end;
  hence thesis;
end;

canceled 7;

theorem Th17:
  for A being Subset of I[01], a, b being real number st a < b & A
  = ].a,b.[ holds [.a,b.] c= the carrier of I[01]
proof
  let A be Subset of I[01], a, b be real number;
  assume
A1: a < b;
  assume
A2: A = ].a,b.[;
  then
A3: b <= 1 by A1,BORSUK_1:83,XXREAL_1:51;
  0 <= a by A1,A2,BORSUK_1:83,XXREAL_1:51;
  hence thesis by A3,BORSUK_1:83,XXREAL_1:34;
end;

theorem Th18:
  for A being Subset of I[01], a, b being real number st a < b & A
  = ].a,b.] holds [.a,b.] c= the carrier of I[01]
proof
  let A be Subset of I[01], a, b be real number;
  assume
A1: a < b;
A2: ].a,b.[ c= ]. a,b .] by XXREAL_1:21;
  assume
  A = ].a,b.];
  then
A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:83,XBOOLE_1:1;
  then
A4: b <= 1 by A1,XXREAL_1:51;
  0 <= a by A1,A3,XXREAL_1:51;
  hence thesis by A4,BORSUK_1:83,XXREAL_1:34;
end;

theorem Th19:
  for A being Subset of I[01], a, b being real number st a < b & A
  = [.a,b.[ holds [.a,b.] c= the carrier of I[01]
proof
  let A be Subset of I[01], a, b be real number;
  assume
A1: a < b;
A2: ].a,b.[ c= [. a,b .[ by XXREAL_1:22;
  assume
  A = [.a,b.[;
  then
A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:83,XBOOLE_1:1;
  then
A4: b <= 1 by A1,XXREAL_1:51;
  0 <= a by A1,A3,XXREAL_1:51;
  hence thesis by A4,BORSUK_1:83,XXREAL_1:34;
end;

theorem Th20:
  for a, b being real number st a <> b holds Cl ].a,b.] = [.a,b.]
proof
  let a, b be real number;
A1: Cl ].a,b.] c= [.a,b.] by MEASURE6:93,XXREAL_1:23;
A2: Cl ].a,b.[ c= Cl ].a,b.] by MEASURE6:98,XXREAL_1:21;
  assume
  a <> b;
  then [.a,b.] c= Cl ].a,b.] by A2,TOPREAL6:82;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th21:
  for a, b being real number st a <> b holds Cl [.a,b.[ = [.a,b.]
proof
  let a, b be real number;
A1: Cl [.a,b.[ c= [.a,b.] by MEASURE6:93,XXREAL_1:24;
A2: Cl ].a,b.[ c= Cl [.a,b.[ by MEASURE6:98,XXREAL_1:22;
  assume
  a <> b;
  then [.a,b.] c= Cl [.a,b.[ by A2,TOPREAL6:82;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem
  for A being Subset of I[01], a, b being real number st a < b & A = ].a
  ,b.[ holds Cl A = [.a,b.]
proof
  let A be Subset of I[01], a, b be real number;
  assume that
A1: a < b and
A2: A = ].a,b.[;
  reconsider A1 = ].a,b.[ as Subset of R^1 by TOPMETR:24;
A3: Cl ].a,b.[ = [.a,b.] by A1,TOPREAL6:82;
  Cl A = (Cl A1) /\ [#]I[01] by A2,PRE_TOPC:47
    .= [.a,b.] /\ [#]I[01] by A3,TOPREAL6:80
    .= [.a,b.] by A1,A2,Th17,XBOOLE_1:28;
  hence thesis;
end;

theorem Th23:
  for A being Subset of I[01], a, b being real number st a < b & A
  = ].a,b.] holds Cl A = [.a,b.]
proof
  let A be Subset of I[01], a, b be real number;
  assume that
A1: a < b and
A2: A = ].a,b.];
  reconsider A1 = ].a,b.] as Subset of R^1 by TOPMETR:24;
A3: Cl ].a,b.] = [.a,b.] by A1,Th20;
  Cl A = (Cl A1) /\ [#]I[01] by A2,PRE_TOPC:47
    .= [.a,b.] /\ [#]I[01] by A3,TOPREAL6:80
    .= [.a,b.] by A1,A2,Th18,XBOOLE_1:28;
  hence thesis;
end;

theorem Th24:
  for A being Subset of I[01], a, b being real number st a < b & A
  = [.a,b.[ holds Cl A = [.a,b.]
proof
  let A be Subset of I[01], a, b be real number;
  assume that
A1: a < b and
A2: A = [.a,b.[;
  reconsider A1 = [.a,b.[ as Subset of R^1 by TOPMETR:24;
A3: Cl [.a,b.[ = [.a,b.] by A1,Th21;
  Cl A = (Cl A1) /\ [#]I[01] by A2,PRE_TOPC:47
    .= [.a,b.] /\ [#]I[01] by A3,TOPREAL6:80
    .= [.a,b.] by A1,A2,Th19,XBOOLE_1:28;
  hence thesis;
end;

canceled 7;

theorem Th32:
  for A being Subset of I[01], a, b being real number st a <= b &
  A = [.a,b.] holds 0 <= a & b <= 1
proof
  let A be Subset of I[01], a, b be real number;
  assume that
A1: a <= b and
A2: A = [.a,b.];
A3: b in A by A1,A2,XXREAL_1:1;
  a in A by A1,A2,XXREAL_1:1;
  hence thesis by A3,BORSUK_1:86;
end;

theorem Th33:
  for A, B being Subset of I[01], a, b, c being real number st a <
  b & b < c & A = [.a,b.[ & B = ].b,c.] holds A, B are_separated
proof
  let A, B be Subset of I[01], a, b, c be real number;
  assume that
A1: a < b and
A2: b < c and
A3: A = [.a,b.[ and
A4: B = ].b,c.];
  Cl A = [.a,b.] by A1,A3,Th24;
  hence Cl A misses B by A4,XXREAL_1:90;
  Cl B = [.b,c.] by A2,A4,Th23;
  hence thesis by A3,XXREAL_1:95;
end;

canceled 9;

theorem
  for p1, p2 being Point of I[01] holds [. p1, p2 .] is Subset of I[01]
  by BORSUK_1:83,XXREAL_2:def 12;

theorem Th44:
  for a, b being Point of I[01] holds ]. a, b .[ is Subset of
  I[01]
proof
  let a, b be Point of I[01];
A1: [. a,b .] is Subset of I[01] by BORSUK_1:83,XXREAL_2:def 12;
  ]. a,b .[ c= [. a,b .] by XXREAL_1:25;
  hence thesis by A1,XBOOLE_1:1;
end;

begin :: Decompositions of Intervals

theorem
  for p being real number holds {p} is closed-interval Subset of REAL
proof
  let p be real number;
A1: {p} = [.p,p.] by XXREAL_1:17;
  p is Real by XREAL_0:def 1;
  hence thesis by A1,INTEGRA1:def 1;
end;

theorem Th46:
  for A being non empty connected Subset of I[01], a, b, c being
  Point of I[01] st a <= b & b <= c & a in A & c in A holds b in A
proof
  let A be non empty connected Subset of I[01], a, b, c be Point of I[01];
  assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A;
  per cases by A1,A2,A3,A4,XXREAL_0:1;
  suppose
    a = b or b = c;
    hence thesis by A3,A4;
  end;
  suppose
A5: a < b & b < c & a in A & c in A;
A6: ].b,1 .] c= [.b,1 .] by XXREAL_1:23;
A7: [.0,b.[ c= [.0,b.] by XXREAL_1:24;
A8: 0 <= a by BORSUK_1:86;
A9: c <= 1 by BORSUK_1:86;
    then
A10: b < 1 by A5,XXREAL_0:2;
    then
A11: b in [. 0,1 .] by A5,A8,XXREAL_1:1;
    1 in [.0,1 .] by XXREAL_1:1;
    then
A12: [. b,1 .] c= [.0,1 .] by A11,XXREAL_2:def 12;
    0 in [.0,1 .] by XXREAL_1:1;
    then [.0,b.] c= [. 0,1 .] by A11,XXREAL_2:def 12;
    then reconsider
    B = [.0,b.[, C = ].b,1 .] as non empty Subset of I[01] by A5,A8,A9,A7,A6
,A12,BORSUK_1:83,XBOOLE_1:1,XXREAL_1:2,3;
    assume
    not b in A;
    then A c= [. 0,1 .] \ {b} by BORSUK_1:83,ZFMISC_1:40;
    then
A13: A c= [. 0,b .[ \/ ]. b,1 .] by A5,A8,A10,XXREAL_1:201;
    now
      per cases by A5,A8,A10,A13,Th33,CONNSP_1:17;
      suppose
        A c= B;
        hence contradiction by A5,XXREAL_1:3;
      end;
      suppose
        A c= C;
        hence contradiction by A5,XXREAL_1:2;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th47:
  for A being non empty connected Subset of I[01], a, b being real
  number st a in A & b in A holds [.a,b.] c= A
proof
  let A be non empty connected Subset of I[01], a, b be real number;
  assume that
A1: a in A and
A2: b in A;
  let x be set;
  assume
  x in [.a,b.];
  then x in { y where y is Real : a <= y & y <= b } by RCOMP_1:def 1;
  then consider z being Real such that
A3: z = x and
A4: a <= z and
A5: z <= b;
A6: 0 <= z by A1,A4,BORSUK_1:86;
  b <= 1 by A2,BORSUK_1:86;
  then z <= 1 by A5,XXREAL_0:2;
  then reconsider z as Point of I[01] by A6,BORSUK_1:86;
  z in A by A1,A2,A4,A5,Th46;
  hence thesis by A3;
end;

theorem Th48:
  for a, b being real number, A being Subset of I[01] st A = [.a,b
  .] holds A is closed
proof
  let a, b be real number, A be Subset of I[01];
  assume
A1: A = [.a,b.];
  per cases;
  suppose
A2: a <= b;
    then
A3: b <= 1 by A1,Th32;
    0 <= a by A1,A2,Th32;
    then
A4: Closed-Interval-TSpace(a,b) is closed SubSpace of
    Closed-Interval-TSpace(0,1) by A2,A3,TREAL_1:6;
    then reconsider
    BA = the carrier of Closed-Interval-TSpace(a,b) as Subset of
    Closed-Interval-TSpace(0,1) by BORSUK_1:35;
    BA is closed by A4,BORSUK_1:def 14;
    hence thesis by A1,A2,TOPMETR:25,27;
  end;
  suppose
    a > b;
    then A = {}I[01] by A1,XXREAL_1:29;
    hence thesis;
  end;
end;

theorem Th49:
  for p1, p2 being Point of I[01] st p1 <= p2 holds [. p1, p2 .]
  is non empty compact connected Subset of I[01]
proof
  let p1, p2 be Point of I[01];
A1: p2 <= 1 by BORSUK_1:86;
  set S = [. p1, p2 .];
  reconsider S as Subset of I[01] by BORSUK_1:83,XXREAL_2:def 12;
  assume
A2: p1 <= p2;
  then
A3: Closed-Interval-TSpace(p1,p2) is connected by TREAL_1:23;
A4: S is closed by Th48;
  0 <= p1 by BORSUK_1:86;
  then I[01] | S = Closed-Interval-TSpace(p1,p2) by A2,A1,TOPMETR:31;
  hence thesis by A4,A3,COMPTS_1:17,CONNSP_1:def 3;
end;

theorem Th50:
  for X being Subset of I[01], X9 being Subset of REAL st X9 = X
  holds X9 is bounded_above bounded_below
proof
  let X be Subset of I[01], X9 be Subset of REAL;
  assume
A1: X9 = X;
  then for r being real number st r in X9 holds r <= 1 by BORSUK_1:86;
  hence X9 is bounded_above by SEQ_4:def 1;
  for r being real number st r in X9 holds 0 <= r by A1,BORSUK_1:86;
  hence thesis by SEQ_4:def 2;
end;

theorem Th51:
  for X being Subset of I[01], X9 being Subset of REAL, x being
  real number st x in X9 & X9 = X holds inf X9 <= x & x <= sup X9
proof
  let X be Subset of I[01], X9 be Subset of REAL, x be real number;
  assume that
A1: x in X9 and
A2: X9 = X;
  X9 is bounded_above bounded_below by A2,Th50;
  hence thesis by A1,SEQ_4:def 4,def 5;
end;

Lm1: I[01] is closed SubSpace of R^1 by TOPMETR:27,TREAL_1:5;

theorem Th52:
  for A being Subset of REAL, B being Subset of I[01] st A = B
  holds A is closed iff B is closed
proof
  reconsider Z = the carrier of I[01] as Subset of R^1 by BORSUK_1:35;
  let A be Subset of REAL, B be Subset of I[01];
  assume
A1: A = B;
  the carrier of I[01] c= the carrier of R^1 by BORSUK_1:35;
  then reconsider C = A as Subset of R^1 by A1,XBOOLE_1:1;
  hereby
    assume
    A is closed;
    then
A2: C is closed by TOPREAL6:79;
    C /\ [#] I[01] = B by A1,XBOOLE_1:28;
    hence B is closed by A2,PRE_TOPC:43;
  end;
  assume
A3: B is closed;
  Z is closed by Lm1,BORSUK_1:def 14;
  then B is closed iff C is closed by A1,TSEP_1:8;
  hence thesis by A3,TOPREAL6:79;
end;

theorem Th53:
  for C being closed-interval Subset of REAL holds inf C <= sup C
proof
  let C be closed-interval Subset of REAL;
  consider c being Element of C;
A1: c <= sup C by INTEGRA2:1;
  inf C <= c by INTEGRA2:1;
  hence thesis by A1,XXREAL_0:2;
end;

theorem Th54:
  for C being non empty compact connected Subset of I[01], C9
  being Subset of REAL st C = C9 & [. inf C9, sup C9 .] c= C9 holds [. inf C9,
  sup C9 .] = C9
proof
  let C be non empty compact connected Subset of I[01], C9 be Subset of REAL;
  assume that
A1: C = C9 and
A2: [. inf C9, sup C9 .] c= C9;
  assume
  [. inf C9, sup C9 .] <> C9;
  then not C9 c= [. inf C9, sup C9 .] by A2,XBOOLE_0:def 10;
  then consider c being set such that
A3: c in C9 and
A4: not c in [. inf C9, sup C9 .] by TARSKI:def 3;
  reconsider c as real number by A3;
A5: c <= sup C9 by A1,A3,Th51;
  inf C9 <= c by A1,A3,Th51;
  hence thesis by A4,A5,XXREAL_1:1;
end;

theorem Th55:
  for C being non empty compact connected Subset of I[01] holds C
  is closed-interval Subset of REAL
proof
  let C be non empty compact connected Subset of I[01];
  reconsider C9 = C as Subset of REAL by BORSUK_1:83,XBOOLE_1:1;
  C9 is bounded_below bounded_above by Th50;
  then
A1: lower_bound C9 <= upper_bound C9 by SEQ_4:24;
A2: C9 is closed by Th52;
  then
A3: sup C9 in C9 by Th50,RCOMP_1:30;
  inf C9 in C9 by A2,Th50,RCOMP_1:31;
  then [. inf C9, sup C9 .] = C9 by A3,Th47,Th54;
  hence thesis by A1,INTEGRA1:def 1;
end;

theorem Th56:
  for C being non empty compact connected Subset of I[01] ex p1,
  p2 being Point of I[01] st p1 <= p2 & C = [. p1, p2 .]
proof
  let C be non empty compact connected Subset of I[01];
  reconsider C9 = C as closed-interval Subset of REAL by Th55;
A1: C9 = [. inf C9, sup C9 .] by INTEGRA1:5;
A2: inf C9 <= sup C9 by Th53;
  then
A3: sup C9 in C by A1,XXREAL_1:1;
  inf C9 in C by A1,A2,XXREAL_1:1;
  then reconsider p1 = inf C9, p2 = sup C9 as Point of I[01] by A3;
  take p1, p2;
  thus p1 <= p2 by Th53;
  thus thesis by INTEGRA1:5;
end;

begin :: Decompositions of Simple Closed Curves

definition
  func I(01) -> strict non empty SubSpace of I[01] means
  :Def1:
  the carrier of
  it = ]. 0,1 .[;
  existence
  proof
    reconsider E = ]. 0,1 .[ as non empty Subset of I[01] by BORSUK_1:83
,XXREAL_1:25,33;
    take I[01] | E;
    thus thesis by PRE_TOPC:29;
  end;
  uniqueness by TSEP_1:5;
end;

theorem
  for A being Subset of I[01] st A = the carrier of I(01) holds I(01) =
  I[01] | A by PRE_TOPC:29,TSEP_1:5;

theorem Th58:
  the carrier of I(01) = (the carrier of I[01]) \ {0,1}
proof
A1: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128;
  the carrier of I(01) = ]. 0,1 .[ by Def1;
  hence thesis by A1,BORSUK_1:83,XBOOLE_1:88,XXREAL_1:86;
end;

theorem Th59:
  I(01) is open SubSpace of I[01] by Th58,JORDAN6:41,TSEP_1:def 1;

theorem Th60:
  for r being real number holds r in the carrier of I(01) iff 0 <
  r & r < 1
proof
  let r be real number;
  hereby
    assume
    r in the carrier of I(01);
    then r in ]. 0, 1 .[ by Def1;
    hence 0 < r & r < 1 by XXREAL_1:4;
  end;
  assume that
A1: 0 < r and
A2: r < 1;
  r in ]. 0, 1 .[ by A1,A2,XXREAL_1:4;
  hence thesis by Def1;
end;

theorem Th61:
  for a, b being Point of I[01] st a < b & b <> 1 holds ]. a, b .]
  is non empty Subset of I(01)
proof
  let a, b be Point of I[01];
  assume that
A1: a < b and
A2: b <> 1;
  b <= 1 by BORSUK_1:86;
  then
A3: b < 1 by A2,XXREAL_0:1;
  ]. a, b .] c= the carrier of I(01)
  proof
    let x be set;
    assume
    x in ]. a, b .];
    then x in { r where r is Real : a < r & r <= b } by RCOMP_1:def 9;
    then consider r being Real such that
A4: x = r and
A5: a < r and
A6: r <= b;
A7: 0 < r by A5,BORSUK_1:86;
    r < 1 by A3,A6,XXREAL_0:2;
    hence thesis by A4,A7,Th60;
  end;
  hence thesis by A1,XXREAL_1:2;
end;

theorem Th62:
  for a, b being Point of I[01] st a < b & a <> 0 holds [. a, b .[
  is non empty Subset of I(01)
proof
  let a, b be Point of I[01];
  assume that
A1: a < b and
A2: a <> 0;
A3: b <= 1 by BORSUK_1:86;
  [. a, b .[ c= the carrier of I(01)
  proof
    let x be set;
    assume
    x in [. a, b .[;
    then x in { r where r is Real : a <= r & r < b } by RCOMP_1:def 8;
    then consider r being Real such that
A4: x = r and
A5: a <= r and
A6: r < b;
A7: r < 1 by A3,A6,XXREAL_0:2;
    0 < r by A2,A5,BORSUK_1:86;
    hence thesis by A4,A7,Th60;
  end;
  hence thesis by A1,XXREAL_1:3;
end;

theorem
  for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square,
  (TOP-REAL 2) | D are_homeomorphic
proof
  let D be Simple_closed_curve;
  ex f being Function of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|D st f
  is being_homeomorphism by TOPREAL2:def 1;
  hence thesis by T_0TOPSP:def 1;
end;

theorem
  for n being Element of NAT, D being non empty Subset of TOP-REAL n, p1
, p2 being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I(01), (TOP-REAL
  n) | (D \ {p1,p2}) are_homeomorphic
proof
  reconsider K0 = the carrier of I(01) as Subset of I[01] by BORSUK_1:35;
  let n be Element of NAT, D be non empty Subset of TOP-REAL n, p1, p2 be
  Point of TOP-REAL n;
  assume
A1: D is_an_arc_of p1, p2;
  then consider f being Function of I[01], (TOP-REAL n)|D such that
A2: f is being_homeomorphism and
A3: f.0 = p1 and
A4: f.1 = p2 by TOPREAL1:def 2;
A5: rng f = [#] ((TOP-REAL n)|D) by A2,TOPS_2:def 5
    .= D by PRE_TOPC:29;
A6: dom f = the carrier of I[01] by FUNCT_2:def 1;
  then
A7: 0 in dom f by BORSUK_1:86;
A8: 1 in dom f by A6,BORSUK_1:86;
A9: f is continuous one-to-one by A2,TOPS_2:def 5;
  then
A10: f .: the carrier of I(01) = f .: (the carrier of I[01]) \ f .: {0,1} by
Th58,FUNCT_1:123
    .= D \ f .: {0,1} by A6,A5,RELAT_1:146
    .= D \ {p1,p2} by A3,A4,A7,A8,FUNCT_1:118;
A11: D \ {p1,p2} c= D by XBOOLE_1:36;
  then reconsider D0 = D \ {p1,p2} as Subset of (TOP-REAL n)|D by PRE_TOPC:29;
  reconsider D1 = D \ {p1,p2} as non empty Subset of TOP-REAL n by A1,
JORDAN6:56;
A12: (TOP-REAL n)|D1 = ((TOP-REAL n)|D)|D0 by GOBOARD9:4;
  set g = (f") | D1;
A13: D1 = the carrier of (TOP-REAL n)|D1 by PRE_TOPC:29;
  D1 c= the carrier of (TOP-REAL n)|D by A11,PRE_TOPC:29;
  then reconsider ff = g as Function of (TOP-REAL n)|D1, I[01] by A13,
FUNCT_2:38;
  f" is continuous by A2,TOPS_2:def 5;
  then
A14: ff is continuous by A12,TOPMETR:10;
  set fD = f | the carrier of I(01);
A15: I(01) = I[01] | K0 by PRE_TOPC:29,TSEP_1:5;
  then reconsider fD1 = fD as Function of I[01]|K0, (TOP-REAL n)|D by
FUNCT_2:38;
A16: dom fD = the carrier of I(01) by A6,BORSUK_1:35,RELAT_1:91;
  rng f = [#]((TOP-REAL n)|D) by A2,TOPS_2:def 5;
  then
A17: f" = (f qua Function)" by A9,TOPS_2:def 4;
A18: rng fD = f .: the carrier of I(01) by RELAT_1:148;
  then
A19: rng fD = the carrier of ((TOP-REAL n)|(D \ {p1,p2})) by A10,PRE_TOPC:29;
  then reconsider fD as Function of I(01), (TOP-REAL n)|(D \ {p1,p2}) by A16,
FUNCT_2:3;
A20: dom fD = [#]I(01) by A6,BORSUK_1:35,RELAT_1:91;
  f is one-to-one by A2,TOPS_2:def 5;
  then
A21: fD is one-to-one by FUNCT_1:84;
  then fD" = (fD qua Function)" by A19,TOPS_2:def 4;
  then
A22: fD" is continuous by A9,A10,A15,A14,A17,RFUNCT_2:40,TOPMETR:9;
  fD1 is continuous by A9,TOPMETR:10;
  then
A23: fD is continuous by A15,A12,TOPMETR:9;
  rng fD = [#]((TOP-REAL n)|(D \ {p1,p2})) by A10,A18,PRE_TOPC:29;
  then fD is being_homeomorphism by A20,A21,A23,A22,TOPS_2:def 5;
  hence thesis by T_0TOPSP:def 1;
end;

theorem Th65:
  for n being Element of NAT, D being Subset of TOP-REAL n, p1, p2
being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I[01], (TOP-REAL n) |
  D are_homeomorphic
proof
  let n be Element of NAT, D be Subset of TOP-REAL n, p1, p2 be Point of
  TOP-REAL n;
  assume
  D is_an_arc_of p1, p2;
  then
  ex f being Function of I[01], (TOP-REAL n)|D st f is being_homeomorphism
  & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2;
  hence thesis by T_0TOPSP:def 1;
end;

theorem
  for n being Element of NAT, p1, p2 being Point of TOP-REAL n st p1 <>
p2 holds I[01], (TOP-REAL n) | LSeg (p1, p2) are_homeomorphic by Th65,
TOPREAL1:15;

theorem Th67:
  for E being Subset of I(01) st (ex p1, p2 being Point of I[01]
  st p1 < p2 & E = [. p1,p2 .]) holds I[01], I(01)|E are_homeomorphic
proof
  let E be Subset of I(01);
  given p1, p2 being Point of I[01] such that
A1: p1 < p2 and
A2: E = [. p1,p2 .];
A3: p2 <= 1 by BORSUK_1:86;
  0 <= p1 by BORSUK_1:86;
  then reconsider
  S = Closed-Interval-TSpace(p1,p2) as SubSpace of I[01] by A1,A3,TOPMETR:27
,TREAL_1:6;
  reconsider T = I(01)|E as SubSpace of I[01] by TSEP_1:7;
  the carrier of S = E by A1,A2,TOPMETR:25;
  then
A4: S = T by PRE_TOPC:29,TSEP_1:5;
  set f = L[01]((#)(p1,p2), (p1,p2)(#));
  f is being_homeomorphism by A1,TREAL_1:20;
  hence thesis by A4,TOPMETR:27,T_0TOPSP:def 1;
end;

theorem Th68:
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
  < b ex E being non empty Subset of I[01], f being Function of I[01]|E, (
TOP-REAL n)|A st E = [. a, b .] & f is being_homeomorphism & f.a = p & f.b = q
proof
A1: 0 = (#)(0,1) by TREAL_1:def 1;
  let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
  TOP-REAL n, a, b be Point of I[01];
  assume that
A2: A is_an_arc_of p, q and
A3: a < b;
  reconsider E = [. a, b .] as non empty Subset of I[01] by A3,Th49;
A4: b <= 1 by BORSUK_1:86;
  0 <= a by BORSUK_1:86;
  then
A5: I[01]|E = Closed-Interval-TSpace(a,b) by A3,A4,TOPMETR:31;
  then reconsider
  e = P[01](a,b,(#)(0,1),(0,1)(#)) as Function of I[01]|E, I[01] by TOPMETR:27;
  take E;
A6: a = (#)(a,b) by A3,TREAL_1:def 1;
  reconsider B = A as non empty Subset of TOP-REAL n by A2,TOPREAL1:4;
  consider f being Function of I[01], (TOP-REAL n)|B such that
A7: f is being_homeomorphism and
A8: f.0 = p and
A9: f.1 = q by A2,TOPREAL1:def 2;
  set g = f * e;
  reconsider g as Function of I[01]|E, (TOP-REAL n)|A;
  take g;
  thus E = [. a, b .];
  e is being_homeomorphism by A3,A5,TOPMETR:27,TREAL_1:20;
  hence g is being_homeomorphism by A7,TOPS_2:71;
  a in E by A3,XXREAL_1:1;
  then a in the carrier of I[01]|E by PRE_TOPC:29;
  hence g.a = f.(e.a) by FUNCT_2:21
    .= p by A3,A8,A1,A6,TREAL_1:16;
A10: 1 = (0,1)(#) by TREAL_1:def 2;
A11: b = (a,b)(#) by A3,TREAL_1:def 2;
  b in E by A3,XXREAL_1:1;
  then b in the carrier of I[01]|E by PRE_TOPC:29;
  hence g.b = f.(e.b) by FUNCT_2:21
    .= q by A3,A9,A10,A11,TREAL_1:16;
end;

theorem Th69:
  for A being TopSpace, B being non empty TopSpace, f being
Function of A, B, C being TopSpace, X being Subset of A st f is continuous & C
  is SubSpace of B holds for h being Function of A|X, C st h = f|X holds h is
  continuous
proof
  let A be TopSpace, B be non empty TopSpace;
  let f be Function of A,B;
  let C be TopSpace, X be Subset of A;
  assume that
A1: f is continuous and
A2: C is SubSpace of B;
  the carrier of A|X = X by PRE_TOPC:29;
  then reconsider g = f|X as Function of A|X, B by FUNCT_2:38;
  let h be Function of A|X, C;
  assume
A3: h = f|X;
  g is continuous by A1,TOPMETR:10;
  hence thesis by A2,A3,PRE_TOPC:57;
end;

theorem Th70:
  for X being Subset of I[01], a, b being Point of I[01] st X = ].
  a, b .[ holds X is open
proof
  let X be Subset of I[01], a, b be Point of I[01];
A1: 0 <= a by BORSUK_1:86;
  1 in the carrier of I[01] by BORSUK_1:86;
  then reconsider B = [. b, 1 .] as Subset of I[01] by BORSUK_1:83
,XXREAL_2:def 12;
  0 in the carrier of I[01] by BORSUK_1:86;
  then reconsider A = [. 0, a .] as Subset of I[01] by BORSUK_1:83
,XXREAL_2:def 12;
A2: b <= 1 by BORSUK_1:86;
A3: B is closed by Th48;
A4: A is closed by Th48;
  assume
  X = ]. a, b .[;
  then X = (A \/ B)` by A1,A2,BORSUK_1:83,XXREAL_1:200;
  hence thesis by A4,A3;
end;

theorem Th71:
  for X being Subset of I(01), a, b being Point of I[01] st X = ].
  a, b .[ holds X is open
proof
  let X be Subset of I(01), a, b be Point of I[01];
  assume
A1: X = ]. a, b .[;
  then reconsider X9 = X as Subset of I[01] by Th44;
  X9 is open by A1,Th70;
  hence thesis by Th59,TSEP_1:17;
end;

theorem Th72:
  for X being Subset of I(01), a being Point of I[01] st X = ]. 0,
  a .] holds X is closed
proof
  let X be Subset of I(01), a be Point of I[01];
  assume
A1: X = ]. 0, a .];
  per cases;
  suppose
A2: 0 < a;
    [#] I(01) = ]. 0, 1 .[ by Def1;
    then
A3: [#] I(01) \ X = ]. a, 1 .[ by A1,A2,XXREAL_1:187;
    1 in the carrier of I[01] by BORSUK_1:86;
    then [#] I(01) \ X is open by A3,Th71;
    hence thesis by PRE_TOPC:def 6;
  end;
  suppose
    0 >= a;
    then X = {}I(01) by A1,XXREAL_1:26;
    hence thesis;
  end;
end;

theorem Th73:
  for X being Subset of I(01), a being Point of I[01] st X = [. a,
  1 .[ holds X is closed
proof
A1: 0 in the carrier of I[01] by BORSUK_1:86;
  let X be Subset of I(01), a be Point of I[01];
  assume
A2: X = [. a, 1 .[;
  per cases;
  suppose
A3: X is non empty;
A4: a <= 1 by BORSUK_1:86;
    a <> 1 by A2,A3,XXREAL_1:18;
    then
A5: a < 1 by A4,XXREAL_0:1;
    [#] I(01) = ]. 0, 1 .[ by Def1;
    then [#] I(01) \ X = ]. 0, a .[ by A2,A5,XXREAL_1:195;
    then [#] I(01) \ X is open by A1,Th71;
    hence thesis by PRE_TOPC:def 6;
  end;
  suppose
    X is empty;
    hence thesis;
  end;
end;

theorem Th74:
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & b <> 1 ex E being non empty Subset of I(01), f being Function of I(01)|E,
  (TOP-REAL n)|(A \ {p}) st E = ]. a, b .] & f is being_homeomorphism & f.b = q
proof
  let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
  TOP-REAL n, a, b be Point of I[01];
  assume that
A1: A is_an_arc_of p, q and
A2: a < b and
A3: b <> 1;
  reconsider B = A as non empty Subset of TOP-REAL n by A1,TOPREAL1:4;
  consider F being non empty Subset of I[01], s being Function of I[01]|F, (
  TOP-REAL n)|B such that
A4: F = [. a, b .] and
A5: s is being_homeomorphism and
A6: s.a = p and
A7: s.b = q by A1,A2,Th68;
A8: dom s = [#] (I[01]|F) by A5,TOPS_2:def 5
    .= F by PRE_TOPC:def 10;
  then
A9: a in dom s by A2,A4,XXREAL_1:1;
  reconsider E = ]. a, b .] as non empty Subset of I(01) by A2,A3,Th61;
  set X = E;
A10: I(01)|X is SubSpace of I[01] by TSEP_1:7;
  set sX = s|E;
A11: s is continuous one-to-one by A5,TOPS_2:def 5;
A12: s" is continuous by A5,TOPS_2:def 5;
A13: the carrier of (TOP-REAL n)|A = A by PRE_TOPC:29;
  then reconsider Ap = A \ {p} as Subset of (TOP-REAL n)|A by XBOOLE_1:36;
  the carrier of (TOP-REAL n)|(A \ {p}) = A \ {p} by PRE_TOPC:29;
  then the carrier of (TOP-REAL n)|(A \ {p}) c= the carrier of (TOP-REAL n)|A
  by A13,XBOOLE_1:36;
  then
A14: (TOP-REAL n)|(A \ {p}) is SubSpace of (TOP-REAL n)|A by TSEP_1:4;
A15: E c= F by A4,XXREAL_1:23;
  then reconsider X9 = E as Subset of I[01]|F by PRE_TOPC:29;
A16: I[01]|F|X9 is SubSpace of I[01] by TSEP_1:7;
  the carrier of I(01)|E = E by PRE_TOPC:29;
  then the carrier of I(01)|X c= the carrier of I[01]|F by A15,PRE_TOPC:29;
  then
A17: I(01)|X is SubSpace of I[01]|F by A10,TSEP_1:4;
A18: ((TOP-REAL n)|A)|Ap = (TOP-REAL n)|(A \ {p}) by PRE_TOPC:28,XBOOLE_1:36;
A19: dom sX = X by A4,A8,RELAT_1:91,XXREAL_1:23
    .= [#] (I(01)|X) by PRE_TOPC:def 10;
A20: rng s = [#] ((TOP-REAL n)|A) by A5,TOPS_2:def 5;
  then
A21: rng s = A by PRE_TOPC:def 10;
  X = F \ {a} by A2,A4,XXREAL_1:134;
  then
A22: s.:X = s.:F \ Im(s,a) by A11,FUNCT_1:123
    .= s.:F \ {s.a} by A9,FUNCT_1:117
    .= rng s \ {p} by A6,A8,RELAT_1:146
    .= [#] ((TOP-REAL n)|(A \ {p})) by A21,PRE_TOPC:def 10;
  then
A23: [#] ((TOP-REAL n)|(A \ {p})) = rng sX by RELAT_1:148;
  rng (s|E) = the carrier of (TOP-REAL n)|(A \ {p}) by A22,RELAT_1:148;
  then reconsider sX as Function of I(01)|E, (TOP-REAL n)|(A \ {p}) by A19,
FUNCT_2:3;
  b in X by A2,XXREAL_1:2;
  then
A24: sX.b = q by A7,FUNCT_1:72;
  the carrier of I(01)|X = X by PRE_TOPC:29;
  then I(01)|X = I[01]|F|X9 by A10,A16,PRE_TOPC:29,TSEP_1:5;
  then
A25: sX is continuous by A11,A14,Th69;
A26: sX is one-to-one by A11,FUNCT_1:84;
  then sX" = (sX qua Function)" by A23,TOPS_2:def 4
    .= (s qua Function)" | (s.:X) by A11,RFUNCT_2:40
    .= s" | [#] ((TOP-REAL n)|(A \ {p})) by A11,A20,A22,TOPS_2:def 4
    .= s" | Ap by PRE_TOPC:def 10;
  then sX" is continuous by A12,A17,A18,Th69;
  then sX is being_homeomorphism by A23,A19,A25,A26,TOPS_2:def 5;
  hence thesis by A24;
end;

theorem Th75:
  for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & a <> 0 ex E being non empty Subset of I(01), f being Function of I(01)|E,
  (TOP-REAL n)|(A \ {q}) st E = [. a, b .[ & f is being_homeomorphism & f.a = p
proof
  let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
  TOP-REAL n, a, b be Point of I[01];
  assume that
A1: A is_an_arc_of p, q and
A2: a < b and
A3: a <> 0;
  reconsider B = A as non empty Subset of TOP-REAL n by A1,TOPREAL1:4;
  consider F being non empty Subset of I[01], s being Function of I[01]|F, (
  TOP-REAL n)|B such that
A4: F = [. a, b .] and
A5: s is being_homeomorphism and
A6: s.a = p and
A7: s.b = q by A1,A2,Th68;
A8: dom s = [#] (I[01]|F) by A5,TOPS_2:def 5
    .= F by PRE_TOPC:def 10;
  then
A9: b in dom s by A2,A4,XXREAL_1:1;
  reconsider E = [. a, b .[ as non empty Subset of I(01) by A2,A3,Th62;
  set X = E;
A10: I(01)|X is SubSpace of I[01] by TSEP_1:7;
  set sX = s|E;
A11: s is continuous one-to-one by A5,TOPS_2:def 5;
A12: s" is continuous by A5,TOPS_2:def 5;
A13: the carrier of (TOP-REAL n)|A = A by PRE_TOPC:29;
  then reconsider Ap = A \ {q} as Subset of (TOP-REAL n)|A by XBOOLE_1:36;
  the carrier of (TOP-REAL n)|(A \ {q}) = A \ {q} by PRE_TOPC:29;
  then the carrier of (TOP-REAL n)|(A \ {q}) c= the carrier of (TOP-REAL n)|A
  by A13,XBOOLE_1:36;
  then
A14: (TOP-REAL n)|(A \ {q}) is SubSpace of (TOP-REAL n)|A by TSEP_1:4;
A15: E c= F by A4,XXREAL_1:24;
  then reconsider X9 = E as Subset of I[01]|F by PRE_TOPC:29;
A16: I[01]|F|X9 is SubSpace of I[01] by TSEP_1:7;
  the carrier of I(01)|E = E by PRE_TOPC:29;
  then the carrier of I(01)|X c= the carrier of I[01]|F by A15,PRE_TOPC:29;
  then
A17: I(01)|X is SubSpace of I[01]|F by A10,TSEP_1:4;
A18: ((TOP-REAL n)|A)|Ap = (TOP-REAL n)|(A \ {q}) by PRE_TOPC:28,XBOOLE_1:36;
A19: dom sX = X by A4,A8,RELAT_1:91,XXREAL_1:24
    .= [#] (I(01)|X) by PRE_TOPC:def 10;
A20: rng s = [#] ((TOP-REAL n)|A) by A5,TOPS_2:def 5;
  then
A21: rng s = A by PRE_TOPC:def 10;
  X = F \ {b} by A2,A4,XXREAL_1:135;
  then
A22: s.:X = s.:F \ Im(s,b) by A11,FUNCT_1:123
    .= s.:F \ {s.b} by A9,FUNCT_1:117
    .= rng s \ {q} by A7,A8,RELAT_1:146
    .= [#] ((TOP-REAL n)|(A \ {q})) by A21,PRE_TOPC:def 10;
  then
A23: [#] ((TOP-REAL n)|(A \ {q})) = rng sX by RELAT_1:148;
  rng (s|E) = the carrier of (TOP-REAL n)|(A \ {q}) by A22,RELAT_1:148;
  then reconsider sX as Function of I(01)|E, (TOP-REAL n)|(A \ {q}) by A19,
FUNCT_2:3;
  a in X by A2,XXREAL_1:3;
  then
A24: sX.a = p by A6,FUNCT_1:72;
  the carrier of I(01)|X = X by PRE_TOPC:29;
  then I(01)|X = I[01]|F|X9 by A10,A16,PRE_TOPC:29,TSEP_1:5;
  then
A25: sX is continuous by A11,A14,Th69;
A26: sX is one-to-one by A11,FUNCT_1:84;
  then sX" = (sX qua Function)" by A23,TOPS_2:def 4
    .= (s qua Function)" | (s.:X) by A11,RFUNCT_2:40
    .= s" | [#] ((TOP-REAL n)|(A \ {q})) by A11,A20,A22,TOPS_2:def 4
    .= s" | Ap by PRE_TOPC:def 10;
  then sX" is continuous by A12,A17,A18,Th69;
  then sX is being_homeomorphism by A23,A19,A25,A26,TOPS_2:def 5;
  hence thesis by A24;
end;

theorem Th76:
  for n being Element of NAT, A, B being Subset of TOP-REAL n, p,
q being Point of TOP-REAL n st A is_an_arc_of p, q & B is_an_arc_of q, p & A /\
  B = { p, q } & p <> q holds I(01), (TOP-REAL n) | ((A \ {p}) \/ (B \ {p}))
  are_homeomorphic
proof
  reconsider a = 0, b = 1/2, c = 1 as Point of I[01] by BORSUK_1:86;
  let n be Element of NAT, A, B be Subset of TOP-REAL n, p, q be Point of
  TOP-REAL n;
  assume that
A1: A is_an_arc_of p, q and
A2: B is_an_arc_of q, p and
A3: A /\ B = { p, q } and
A4: p <> q;
  consider E2 being non empty Subset of I(01), ty being Function of I(01)|E2,
  (TOP-REAL n)|(B \ {p}) such that
A5: E2 = [. b, c .[ and
A6: ty is being_homeomorphism and
A7: ty.b = q by A2,Th75;
  consider E1 being non empty Subset of I(01), sx being Function of I(01)|E1,
  (TOP-REAL n)|(A \ {p}) such that
A8: E1 = ]. a, b .] and
A9: sx is being_homeomorphism and
A10: sx.b = q by A1,Th74;
  set T1 = I(01)|E1, T2 = I(01)|E2, T = I(01), S = (TOP-REAL n) | ((A \ {p})
  \/ (B \ {p})), U1 = (TOP-REAL n) | (A \ {p}), U2 = (TOP-REAL n)|(B \ {p});
A11: A \ {p} is non empty by A1,Th7;
  then reconsider S as non empty SubSpace of TOP-REAL n;
  B \ {p} is non empty by A2,Th7,JORDAN5B:14;
  then reconsider U1, U2 as non empty SubSpace of TOP-REAL n by A11;
A12: the carrier of S = (A \ {p}) \/ (B \ {p}) by PRE_TOPC:29;
  the carrier of U2 = B \ {p} by PRE_TOPC:29;
  then
A13: the carrier of U2 c= the carrier of S by A12,XBOOLE_1:7;
  then reconsider ty9 = ty as Function of T2, S by FUNCT_2:9;
A14: U2 is SubSpace of S by A13,TSEP_1:4;
  ty is continuous by A6,TOPS_2:def 5;
  then
A15: ty9 is continuous by A14,PRE_TOPC:56;
  reconsider F1 = [#] T1, F2 = [#] T2 as non empty Subset of T by
PRE_TOPC:def 10;
A16: F2 = [. 1/2, 1 .[ by A5,PRE_TOPC:def 10;
  the carrier of U1 = A \ {p} by PRE_TOPC:29;
  then
A17: the carrier of U1 c= the carrier of S by A12,XBOOLE_1:7;
  then reconsider sx9 = sx as Function of T1, S by FUNCT_2:9;
A18: U1 is SubSpace of S by A17,TSEP_1:4;
A19: rng ty = [#] ((TOP-REAL n)|(B \ {p})) by A6,TOPS_2:def 5;
  then
A20: rng ty = B \ {p} by PRE_TOPC:def 10;
A21: rng sx = [#] ((TOP-REAL n)|(A \ {p})) by A9,TOPS_2:def 5;
  then
A22: rng sx = A \ {p} by PRE_TOPC:def 10;
  then
A23: rng sx9 /\ rng ty9 = ((A \ {p}) /\ B) \ {p} by A20,XBOOLE_1:49
    .= ((A /\ B) \ {p}) \ {p} by XBOOLE_1:49
    .= (A /\ B) \ ({p} \/ {p}) by XBOOLE_1:41
    .= { sx9.b } by A3,A4,A10,ZFMISC_1:23;
  sx is continuous by A9,TOPS_2:def 5;
  then
A24: sx9 is continuous by A18,PRE_TOPC:56;
A25: 1/2 in the carrier of I[01] by BORSUK_1:86;
  then
A26: F2 is closed by A16,Th73;
A27: F1 = ]. 0, 1/2 .] by A8,PRE_TOPC:def 10;
  then
A28: ([#] T1) \/ ([#] T2) = ]. 0, 1 .[ by A16,XXREAL_1:172
    .= [#] T by Def1;
A29: ([#] T1) /\ ([#] T2) = { 1/2 } by A27,A16,XXREAL_1:138;
A30: for d be set st d in ([#] T1) /\ ([#] T2) holds sx.d = ty.d
  proof
    let d be set;
    assume
    d in ([#] T1) /\ ([#] T2);
    then d = b by A29,TARSKI:def 1;
    hence thesis by A10,A7;
  end;
  F1 is closed by A25,A27,Th72;
  then consider F being Function of T,S such that
A31: F = sx9+*ty and
A32: F is continuous by A24,A15,A26,A28,A30,JGRAPH_2:9;
A33: [#] U2 = B \ {p} by PRE_TOPC:def 10;
  then
A34: [#] U2 c= (A \ {p}) \/ (B \ {p}) by XBOOLE_1:7;
  the carrier of T2 c= the carrier of T by BORSUK_1:35;
  then reconsider g = ty" as Function of U2, T by FUNCT_2:9;
  the carrier of T1 c= the carrier of T by BORSUK_1:35;
  then reconsider f = sx" as Function of U1, T by FUNCT_2:9;
A35: dom ty9 = [#] T2 by FUNCT_2:def 1;
A36: [#] U1 = A \ {p} by PRE_TOPC:def 10;
  then [#] U1 c= (A \ {p}) \/ (B \ {p}) by XBOOLE_1:7;
  then reconsider V1 = [#] U1, V2 = [#] U2 as Subset of S by A34,PRE_TOPC:29;
A37: dom F = [#] I(01) by FUNCT_2:def 1;
A38: V2 is closed
  proof
    reconsider B9 = B as Subset of TOP-REAL n;
A39: B9 is closed by A2,COMPTS_1:16,JORDAN5A:1;
A40: not p in {q} by A4,TARSKI:def 1;
    q in B by A2,TOPREAL1:4;
    then
A41: {q} c= B by ZFMISC_1:37;
A42: B /\ (A \ {p}) = B /\ A \ {p} by XBOOLE_1:49
      .= {q} by A3,A4,ZFMISC_1:23;
    B9 /\ [#] S = B9 /\ ((A \ {p}) \/ (B \ {p})) by PRE_TOPC:def 10
      .= (B /\ (A \ {p})) \/ (B /\ (B \ {p})) by XBOOLE_1:23
      .= (B /\ (A \ {p})) \/ (B \ {p}) by XBOOLE_1:28,36
      .= B \ {p} by A40,A41,A42,XBOOLE_1:12,ZFMISC_1:40
      .= V2 by PRE_TOPC:def 10;
    hence thesis by A39,PRE_TOPC:43;
  end;
A43: V1 is closed
  proof
    reconsider A9 = A as Subset of TOP-REAL n;
A44: A9 is closed by A1,COMPTS_1:16,JORDAN5A:1;
A45: not p in {q} by A4,TARSKI:def 1;
    q in A by A1,TOPREAL1:4;
    then
A46: {q} c= A by ZFMISC_1:37;
A47: A /\ (B \ {p}) = A /\ B \ {p} by XBOOLE_1:49
      .= {q} by A3,A4,ZFMISC_1:23;
    A9 /\ [#] S = A9 /\ ((A \ {p}) \/ (B \ {p})) by PRE_TOPC:def 10
      .= (A /\ (A \ {p})) \/ (A /\ (B \ {p})) by XBOOLE_1:23
      .= (A \ {p}) \/ (A /\ (B \ {p})) by XBOOLE_1:28,36
      .= A \ {p} by A45,A46,A47,XBOOLE_1:12,ZFMISC_1:40
      .= V1 by PRE_TOPC:def 10;
    hence thesis by A44,PRE_TOPC:43;
  end;
  ty" is continuous by A6,TOPS_2:def 5;
  then
A48: g is continuous by PRE_TOPC:56;
  sx" is continuous by A9,TOPS_2:def 5;
  then
A49: f is continuous by PRE_TOPC:56;
A50: ty9 is one-to-one by A6,TOPS_2:def 5;
  then
A51: ty" = (ty qua Function)" by A19,TOPS_2:def 4;
A52: dom sx9 = [#] T1 by FUNCT_2:def 1;
  then
A53: dom sx9 /\ dom ty9 = { b } by A27,A16,A35,XXREAL_1:138;
  sx9 tolerates ty9
  proof
    let t be set;
    assume
    t in dom sx9 /\ dom ty9;
    then t = b by A53,TARSKI:def 1;
    hence thesis by A10,A7;
  end;
  then
A54: rng F = rng sx9 \/ rng ty9 by A31,FRECHET:39
    .= [#] S by A22,A20,PRE_TOPC:def 10;
A55: sx9 is one-to-one by A9,TOPS_2:def 5;
  then
A56: sx" = (sx qua Function)" by A21,TOPS_2:def 4;
A57: for r being set st r in ([#] U1) /\ ([#] U2) holds f.r = g.r
  proof
    let r be set;
    b in E2 by A5,XXREAL_1:3;
    then
A58: b in dom ty by A35,PRE_TOPC:def 10;
    b in E1 by A8,XXREAL_1:2;
    then b in dom sx by A52,PRE_TOPC:def 10;
    then
A59: f.q = b by A10,A55,A56,FUNCT_1:56;
    assume
    r in ([#] U1) /\ ([#] U2);
    then r = q by A10,A21,A19,A23,TARSKI:def 1;
    hence thesis by A7,A50,A51,A58,A59,FUNCT_1:56;
  end;
  ([#] U1) \/ ([#] U2) = [#] S by A36,A33,PRE_TOPC:def 10;
  then
A60: ex h being Function of S,T st h = f+*g & h is continuous by A18,A14,A43
,A38,A49,A48,A57,JGRAPH_2:9;
A61: F is one-to-one by A31,A55,A50,A53,A23,Th5;
  then F" = (F qua Function)" by A54,TOPS_2:def 4;
  then F" = sx" +* ty" by A10,A7,A31,A55,A50,A53,A23,A56,A51,Th6;
  then F is being_homeomorphism by A32,A37,A61,A54,A60,TOPS_2:def 5;
  hence thesis by T_0TOPSP:def 1;
end;

theorem Th77:
  for D being Simple_closed_curve, p being Point of TOP-REAL 2 st
  p in D holds (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
proof
  let D be Simple_closed_curve, p be Point of TOP-REAL 2;
  consider q being Point of TOP-REAL 2 such that
A1: q in D and
A2: p <> q by Th4;
  not q in {p} by A2,TARSKI:def 1;
  then reconsider R2p = D \ {p} as non empty Subset of TOP-REAL 2 by A1,
XBOOLE_0:def 5;
  assume
  p in D;
  then consider P1, P2 being non empty Subset of TOP-REAL 2 such that
A3: P1 is_an_arc_of p,q and
A4: P2 is_an_arc_of p,q and
A5: D = P1 \/ P2 and
A6: P1 /\ P2 = {p,q} by A1,A2,TOPREAL2:5;
A7: P2 is_an_arc_of q, p by A4,JORDAN5B:14;
  D \ {p} = (P1 \ {p}) \/ (P2 \ {p}) by A5,XBOOLE_1:42;
  then (TOP-REAL 2) | R2p, I(01) are_homeomorphic by A2,A3,A6,A7,Th76;
  hence thesis;
end;

theorem
  for D being Simple_closed_curve, p, q being Point of TOP-REAL 2 st p
  in D & q in D holds (TOP-REAL 2) | (D \ {p}), (TOP-REAL 2) | (D \ {q})
  are_homeomorphic
proof
  let D be Simple_closed_curve, p, q be Point of TOP-REAL 2;
  assume that
A1: p in D and
A2: q in D;
  per cases;
  suppose
    p = q;
    hence thesis;
  end;
  suppose
    p <> q;
    then reconsider
    Dp = D \ {p}, Dq = D \ {q} as non empty Subset of TOP-REAL 2 by A1,A2,
ZFMISC_1:64;
A3: (TOP-REAL 2) | Dq, I(01) are_homeomorphic by A2,Th77;
    (TOP-REAL 2) | Dp, I(01) are_homeomorphic by A1,Th77;
    hence thesis by A3,BORSUK_3:3;
  end;
end;

theorem Th79:
  for n being Element of NAT, C being non empty Subset of TOP-REAL
n, E being Subset of I(01) st (ex p1, p2 being Point of I[01] st p1 < p2 & E =
  [. p1,p2 .]) & I(01)|E, (TOP-REAL n)|C are_homeomorphic holds ex s1, s2 being
  Point of TOP-REAL n st C is_an_arc_of s1,s2
proof
  let n be Element of NAT, C be non empty Subset of TOP-REAL n, E be Subset of
  I(01);
  given p1, p2 being Point of I[01] such that
A1: p1 < p2 and
A2: E = [. p1,p2 .];
A3: I[01], I(01)|E are_homeomorphic by A1,A2,Th67;
  assume
A4: I(01)|E, (TOP-REAL n)|C are_homeomorphic;
  E is non empty by A1,A2,Th49;
  then I[01], (TOP-REAL n)|C are_homeomorphic by A4,A3,BORSUK_3:3;
  then consider g being Function of I[01], (TOP-REAL n)|C such that
A5: g is being_homeomorphism by T_0TOPSP:def 1;
  set s1 = g.0, s2 = g.1;
  0 in the carrier of I[01] by BORSUK_1:86;
  then
A6: g.0 in the carrier of (TOP-REAL n)|C by FUNCT_2:7;
  1 in the carrier of I[01] by BORSUK_1:86;
  then
A7: g.1 in the carrier of (TOP-REAL n)|C by FUNCT_2:7;
  the carrier of (TOP-REAL n)|C c= the carrier of TOP-REAL n by BORSUK_1:35;
  then reconsider s1, s2 as Point of TOP-REAL n by A6,A7;
  C is_an_arc_of s1, s2 by A5,TOPREAL1:def 2;
  hence thesis;
end;

theorem Th80:
  for Dp being non empty Subset of TOP-REAL 2, f being Function of
  (TOP-REAL 2) | Dp, I(01), C being non empty Subset of TOP-REAL 2 st f is
being_homeomorphism & C c= Dp & (ex p1, p2 being Point of I[01] st p1 < p2 & f
.:C = [. p1,p2 .]) holds ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of
  s1,s2
proof
  let Dp be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2) | Dp
  , I(01), C be non empty Subset of TOP-REAL 2;
  assume that
A1: f is being_homeomorphism and
A2: C c= Dp;
  reconsider C9 = C as Subset of (TOP-REAL 2) | Dp by A2,PRE_TOPC:29;
A3: the carrier of (TOP-REAL 2)|Dp = Dp by PRE_TOPC:29;
  dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
  then C c= dom f by A2,PRE_TOPC:29;
  then
A4: C c= f"(f.:C) by FUNCT_1:146;
  given p1, p2 being Point of I[01] such that
A5: p1 < p2 and
A6: f.:C = [. p1,p2 .];
  reconsider E = [. p1,p2 .] as Subset of I(01) by A6;
A7: rng f = [#] I(01) by A1,TOPS_2:def 5;
A8: f is continuous one-to-one by A1,TOPS_2:def 5;
  then f"(f.:C) c= C by FUNCT_1:152;
  then f"(f.:C) = C by A4,XBOOLE_0:def 10;
  then
A9: f".:E = C by A6,A8,A7,TOPS_2:68;
  the carrier of (TOP-REAL 2)|C = C by PRE_TOPC:29;
  then
A10: (TOP-REAL 2)|C is SubSpace of (TOP-REAL 2) | Dp by A2,A3,TOPMETR:4;
  set g = f"| E;
  the carrier of (I(01)|E) = E by PRE_TOPC:29;
  then
A11: g is Function of the carrier of I(01)|E, the carrier of (TOP-REAL 2)|Dp
  by FUNCT_2:38;
A12: rng g = f".:E by RELAT_1:148
    .= [#] ((TOP-REAL 2)|C) by A9,PRE_TOPC:29;
  then reconsider g as Function of I(01)|E, (TOP-REAL 2)|C by A11,FUNCT_2:8;
  f" is being_homeomorphism by A1,TOPS_2:70;
  then
A13: f" is one-to-one by TOPS_2:def 5;
  then
A14: g is one-to-one by FUNCT_1:84;
  then
A15: g" = (g qua Function)" by A12,TOPS_2:def 4
    .= ((f" qua Function)")|((f").:E) by A13,RFUNCT_2:40
    .= ((f qua Function)"")|((f").:E) by A8,A7,TOPS_2:def 4
    .= f|C by A8,A9,FUNCT_1:65;
  then reconsider t = f|C as Function of (TOP-REAL 2) | C, I(01)|E;
  dom (f") = the carrier of I(01) by FUNCT_2:def 1;
  then dom g = E by RELAT_1:91
    .= the carrier of (I(01)|E) by PRE_TOPC:29;
  then
A16: dom g = [#] (I(01)|E);
  f" is continuous by A1,TOPS_2:def 5;
  then
A17: g is continuous by A10,Th69;
  ((TOP-REAL 2) | Dp)|C9 = (TOP-REAL 2) | C by A2,PRE_TOPC:28;
  then t is continuous by A8,Th69;
  then g is being_homeomorphism by A12,A16,A14,A17,A15,TOPS_2:def 5;
  then I(01)|E, (TOP-REAL 2)|C are_homeomorphic by T_0TOPSP:def 1;
  hence thesis by A5,Th79;
end;

theorem
  for D being Simple_closed_curve, C being non empty compact connected
  Subset of TOP-REAL 2 st C c= D holds C = D or (ex p1, p2 being Point of
TOP-REAL 2 st C is_an_arc_of p1,p2) or ex p being Point of TOP-REAL 2 st C = {p
  }
proof
  let D be Simple_closed_curve, C be non empty compact connected Subset of
  TOP-REAL 2;
  assume
A1: C c= D;
  assume
A2: C <> D;
  per cases;
  suppose
    C is trivial;
    hence thesis by Th2;
  end;
  suppose
A3: C is non trivial;
    C c< D by A1,A2,XBOOLE_0:def 8;
    then consider p being Point of TOP-REAL 2 such that
A4: p in D and
A5: C c= D \ {p} by Th1;
    consider d1,d2 being Point of TOP-REAL 2 such that
A6: d1 in C and
A7: d2 in C and
A8: d1 <> d2 by A3,REALSET1:15;
    reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2 by A6,A5;
    (TOP-REAL 2) | Dp, I(01) are_homeomorphic by A4,Th77;
    then consider f being Function of (TOP-REAL 2) | Dp, I(01) such that
A9: f is being_homeomorphism by T_0TOPSP:def 1;
    reconsider C9 = C as Subset of (TOP-REAL 2) | Dp by A5,PRE_TOPC:29;
    C c= [#] ((TOP-REAL 2) | Dp) by A5,PRE_TOPC:29;
    then
A10: C9 is compact by COMPTS_1:11;
    set fC = f.:C9;
A11: C9 is connected by CONNSP_1:24;
A12: rng f = [#] I(01) by A9,TOPS_2:def 5;
    f is continuous by A9,TOPS_2:def 5;
    then reconsider fC as compact connected Subset of I(01) by A10,A11,A12,
COMPTS_1:24,TOPS_2:75;
    reconsider fC9 = fC as Subset of I[01] by PRE_TOPC:39;
A13: fC9 c= [#] I(01);
A14: for P being Subset of I(01) st P=fC9 holds P is compact;
    d1 in D \ {p} by A6,A5;
    then d1 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:29;
    then
A15: d1 in dom f by FUNCT_2:def 1;
A16: f is one-to-one by A9,TOPS_2:def 5;
    d2 in D \ {p} by A7,A5;
    then d2 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:29;
    then
A17: d2 in dom f by FUNCT_2:def 1;
A18: f.d2 in f.:C9 by A7,FUNCT_2:43;
    then reconsider
    fC9 as non empty compact connected Subset of I[01] by A13,A14,COMPTS_1:11
,CONNSP_1:24;
    consider p1, p2 being Point of I[01] such that
A19: p1 <= p2 and
A20: fC9 = [. p1,p2 .] by Th56;
A21: f.d1 in f.:C9 by A6,FUNCT_2:43;
    p1 <> p2
    proof
      assume
      p1 = p2;
      then
A22:  fC9 = {p1} by A20,XXREAL_1:17;
      then
A23:  f.d2 = p1 by A18,TARSKI:def 1;
      f.d1 = p1 by A21,A22,TARSKI:def 1;
      hence thesis by A8,A15,A17,A16,A23,FUNCT_1:def 8;
    end;
    then p1 < p2 by A19,XXREAL_0:1;
    hence thesis by A5,A9,A20,Th80;
  end;
end;

begin :: Addenda

:: from BORSUK_6, 2007.04.08, A,T.

definition
  let T be 1-sorted;
  attr T is real-membered means :: BORSUK_6:def 1
  :Def2:
  the carrier of T is real-membered;
end;

registration
  cluster I[01] -> real-membered;
  coherence
  proof
    thus the carrier of I[01] is real-membered by BORSUK_1:83;
  end;
end;

:: from RCOMP_3, 2007.04.08, A,T.

registration
  cluster real-membered 1-sorted;
  existence
  proof
    take I[01];
    thus thesis;
  end;
end;

registration
  let S be real-membered 1-sorted;
  cluster the carrier of S -> real-membered;
  coherence by Def2;
end;

theorem Th82:
  for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex D being closed-interval Subset of REAL st C c= D & D c= ].0,1.[ & inf
  C = inf D & sup C = sup D
proof
  let C be non empty compact Subset of I[01];
  assume
A1: C c= ].0,1.[;
  reconsider C9 = C as Subset of REAL by BORSUK_1:83,XBOOLE_1:1;
  reconsider D = [. inf C9, sup C9 .] as Subset of REAL;
A2: C9 is bounded_below bounded_above by Th50;
  then
A3: lower_bound C9 <= upper_bound C9 by SEQ_4:24;
A4: C c= D
  proof
    let x be set;
    assume
A5: x in C;
    then x in the carrier of I[01];
    then reconsider x9 = x as Real by BORSUK_1:83;
A6: x9 <= sup C9 by A5,Th51;
    inf C9 <= x9 by A5,Th51;
    hence thesis by A6,XXREAL_1:1;
  end;
A7: C9 is closed by Th52;
  then
A8: inf C9 in C9 by Th50,RCOMP_1:31;
A9: sup C9 in C9 by A7,Th50,RCOMP_1:30;
  then
A10: D is non empty compact connected Subset of I[01] by A2,A8,Th49,SEQ_4:24;
  then
A11: D is closed-interval Subset of REAL by Th55;
  then
A12: D = [. inf D, sup D .] by INTEGRA1:5;
  then
A13: sup C9 = sup D by A3,XXREAL_1:66;
A14: not 1 in D
  proof
    assume
    1 in D;
    then sup D >= 1 by A11,INTEGRA2:1;
    hence thesis by A1,A9,A13,XXREAL_1:4;
  end;
A15: inf C9 = inf D by A3,A12,XXREAL_1:66;
A16: not 0 in D
  proof
    assume
    0 in D;
    then inf D <= 0 by A11,INTEGRA2:1;
    hence thesis by A1,A8,A15,XXREAL_1:4;
  end;
A17: D c= ].0,1.[
  proof
    let x be set;
    assume
    x in D;
    hence thesis by A10,A16,A14,BORSUK_1:83,XXREAL_1:5;
  end;
  reconsider D as closed-interval Subset of REAL by A3,INTEGRA1:def 1;
  take D;
  thus thesis by A4,A3,A12,A17,XXREAL_1:66;
  consider x being Element of C9;
end;

theorem Th83:
  for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex p1, p2 being Point of I[01] st p1 <= p2 & C c= [. p1, p2 .] & [.p1,p2
  .] c= ]. 0, 1 .[
proof
  let C be non empty compact Subset of I[01];
  assume
  C c= ].0,1.[;
  then consider D being closed-interval Subset of REAL such that
A1: C c= D and
A2: D c= ].0,1.[ and
  inf C = inf D and
  sup C = sup D by Th82;
  consider p1,p2 being Real such that
A3: p1 <= p2 and
A4: D = [.p1,p2.] by INTEGRA1:def 1;
  p1 in D by A3,A4,XXREAL_1:1;
  then
A5: p1 in ].0,1.[ by A2;
  p2 in D by A3,A4,XXREAL_1:1;
  then
A6: p2 in ].0,1.[ by A2;
  ].0,1.[ c= [.0,1.] by XXREAL_1:25;
  then reconsider p1, p2 as Point of I[01] by A5,A6,BORSUK_1:83;
  take p1, p2;
  thus p1 <= p2 by A3;
  thus thesis by A1,A2,A4;
end;

theorem
  for D being Simple_closed_curve, C being closed Subset of TOP-REAL 2
st C c< D ex p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2 st B
  is_an_arc_of p1,p2 & C c= B & B c= D
proof
  let D be Simple_closed_curve, C be closed Subset of TOP-REAL 2;
  assume
A1: C c< D;
  then
A2: C c= D by XBOOLE_0:def 8;
A3: for C being compact Subset of TOP-REAL 2 st C is non trivial & C c< D ex
p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2 st B is_an_arc_of
  p1,p2 & C c= B & B c= D
  proof
    let C be compact Subset of TOP-REAL 2;
    assume
    C is non trivial;
    then consider d1,d2 being Point of TOP-REAL 2 such that
A4: d1 in C and
A5: d2 in C and
A6: d1 <> d2 by REALSET1:15;
    assume
    C c< D;
    then consider p being Point of TOP-REAL 2 such that
A7: p in D and
A8: C c= D \ {p} by A4,Th1;
    reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2 by A4,A8;
    (TOP-REAL 2) | Dp, I(01) are_homeomorphic by A7,Th77;
    then consider f being Function of (TOP-REAL 2) | Dp, I(01) such that
A9: f is being_homeomorphism by T_0TOPSP:def 1;
    d2 in D \ {p} by A5,A8;
    then d2 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:29;
    then
A10: d2 in dom f by FUNCT_2:def 1;
    d1 in D \ {p} by A4,A8;
    then d1 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:29;
    then
A11: d1 in dom f by FUNCT_2:def 1;
A12: f is one-to-one by A9,TOPS_2:def 5;
    C c= the carrier of (TOP-REAL 2) | Dp by A8,PRE_TOPC:29;
    then
A13: C c= dom f by FUNCT_2:def 1;
    dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
    then
A14: dom f c= the carrier of TOP-REAL 2 by BORSUK_1:35;
    dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
    then
A15: dom f = Dp by PRE_TOPC:29;
    reconsider C9 = C as Subset of (TOP-REAL 2) | Dp by A8,PRE_TOPC:29;
    C c= [#] ((TOP-REAL 2) | Dp) by A8,PRE_TOPC:29;
    then
A16: C9 is compact by COMPTS_1:11;
    set fC = f.:C9;
A17: rng f = [#] I(01) by A9,TOPS_2:def 5;
    f is continuous by A9,TOPS_2:def 5;
    then reconsider fC as compact Subset of I(01) by A16,A17,COMPTS_1:24;
    reconsider fC9 = fC as Subset of I[01] by PRE_TOPC:39;
A18: fC9 c= [#] I(01);
A19: for P being Subset of I(01) st P=fC9 holds P is compact;
    fC9 c= the carrier of I(01);
    then
A20: fC9 c= ].0,1.[ by Def1;
A21: f.d2 in f.:C9 by A5,FUNCT_2:43;
    then reconsider fC9 as non empty compact Subset of I[01] by A18,A19,
COMPTS_1:11;
    consider p1, p2 being Point of I[01] such that
A22: p1 <= p2 and
A23: fC9 c= [. p1,p2 .] and
A24: [.p1,p2.] c= ].0,1.[ by A20,Th83;
    reconsider E = [.p1,p2.] as non empty compact connected Subset of I[01] by
A22,Th49;
A25: f " E c= dom f by RELAT_1:167;
A26: f.d1 in f.:C9 by A4,FUNCT_2:43;
    p1 <> p2
    proof
      assume
      p1 = p2;
      then
A27:  fC9 c= {p1} by A23,XXREAL_1:17;
      then
A28:  f.d2 = p1 by A21,TARSKI:def 1;
      f.d1 = p1 by A26,A27,TARSKI:def 1;
      hence thesis by A6,A11,A10,A12,A28,FUNCT_1:def 8;
    end;
    then
A29: p1 < p2 by A22,XXREAL_0:1;
    E c= rng f by A17,A24,Def1;
    then reconsider B = f " E as non empty Subset of TOP-REAL 2 by A25,A14,
RELAT_1:174,XBOOLE_1:1;
    rng f = ].0,1.[ by A17,Def1;
    then f.: (f"E) = E by A24,FUNCT_1:147;
    then consider s1, s2 being Point of TOP-REAL 2 such that
A30: B is_an_arc_of s1,s2 by A9,A29,A15,Th80,RELAT_1:167;
    take s1, s2, B;
    thus B is_an_arc_of s1,s2 by A30;
    Dp c= D by XBOOLE_1:36;
    hence thesis by A23,A25,A15,A13,FUNCT_1:163,XBOOLE_1:1;
  end;
  D is Bounded by JORDAN2C:73;
  then
A31: C is compact by A2,JORDAN2C:16,TOPREAL6:88;
  per cases;
  suppose
A32: C is trivial;
    per cases;
    suppose
A33:  C = {};
      consider p,q being Point of TOP-REAL 2 such that
A34:  p <> q and
A35:  p in D and
A36:  q in D by TOPREAL2:4;
      reconsider CC = {p,q} as Subset of TOP-REAL 2;
A37:  q in CC by TARSKI:def 2;
      p in CC by TARSKI:def 2;
      then
A38:  CC is non trivial by A34,A37,REALSET1:14;
      reconsider pp = {p}, qq = {q} as Subset of TOP-REAL 2;
      CC = pp \/ qq by ENUMSET1:41;
      then
A39:  CC is compact by COMPTS_1:19;
A40:  CC <> D
      proof
        assume
        CC = D;
        then D \ CC = {} by XBOOLE_1:37;
        then not {}((TOP-REAL 2)|D) is connected by A34,A35,A36,JORDAN6:60;
        hence thesis;
      end;
      CC c= D by A35,A36,ZFMISC_1:38;
      then CC c< D by A40,XBOOLE_0:def 8;
      then consider
      p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2
      such that
A41:  B is_an_arc_of p1,p2 and
      CC c= B and
A42:  B c= D by A3,A38,A39;
      take p1, p2, B;
      thus B is_an_arc_of p1,p2 by A41;
      thus C c= B by A33,XBOOLE_1:2;
      thus thesis by A42;
    end;
    suppose
      C <> {};
      then consider x being Element of TOP-REAL 2 such that
A43:  C = {x} by A32,Th2;
      consider y being Element of D such that
A44:  x <> y by Th3;
      reconsider y9 = y as Element of TOP-REAL 2;
      reconsider Y = {y9} as compact non empty Subset of TOP-REAL 2;
      reconsider Cy = C \/ Y as non empty compact Subset of TOP-REAL 2 by A31,
COMPTS_1:19;
A45:  x in C by A43,TARSKI:def 1;
A46:  Cy <> D
      proof
        assume
        Cy = D;
        then
A47:    D \ Cy = {} by XBOOLE_1:37;
        Cy = {x,y} by A43,ENUMSET1:41;
        then not {}((TOP-REAL 2)|D) is connected by A2,A45,A44,A47,JORDAN6:60;
        hence thesis;
      end;
      {y} c= D;
      then Cy c= D by A2,XBOOLE_1:8;
      then
A48:  Cy c< D by A46,XBOOLE_0:def 8;
A49:  C c= Cy by XBOOLE_1:7;
      y in Y by TARSKI:def 1;
      then y in Cy by XBOOLE_0:def 3;
      then Cy is non trivial by A45,A44,A49,REALSET1:14;
      then consider
      p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2
      such that
A50:  B is_an_arc_of p1,p2 and
A51:  Cy c= B and
A52:  B c= D by A3,A48;
      take p1, p2, B;
      thus B is_an_arc_of p1,p2 by A50;
      thus C c= B by A49,A51,XBOOLE_1:1;
      thus thesis by A52;
    end;
  end;
  suppose
    C is non trivial;
    hence thesis by A1,A31,A3;
  end;
end;