The Mizar article:

On the Decompositions of Intervals and Simple Closed Curves

by
Adam Grabowski

Received August 7, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: BORSUK_4
[ MML identifier index ]


environ

 vocabulary BOOLE, TOPREAL1, EUCLID, ARYTM_1, PRE_TOPC, COMPTS_1, SEQ_1,
      TOPREAL2, RELAT_2, BORSUK_1, SUBSET_1, RCOMP_1, TOPS_2, TOPMETR,
      CONNSP_1, ARYTM_3, SQUARE_1, RELAT_1, ORDINAL2, LATTICES, T_0TOPSP,
      SEQ_2, INTEGRA1, REALSET1, FUNCT_1, BORSUK_4, PARTFUN1, TREAL_1, FUNCT_4,
      ARYTM, JORDAN1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, REALSET1, FUNCT_2,
      STRUCT_0, PRE_TOPC, COMPTS_1, FUNCT_4, RCOMP_1, EUCLID, TOPREAL1,
      TOPREAL2, SEQ_4, T_0TOPSP, TREAL_1, CONNSP_1, BORSUK_1, BORSUK_3, TSEP_1,
      RCOMP_2, JORDAN1, TOPMETR, PSCOMP_1, INTEGRA1, TOPS_2;
 constructors REALSET1, JORDAN2C, TOPS_2, TOPREAL2, TOPREAL1, CONNSP_1,
      RCOMP_2, PSCOMP_1, INTEGRA1, TMAP_1, BORSUK_3, COMPTS_1, YELLOW_8,
      PARTFUN1, LIMFUNC1, SPPOL_1, TOPGRP_1, TREAL_1, DOMAIN_1, XCMPLX_0,
      MEMBERED, JORDAN1;
 clusters XREAL_0, RELSET_1, REVROT_1, TOPREAL6, STRUCT_0, PRE_TOPC, BORSUK_2,
      REALSET1, INTEGRA1, TEX_1, TEX_2, JORDAN1B, YELLOW13, EUCLID, MEMBERED,
      ZFMISC_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions XBOOLE_0, TARSKI, CONNSP_1, PARTFUN1, JORDAN1;
 theorems TOPS_2, T_0TOPSP, BORSUK_1, RCOMP_2, PRE_TOPC, COMPTS_1, TARSKI,
      TOPREAL5, TOPMETR, TOPREAL1, RCOMP_1, SPPOL_1, CONNSP_1, ZFMISC_1,
      JORDAN5A, AXIOMS, XREAL_0, STRUCT_0, SQUARE_1, REAL_1, TOPREAL6,
      PSCOMP_1, TREAL_1, XBOOLE_0, XBOOLE_1, JORDAN6, JORDAN1, SEQ_4, JGRAPH_5,
      INTEGRA1, INTEGRA2, TSEP_1, TOPREAL2, JORDAN5B, REALSET1, FUNCT_2,
      FUNCT_1, GOBOARD9, RELAT_1, PARTFUN1, RFUNCT_2, BORSUK_3, FUNCT_4,
      TOPS_1, JGRAPH_2, CIRCCMB2, TOPMETR2, TEX_2, SUBSET_1, XCMPLX_1;

begin :: Preliminaries

definition
  cluster -> non trivial Simple_closed_curve;
  coherence
  proof
    let D be Simple_closed_curve;
    consider p1,p2 being Point of TOP-REAL 2 such that
A1: p1 <> p2 & p1 in D & p2 in D by TOPREAL2:5;
    thus thesis by A1,SPPOL_1:3;
  end;
end;

definition let T be non empty TopSpace;
  cluster non empty compact connected Subset of T;
  existence
  proof
    consider t being Element of T;
    reconsider E = {t} as Subset of T;
    take E;
    thus thesis by CONNSP_1:29;
  end;
end;

definition
  cluster -> real Element of I[01];
  coherence
  proof
    let a be Element of I[01];
      a in [. 0, 1 .] by BORSUK_1:83;
    hence thesis by XREAL_0:def 1;
  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:  p in B & not p in A by A2,XBOOLE_0:def 4;
     reconsider p as Element of X by A2;
     take p;
       A c= B by A1,XBOOLE_0:def 8;
     hence thesis by A3,ZFMISC_1:40;
   end;

theorem Th2:
  for X being non empty set,
      A being non empty Subset of X holds
   A is trivial iff ex x being Element of X st A = {x}
   proof
     let X be non empty set,
         A be non empty Subset of X;
     hereby assume A is trivial;
       then consider s being Element of A such that
A1:    A = {s} by TEX_2:def 1;
       thus ex x being Element of X st A = {x} by A1;
     end;
     given x being Element of X such that
A2:  A = {x};
     thus thesis by A2;
   end;

definition 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 REALSET1:def 20;
    take X = {x, y};
      x in X & y in X by TARSKI:def 2;
    hence thesis by A1,SPPOL_1:4;
  end;
end;

theorem
    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:32;
    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,XBOOLE_0:def 4;
    take q;
    thus thesis by A1,ZFMISC_1:64;
  end;

definition let X be non trivial set;
 cluster non trivial Subset of X;
 existence
  proof
   take [#]X;
   thus thesis by SUBSET_1:def 4;
  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 p' = p;
      X \ { p' } is non empty by REALSET1:32;
    then consider q being set such that
A1: q in X \ { p' } by XBOOLE_0:def 1;
      q in X by A1,XBOOLE_0:def 4;
    then reconsider q as Element of T;
    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
      let x1,x2 be set;
      assume
A5:   x1 in dom g & x2 in dom f \ dom g;
then A6:   g.x1 in rng g by FUNCT_1:12;
A7:   dom f \ dom g c= dom f by XBOOLE_1:36;
then A8:   f.x2 in rng f by A5,FUNCT_1:12;
        { a } c= dom f & { a } c= dom g by A3,XBOOLE_1:17;
then A9:   a in dom f & a in dom g by ZFMISC_1:37;
      assume g.x1 = f.x2;
      then f.x2 in rng f /\ rng g by A6,A8,XBOOLE_0:def 3;
      then f.x2 = f.a by A4,TARSKI:def 1;
then x2 = a by A1,A5,A7,A9,FUNCT_1:def 8;
      then dom g meets (dom f \ dom g) by A5,A9,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;
    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 A6: f tolerates g by PARTFUN1:def 6;
A7: dom (f") = rng f & dom (g") = rng g by A1,A2,FUNCT_1:55;
      for x being set st x in dom (f") /\ dom (g") holds f".x = g".x
    proof
      let x be set;
      assume A8: x in dom (f") /\ dom (g");
        { a } c= dom f by A3,XBOOLE_1:17;
then A9:   a in dom f by ZFMISC_1:37;
        { a } c= dom g by A3,XBOOLE_1:17;
then A10:   a in dom g by ZFMISC_1:37;
        x = f.a by A4,A7,A8,TARSKI:def 1;
then A11:   a = f".x by A1,A9,FUNCT_1:54;
        x = g.a by A4,A5,A7,A8,TARSKI:def 1;
      hence thesis by A2,A10,A11,FUNCT_1:54;
    end;
then A12: f" tolerates g" by PARTFUN1:def 6;
A13: F is one-to-one by A1,A2,A3,A4,Th5;
A14: rng F = (rng f) \/ (rng g) by A6,CIRCCMB2:5;
      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 A15: dom gf = rng F by A6,CIRCCMB2:5;
A16: dom F = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A17: dom f c= dom F by XBOOLE_1:7;
A18: dom g c= dom F by A16,XBOOLE_1:7;
      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
A19:     y in rng F & x = gf.y;
        per cases by A15,A19,FUNCT_4:13;
        suppose
A20:     y in dom (f");
then A21:     y in rng f by A1,FUNCT_1:55;
          x = f".y by A12,A19,A20,FUNCT_4:16;
        then x in dom f & y = f.x by A1,A21,FUNCT_1:54;
        hence x in dom F & y = F.x by A6,A17,FUNCT_4:16;
        suppose
A22:     y in dom (g");
then A23:     y in rng g by A2,FUNCT_1:55;
          x = g".y by A19,A22,FUNCT_4:14;
        then x in dom g & y = g.x by A2,A23,FUNCT_1:54;
        hence x in dom F & y = F.x by A18,FUNCT_4:14;
      end;
      assume
A24:   x in dom F & y = F.x;
      per cases by A24,FUNCT_4:13;
        suppose
A25:     x in dom f;
then A26:     y = f.x by A6,A24,FUNCT_4:16;
then A27:     x = f".y by A1,A25,FUNCT_1:54;
A28:     y in rng f by A25,A26,FUNCT_1:12;
          rng F = (rng f) \/ (rng g) by A6,CIRCCMB2:5;
then A29:     rng f c= rng F by XBOOLE_1:7;
          y in dom (f") by A1,A28,FUNCT_1:55;
        hence thesis by A12,A27,A28,A29,FUNCT_4:16;
        suppose
A30:     x in dom g;
then A31:     y = g.x by A24,FUNCT_4:14;
then A32:     x = g".y by A2,A30,FUNCT_1:54;
A33:     y in rng g by A30,A31,FUNCT_1:12;
A34:     rng g c= rng F by A14,XBOOLE_1:7;
          y in dom (g") by A2,A33,FUNCT_1:55;
        hence thesis by A32,A33,A34,FUNCT_4:14;
     end;
     hence thesis by A13,A15,FUNCT_1:54;
  end;

theorem Th7:
  for n being Nat,
      A being non empty 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 Nat,
        A be non empty 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;
    then A \ { p, q } c= A \ {p} by XBOOLE_1:34;
    hence thesis by A1,XBOOLE_1:3;
  end;

theorem
    for n being Nat,
      a,b being Point of TOP-REAL n holds LSeg (a,b) is convex
  proof
    let n be Nat;
    let a,b be Point of TOP-REAL n;
    set A = LSeg(a,b);
    let w1,w2 be Point of TOP-REAL n;
    assume w1 in A & w2 in A;
    hence thesis by TOPREAL1:12;
  end;

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 A1:s1 <= s3 & s1 < s4 & 0 <= l & l <= 1;
      now per cases;
      suppose l=0;
      hence thesis by A1;
      suppose l=1;
      hence thesis by A1;
      suppose A2: not(l=0 or l=1);
then A3:   l>0 & l<1 by A1,REAL_1:def 5;
A4:   l*s1<l*s4 by A1,A2,REAL_1:70;
        1-l>0 by A3,SQUARE_1:11;
then A5:   (1-l)*s1<=(1-l)*s3 by A1,AXIOMS:25;
        (1-l)*s1+l*s1=(1-l+l)*s1 by XCMPLX_1:8
                  .=1 * s1 by XCMPLX_1:27
                  .=s1;
      hence thesis by A4,A5,REAL_1:67;
    end;
    hence thesis;
  end;

theorem Th10:
  for x being set, a, b being real number st a <= b &
    x in [. a, b .] holds x in ]. a, b .[ or x = a or x = b
   proof
     let x be set, a,b be real number;
     assume a <= b & x in [. a, b .];
     then x in ]. a, b .[ \/ {a,b} by RCOMP_1:11;
     then x in ]. a, b .[ or x in {a,b} by XBOOLE_0:def 2;
     hence x in ]. a, b .[ or x = a or x = b by TARSKI:def 2;
   end;

theorem Th11:
  for a, b, c, d being real number st
    ].a,b.[ meets [.c,d.] holds b > c
  proof
    let a, b, c, d be real number;
    assume A1: ].a,b.[ meets [.c,d.];
    assume A2: b <= c;
    consider x being set such that
A3: x in ].a,b.[ & x in [.c,d.] by A1,XBOOLE_0:3;
      x in {r where r is Real: a <r & r< b} by A3,RCOMP_1:def 2;
    then consider x' being Real such that
A4: x' = x & a < x' & x' < b;
      x in {r where r is Real: c <= r & r <= d} by A3,RCOMP_1:def 1;
    then consider y' being Real such that
A5: y' = x & c <= y' & y' <= d;
    thus thesis by A2,A4,A5,AXIOMS:22;
  end;

theorem Th12:
  for a, b, c, d being real number st
    b <= c holds [. a, b .] misses ]. c, d .[
  proof
    let a, b, c, d be real number;
    assume A1: b <= c;
    assume [.a,b.] meets ].c,d.[;
    then consider x being set such that
A2: x in [.a,b.] & x in ].c,d.[ by XBOOLE_0:3;
      x in {r where r is Real: a<=r & r<=b} by A2,RCOMP_1:def 1;
    then consider x' being Real such that
A3: x' = x & a <= x' & x' <= b;
      x in {r where r is Real: c < r & r<d} by A2,RCOMP_1:def 2;
    then consider y' being Real such that
A4: y' = x & c < y' & y' < d;
    thus thesis by A1,A3,A4,AXIOMS:22;
  end;

theorem Th13:
  for a, b, c, d being real number st
    b <= c holds ]. a, b .[ misses [. c, d .]
  proof
    let a, b, c, d be real number;
    assume A1: b <= c;
    assume ]. a, b .[ meets [. c, d .];
    then consider x being set such that
A2: x in ]. a, b .[ & x in [. c, d .] by XBOOLE_0:3;
      x in {r where r is Real: a<r & r<b} by A2,RCOMP_1:def 2;
    then consider x' being Real such that
A3: x' = x & a < x' & x' < b;
      x in {r where r is Real: c <= r & r <= d} by A2,RCOMP_1:def 1;
    then consider y' being Real such that
A4: y' = x & c <= y' & y' <= d;
    thus thesis by A1,A3,A4,AXIOMS:22;
  end;

theorem
    for a, b, c, d being real number st a < b &
    [.a,b.] c= [.c,d.] holds c <= a & b <= d
  proof
    let a, b, c, d be real number;
    assume A1: a < b;
    assume A2: [.a,b.] c= [.c,d.];
A3: a in [.a,b.] by A1,RCOMP_1:15;
      b in [.a,b.] by A1,RCOMP_1:15;
    hence thesis by A2,A3,TOPREAL5:1;
  end;

theorem Th15:
  for a, b, c, d being real number st a < b &
    ].a,b.[ c= [.c,d.] holds c <= a & b <= d
  proof
    let a, b, c, d be real number;
    assume A1: a < b & ].a,b.[ c= [.c,d.];
then ].a,b.[ <> {} by RCOMP_1:15;
then A2: ].a,b.[ meets [.c,d.] by A1,XBOOLE_1:69;
    assume A3: c > a or b > d;
    per cases by A3;
    suppose a < c;
    then consider ac be real number such that
A4: a < ac & ac < c by REAL_1:75;
      b > c by A2,Th11;
    then ac < b by A4,AXIOMS:22;
    then ac in ].a,b.[ by A4,JORDAN6:45;
    hence thesis by A1,A4,TOPREAL5:1;
    suppose A5: d < b;
    set ad = max (a,d);
      ad < b by A1,A5,RCOMP_2:2;
    then consider ac be real number such that
A6: ad < ac & ac < b by REAL_1:75;
A7: a <= ad & d <= ad by SQUARE_1:46;
then A8: d < ac by A6,AXIOMS:22;
      a < ac by A6,A7,AXIOMS:22;
    then ac in ].a,b.[ by A6,JORDAN6:45;
    hence thesis by A1,A8,TOPREAL5:1;
  end;

theorem
    for a, b, c, d being real number st a < b &
    ].a,b.[ c= [.c,d.] holds [.a,b.] c= [.c,d.]
  proof
    let a, b, c, d be real number;
    assume A1: a < b;
then A2: ].a,b.[ <> {} by RCOMP_1:15;
    assume A3: ].a,b.[ c= [.c,d.];
then A4: ].a,b.[ meets [.c,d.] by A2,XBOOLE_1:69;
    thus [.a,b.] c= [.c,d.]
    proof
      let x be set;
      assume A5: x in [.a,b.];
      per cases by A1,A5,Th10;
      suppose A6: x = a;
        now per cases;
        suppose A7: not a in [.c,d.];
          now per cases by A7,TOPREAL5:1;
          suppose a < c;
          then consider ac be real number such that
A8:       a < ac & ac < c by REAL_1:75;
            b > c by A4,Th11;
          then ac < b by A8,AXIOMS:22;
          then ac in ].a,b.[ by A8,JORDAN6:45;
          hence thesis by A3,A8,TOPREAL5:1;
          suppose d < a;
          hence thesis by A4,Th12;
        end;
        hence thesis;
        suppose a in [.c,d.];
        hence thesis by A6;
      end;
      hence thesis;
      suppose A9: x = b;
        now per cases;
        suppose A10: not b in [.c,d.];
          now per cases by A10,TOPREAL5:1;
          suppose b < c;
          then consider ac be real number such that
A11:       b < ac & ac < c by REAL_1:75;
            b > c by A4,Th11;
          hence thesis by A11,AXIOMS:22;
          suppose d < b;
          hence thesis by A1,A3,Th15;
        end;
        hence thesis;
        suppose b in [.c,d.];
        hence thesis by A9;
      end;
      hence thesis;
      suppose x in ].a,b.[;
      hence thesis by A3;
    end;
  end;

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: 0 <= a by A1,Th15,BORSUK_1:83;
      b <= 1 by A1,A2,Th15,BORSUK_1:83;
    hence thesis by A3,BORSUK_1:83,TREAL_1:1;
  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 RCOMP_2:17;
    assume A = ].a,b.];
then A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:83,XBOOLE_1:1;
then A4: 0 <= a by A1,Th15;
      b <= 1 by A1,A3,Th15;
    hence thesis by A4,BORSUK_1:83,TREAL_1:1;
  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 RCOMP_2:17;
    assume A = [.a,b.[;
then A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:83,XBOOLE_1:1;
then A4: 0 <= a by A1,Th15;
      b <= 1 by A1,A3,Th15;
    hence thesis by A4,BORSUK_1:83,TREAL_1:1;
  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;
    assume A1: a <> b;
A2: ].a,b.] c= [.a,b.] by RCOMP_2:17;
      [.a,b.] is closed by RCOMP_1:23;
then A3: Cl ].a,b.] c= [.a,b.] by A2,PSCOMP_1:32;
      ].a,b.[ c= ].a,b.] by RCOMP_2:17;
    then Cl ].a,b.[ c= Cl ].a,b.] by PSCOMP_1:37;
    then [.a,b.] c= Cl ].a,b.] by A1,TOPREAL6:82;
    hence thesis by A3,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;
    assume A1: a <> b;
A2: [.a,b.[ c= [.a,b.] by RCOMP_2:17;
      [.a,b.] is closed by RCOMP_1:23;
then A3: Cl [.a,b.[ c= [.a,b.] by A2,PSCOMP_1:32;
      ].a,b.[ c= [.a,b.[ by RCOMP_2:17;
    then Cl ].a,b.[ c= Cl [.a,b.[ by PSCOMP_1:37;
    then [.a,b.] c= Cl [.a,b.[ by A1,TOPREAL6:82;
    hence thesis by A3,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 A1: a < b & A = ].a,b.[;
then A2: Cl ].a,b.[ = [.a,b.] by TOPREAL6:82;
    reconsider A1 = ].a,b.[ as Subset of R^1 by TOPMETR:24;
      [.a,b.] c= the carrier of I[01] by A1,Th17;
then A3: [.a,b.] c= [#]I[01] by PRE_TOPC:12;
      Cl A = (Cl A1) /\ [#]I[01] by A1,PRE_TOPC:47
        .= [.a,b.] /\ [#]I[01] by A2,TOPREAL6:80
        .= [.a,b.] by A3,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 A1: a < b & A = ].a,b.];
then A2: Cl ].a,b.] = [.a,b.] by Th20;
    reconsider A1 = ].a,b.] as Subset of R^1 by TOPMETR:24;
      [.a,b.] c= the carrier of I[01] by A1,Th18;
then A3: [.a,b.] c= [#]I[01] by PRE_TOPC:12;
      Cl A = (Cl A1) /\ [#]I[01] by A1,PRE_TOPC:47
        .= [.a,b.] /\ [#]I[01] by A2,TOPREAL6:80
        .= [.a,b.] by A3,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 A1: a < b & A = [.a,b.[;
then A2: Cl [.a,b.[ = [.a,b.] by Th21;
    reconsider A1 = [.a,b.[ as Subset of R^1 by TOPMETR:24;
      [.a,b.] c= the carrier of I[01] by A1,Th19;
then A3: [.a,b.] c= [#]I[01] by PRE_TOPC:12;
      Cl A = (Cl A1) /\ [#]I[01] by A1,PRE_TOPC:47
        .= [.a,b.] /\ [#]I[01] by A2,TOPREAL6:80
        .= [.a,b.] by A3,XBOOLE_1:28;
    hence thesis;
  end;

theorem
    for a,b being real number st a < b holds
   [.a,b.] <> ].a,b.]
  proof
    let a,b be real number;
    assume A1: a < b;
      not a in ].a,b.] by RCOMP_2:4;
    hence thesis by A1,TOPREAL5:1;
  end;

theorem Th26:
  for a, b being real number holds
    [.a,b.[ misses {b} & ].a,b.] misses {a}
  proof
    let a, b be real number;
      not b in [.a,b.[ by RCOMP_2:3;
    hence [.a,b.[ misses {b} by ZFMISC_1:56;
      not a in ].a,b.] by RCOMP_2:4;
    hence thesis by ZFMISC_1:56;
  end;

Lm1:
  for a, b being real number holds
    ].a,b.[ misses {b} & ].a,b.[ misses {a}
  proof
    let a, b be real number;
      not b in ].a,b.[ by JORDAN6:45;
    hence ].a,b.[ misses {b} by ZFMISC_1:56;
      not a in ].a,b.[ by JORDAN6:45;
    hence thesis by ZFMISC_1:56;
  end;

theorem Th27:
  for a, b being real number st a <= b holds
    [. a, b .] \ { a } = ]. a, b .]
  proof
    let a, b be real number;
A1: ].a,b.] misses { a } by Th26;
    assume a <= b;
    then [.a,a.] \/ ].a,b.] = [.a,b.] by RCOMP_2:20;
    then { a } \/ ].a,b.] = [.a,b.] by RCOMP_1:14;
    then ].a,b.] \ { a } = [.a,b.] \ { a } by XBOOLE_1:40;
    hence thesis by A1,XBOOLE_1:83;
  end;

theorem Th28:
  for a, b being real number st a <= b holds
    [. a, b .] \ { b } = [. a, b .[
  proof
    let a, b be real number;
A1: [.a,b.[ misses { b } by Th26;
    assume a <= b;
    then [.b,b.] \/ [.a,b.[ = [.a,b.] by RCOMP_2:21;
    then { b } \/ [.a,b.[ = [.a,b.] by RCOMP_1:14;
    then [.a,b.[ \ { b } = [.a,b.] \ { b } by XBOOLE_1:40;
    hence thesis by A1,XBOOLE_1:83;
  end;

theorem Th29:
  for a, b, c being real number st a < b & b < c holds
    ]. a, b .] /\ [. b, c .[ = { b }
  proof
    let a, b, c be real number;
    assume
A1: a < b & b < c;
    then b in [. b, c .[ by RCOMP_2:3;
then A2: { b } c= [. b, c .[ by ZFMISC_1:37;
A3: [. b, c .[ c= [. b, c .] by RCOMP_2:17;
      ]. a, b .[ misses [. b, c .] by Th13;
then A4: ]. a, b .[ misses [. b, c .[ by A3,XBOOLE_1:63;
      ]. a, b .] = ]. a, b .[ \/ { b } by A1,RCOMP_2:6;
    then ]. a, b .] /\ [. b, c .[ = { b } /\ [. b, c .[ by A4,XBOOLE_1:78
               .= { b } by A2,XBOOLE_1:28;
    hence thesis;
  end;

theorem Th30:
  for a, b, c being real number holds
    [. a, b .[ misses [. b, c .] & [. a, b .] misses ]. b, c .]
  proof
    let a, b, c be real number;
    thus [.a,b.[ misses [.b,c.]
    proof
      assume [.a,b.[ meets [.b,c.];
      then consider x being set such that
A1:   x in [.a,b.[ & x in [.b,c.] by XBOOLE_0:3;
      reconsider x' = x as Real by A1;
        x' < b & x' >= b by A1,RCOMP_2:3,TOPREAL5:1;
      hence thesis;
    end;
    thus [.a,b.] misses ].b,c.]
    proof
      assume [.a,b.] meets ].b,c.];
      then consider x being set such that
A2:   x in [.a,b.] & x in ].b,c.] by XBOOLE_0:3;
      reconsider x' = x as Real by A2;
        x' <= b & x' > b by A2,RCOMP_2:4,TOPREAL5:1;
      hence thesis;
    end;
  end;

theorem Th31:
  for a, b, c being real number st a <= b & b <= c holds
   [.a,c.] \ {b} = [.a,b.[ \/ ].b,c.]
  proof
    let a, b, c be real number;
    assume a <= b & b <= c;
    then [.a,c.] = [.a,b.[ \/ [.b,b.] \/ ].b,c.] by RCOMP_2:13;
then A1: [.a,c.] = [.a,b.[ \/ {b} \/ ].b,c.] by RCOMP_1:14;
      [.a,b.[ misses {b} & ].b,c.] misses {b} by Th26;
then A2: [.a,b.[ \/ ].b,c.] misses {b} by XBOOLE_1:70;
      [.a,c.] \ {b} = [.a,b.[ \/ ].b,c.] \/ {b} \ {b} by A1,XBOOLE_1:4;
    hence thesis by A2,XBOOLE_1:88;
  end;

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 a <= b & A = [.a,b.];
    then a in A & b in A by RCOMP_1:15;
    hence thesis by JORDAN5A:2;
  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 A1: a < b & b < c & A = [.a,b.[ & B = ].b,c.];
    then Cl A = [.a,b.] by Th24;
    hence Cl A misses B by A1,Th30;
      Cl B = [.b,c.] by A1,Th23;
    hence A misses Cl B by A1,Th30;
  end;

theorem Th34:
  for a, b being real number st a <= b holds
    [. a, b .] = [. a, b .[ \/ { b }
  proof
    let a, b be real number;
    assume
A1: a <= b;
      [. a, b .[ \/ { b } = [. a, b .[ \/ [. b, b .] by RCOMP_1:14
        .= [. a, b .] by A1,RCOMP_2:21;
    hence thesis;
  end;

theorem Th35:
  for a, b being real number st a <= b holds
    [. a, b .] = { a } \/ ]. a, b .]
  proof
    let a, b be real number;
    assume
A1: a <= b;
      { a } \/ ]. a, b .] = [. a, a .] \/ ]. a, b .] by RCOMP_1:14
        .= [. a, b .] by A1,RCOMP_2:20;
    hence thesis;
  end;

theorem Th36:
  for a, b, c, d being real number st a <= b & b < c & c <= d holds
    [. a, d .] = [. a, b .] \/ ]. b, c .[ \/ [. c, d .]
  proof
    let a, b, c, d be real number;
    assume
A1: a <= b & b < c & c <= d;
    then a <= c & b <= d by AXIOMS:22;
    then [. a, d .] = [. a, b .[ \/ [. b, c .] \/ ]. c, d .] by A1,RCOMP_2:13
       .= [. a, b .[ \/ ({ b } \/ ]. b, c .]) \/ ]. c, d .] by A1,Th35
       .= [. a, b .[ \/ { b } \/ ]. b, c .] \/ ]. c, d .] by XBOOLE_1:4
       .= [. a, b .] \/ ]. b, c .] \/ ]. c, d .] by A1,Th34
       .= [. a, b .] \/ (]. b, c .[ \/ { c }) \/ ]. c, d .] by A1,RCOMP_2:6
       .= [. a, b .] \/ ]. b, c .[ \/ { c } \/ ]. c, d .] by XBOOLE_1:4
       .= [. a, b .] \/ ]. b, c .[ \/ ({ c } \/ ]. c, d .]) by XBOOLE_1:4
       .= [. a, b .] \/ ]. b, c .[ \/ [. c, d .] by A1,Th35;
    hence thesis;
  end;

theorem Th37:
  for a, b, c, d being real number st a <= b & b < c & c <= d holds
    [. a, d .] \ ([. a, b .] \/ [. c, d .]) = ]. b, c .[
  proof
    let a, b, c, d be real number;
    set A = [. a, b .], B = ]. b, c .[, C = [. c, d .], D = [. a, d .];
    assume
A1: a <= b & b < c & c <= d;
A2: B misses A by Th12;
      B misses C by Th13;
then A3: B misses A \/ C by A2,XBOOLE_1:70;
      D \ (A \/ C) = (B \/ A \/ C) \ (A \/ C) by A1,Th36
                .= (B \/ (A \/ C)) \ (A \/ C) by XBOOLE_1:4
                .= B by A3,XBOOLE_1:88;
    hence thesis;
  end;

theorem Th38:
  for a, b, c being real number st a < b & b < c holds
    ]. a, b .] \/ ]. b, c .[ = ]. a, c .[
  proof
    let a, b, c be real number;
    assume
A1: a < b & b < c;
then A2: a < c by AXIOMS:22;
A3: ]. a, c .[ misses { c } by Lm1;
      not c in ]. a, b .] by A1,RCOMP_2:4;
then A4: ]. a, b .] misses { c } by ZFMISC_1:56;
      ]. b, c .[ misses { c } by Lm1;
then A5: ]. a, b .] \/ ]. b, c .[ misses { c } by A4,XBOOLE_1:70;
      ]. a, b .] \/ ]. b, c .] = ]. a, c .] by A1,RCOMP_2:12;
    then ]. a, b .] \/ (]. b, c .[ \/ { c }) = ]. a, c .]
      by A1,RCOMP_2:6;
    then ]. a, b .] \/ (]. b, c .[ \/ { c }) = ]. a, c .[ \/ { c }
      by A2,RCOMP_2:6;
    then ]. a, b .] \/ ]. b, c .[ \/ { c } = ]. a, c .[ \/ { c }
      by XBOOLE_1:4;
    then ]. a, b .] \/ ]. b, c .[ = ]. a, c .[ \/ { c } \ { c }
      by A5,XBOOLE_1:88;
    hence thesis by A3,XBOOLE_1:88;
  end;

theorem Th39:
  for a, b, c being real number st a < b & b < c holds
    [. b, c .[ c= ]. a, c .[
  proof
    let a, b, c be real number;
    assume
A1: a < b & b < c;
    let x be set;
    assume
A2: x in [. b, c .[;
    then reconsider r = x as real number by XREAL_0:def 1;
A3: b <= r & r < c by A2,RCOMP_2:3;
    then a < r by A1,AXIOMS:22;
    hence thesis by A3,JORDAN6:45;
  end;

theorem Th40:
  for a, b, c being real number st a < b & b < c holds
    ]. a, b .] \/ [. b, c .[ = ]. a, c .[
  proof
    let a, b, c be real number;
    assume
A1: a < b & b < c;
    then ]. a, b .] \/ ]. b, c .[ = ]. a, c .[ by Th38;
then A2: ]. a, b .] c= ]. a, c .[ by XBOOLE_1:7;
      [. b, c .[ c= ]. a, c .[ by A1,Th39;
    hence ]. a, b .] \/ [. b, c .[ c= ]. a, c .[ by A2,XBOOLE_1:8;
    thus ]. a, c .[ c= ]. a, b .] \/ [. b, c .[
    proof
      let x be set; assume A3: x in ]. a, c .[;
      then reconsider r = x as real number by XREAL_0:def 1;
A4:   a < r & r < c by A3,JORDAN6:45;
        now per cases;
        suppose r <= b;
        then r in ]. a, b .] by A4,RCOMP_2:4;
        hence thesis by XBOOLE_0:def 2;
        suppose r > b;
        then r in [. b, c .[ by A4,RCOMP_2:3;
        hence thesis by XBOOLE_0:def 2;
      end;
      hence thesis;
    end;
  end;

theorem Th41:
  for a, b, c being real number st a < b & b < c holds
    ]. a, c .[ \ ]. a, b .] = ]. b, c .[
  proof
    let a, b, c be real number;
    assume
A1: a < b & b < c;
A2: ]. a, b .] c= [. a, b .] by RCOMP_2:17;
      ]. b, c .[ misses [. a, b .] by Th12;
then A3: ]. b, c .[ misses ]. a, b .] by A2,XBOOLE_1:63;
      ]. a, b .] \/ ]. b, c .[ \ ]. a, b .] = ]. a, c .[ \ ]. a, b .]
      by A1,Th38;
    then ]. b, c .[ \ ]. a, b .] = ]. a, c .[ \ ]. a, b .] by XBOOLE_1:40;
    hence thesis by A3,XBOOLE_1:83;
  end;

theorem Th42:
  for a, b, c being real number st a < b & b < c holds
    ]. a, c .[ \ [. b, c .[ = ]. a, b .[
  proof
    let a, b, c be real number;
    assume
A1: a < b & b < c;
then A2: ]. a, c .[ = ]. a, b .] \/ ]. b, c .[ by Th38
              .= ]. a, b .[ \/ { b } \/ ]. b, c .[ by A1,RCOMP_2:6
              .= ]. a, b .[ \/ ({ b } \/ ]. b, c .[) by XBOOLE_1:4
              .= ]. a, b .[ \/ [. b, c .[ by A1,RCOMP_2:5;
A3: [. b, c .[ c= [. b, c .] by RCOMP_2:17;
      ]. a, b .[ misses [. b, c .] by Th13;
    then ]. a, b .[ misses [. b, c .[ by A3,XBOOLE_1:63;
    hence thesis by A2,XBOOLE_1:88;
  end;

theorem Th43:
  for p1, p2 being Point of I[01] holds
    [. p1, p2 .] is Subset of I[01] by BORSUK_1:83,RCOMP_1:16;

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 .[ c= [. a,b .] by RCOMP_1:15;
      [. a,b .] is Subset of I[01] by Th43;
    then ]. a,b .[ c= the carrier of I[01] by A1,XBOOLE_1:1;
    hence thesis;
  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 is Real by XREAL_0:def 1;
      {p} = [.p,p.] by RCOMP_1:14;
    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 A1: a <= b & b <= c & a in A & c in A;
    per cases by A1,REAL_1:def 5;
    suppose a = b or b = c;
    hence thesis by A1;
    suppose A2: a < b & b < c & a in A & c in A;
    assume not b in A;
then A3: A c= [. 0,1 .] \ {b} by BORSUK_1:83,ZFMISC_1:40;
A4: 0 <= a & c <= 1 by JORDAN5A:2;
then A5: 0 < b & b < 1 by A2,AXIOMS:22;
then A6: A c= [. 0,b .[ \/ ]. b,1 .] by A3,Th31;
A7: [.0,b.[ c= [.0,b.] & ].b,1 .] c= [.b,1 .] by RCOMP_2:17;
      b in [. 0,1 .] & 0 in [.0,1 .] & 1 in [.0,1 .] by A5,TOPREAL5:1;
    then [.0,b.] c= [. 0,1 .] & [. b,1 .] c= [.0,1 .] by RCOMP_1:16;
    then [.0,b.[ c= the carrier of I[01] & ].b,1 .] c= the carrier of I[01]
      by A7,BORSUK_1:83,XBOOLE_1:1;
    then reconsider B = [.0,b.[, C = ].b,1 .] as non empty Subset of I[01]
      by A2,A4,RCOMP_2:3,4;
A8: B,C are_separated by A5,Th33;
      now per cases by A6,A8,CONNSP_1:17;
      suppose A c= B;
      hence contradiction by A2,RCOMP_2:3;
      suppose A c= C;
      hence contradiction by A2,RCOMP_2:4;
    end;
    hence thesis;
  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 A1: a in A & b in A;
then A2: 0 <= a & b <= 1 by JORDAN5A:2;
    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 & a <= z & z <= b;
      0 <= z & z <= 1 by A2,A3,AXIOMS:22;
    then reconsider z as Point of I[01] by JORDAN5A:2;
      z in A by A1,A3,Th46;
    hence thesis by A3;
  end;

theorem Th48:
  for a, b being real number,
      A being Subset of I[01] st a <= b & A = [.a,b.] holds
    A is closed
  proof
    let a, b be real number,
        A be Subset of I[01];
    assume A1: a <= b & A = [.a,b.];
    then 0 <= a & b <= 1 by Th32;
then A2: Closed-Interval-TSpace(a,b) is closed SubSpace of
       Closed-Interval-TSpace(0,1) by A1,TREAL_1:6;
    then the carrier of Closed-Interval-TSpace(a,b) is
      Subset of Closed-Interval-TSpace(0,1)
       by BORSUK_1:35;
    then reconsider BA = the carrier of Closed-Interval-TSpace(a,b) as
      Subset of Closed-Interval-TSpace(0,1);
      BA is closed by A2,BORSUK_1:def 14;
    hence thesis by A1,TOPMETR:25,27;
  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];
    assume A1: p1 <= p2;
    A2: 0 <= p1 & p2 <= 1 by JORDAN5A:2;
    set S = [. p1, p2 .];
      S c= [.0,1.] by BORSUK_1:83,RCOMP_1:16;
    then reconsider S as Subset of I[01] by BORSUK_1:83;
A3: S is closed by A1,Th48;
A4: Closed-Interval-TSpace(p1,p2) is connected by A1,TREAL_1:23;
      I[01] | S = Closed-Interval-TSpace(p1,p2) by A1,A2,JGRAPH_5:7;
    hence thesis by A1,A3,A4,COMPTS_1:17,CONNSP_1:def 3,RCOMP_1:15;
  end;

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

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

Lm2:
  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
    let A be Subset of REAL, B be Subset of I[01];
    assume A1: A = B;
A2: the carrier of I[01] c= the carrier of R^1 by BORSUK_1:35;
    then A c= the carrier of R^1 by A1,XBOOLE_1:1;
    then reconsider C = A as Subset of R^1;
    reconsider Z = the carrier of I[01] as Subset of R^1
      by A2;
  Z is closed by Lm2,BORSUK_1:def 14;
then A3: B is closed iff C is closed by A1,TSEP_1:8;
    hereby assume A is closed;
then A4:   C is closed by TOPREAL6:79;
        C c= the carrier of I[01] by A1;
      then C c= [#] I[01] by PRE_TOPC:12;
      then C /\ [#] I[01] = B by A1,XBOOLE_1:28;
      hence B is closed by A4,PRE_TOPC:43;
    end;
    assume B is closed;
    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;
      inf C <= c & c <= sup C by INTEGRA2:1;
    hence thesis by AXIOMS:22;
  end;

theorem Th54:
  for C being non empty compact connected Subset of I[01],
      C' being Subset of REAL st C = C' & [. inf C', sup C' .] c= C' holds
   [. inf C', sup C' .] = C'
  proof
    let C be non empty compact connected Subset of I[01],
        C' be Subset of REAL;
    assume A1: C = C' & [. inf C', sup C' .] c= C';
    assume [. inf C', sup C' .] <> C';
    then not C' c= [. inf C', sup C' .] by A1,XBOOLE_0:def 10;
    then consider c being set such that
A2: c in C' & not c in [. inf C', sup C' .] by TARSKI:def 3;
    reconsider c as real number by A2,XREAL_0:def 1;
      inf C' <= c & c <= sup C' by A1,A2,Th51;
    hence thesis by A2,TOPREAL5: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 C' = C as Subset of REAL by BORSUK_1:83,XBOOLE_1:1;
      C is closed by COMPTS_1:16;
then A1: C' is closed by Th52;
A2: C' is bounded_below bounded_above by Th50;
then A3: inf C' in C' by A1,RCOMP_1:31;
      sup C' in C' by A1,A2,RCOMP_1:30;
    then [. inf C', sup C' .] c= C' by A3,Th47;
then A4: [. inf C', sup C' .] = C' by Th54;
      C' is bounded by A2,SEQ_4:def 3;
    then inf C' <= sup C' by SEQ_4:24;
    hence thesis by A4,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 C' = C as closed-interval Subset of REAL by Th55;
A1: C' = [. inf C', sup C' .] by INTEGRA1:5;
      inf C' <= sup C' by Th53;
    then inf C' in C & sup C' in C by A1,RCOMP_1:15;
    then reconsider p1 = inf C', p2 = sup C' as Point of I[01];
    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,RCOMP_1:15;
    take I[01] | E;
    thus thesis by JORDAN1:1;
  end;
  uniqueness by TSEP_1:5;
end;

theorem Th57:
  for A being Subset of I[01] st A = the carrier of I(01) holds
    I(01) = I[01] | A
  proof
    let A be Subset of I[01];
    assume
A1: A = the carrier of I(01);
      the carrier of (I[01]|A) = A by JORDAN1:1;
    hence thesis by A1,TSEP_1:5;
  end;

theorem Th58:
  the carrier of I(01) = (the carrier of I[01]) \ {0,1}
  proof
A1: the carrier of I(01) = ]. 0,1 .[ by Def1;
A2: ].0,1.[ misses {0,1} by JORDAN6:44;
      [.0,1.] = ].0,1.[ \/ {0,1} by RCOMP_1:11;
    hence thesis by A1,A2,BORSUK_1:83,XBOOLE_1:88;
  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 JORDAN6:45;
    end;
    assume 0 < r & r < 1;
    then r in ]. 0, 1 .[ by JORDAN6:45;
    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
A1: a < b & b <> 1;
 0 <= a & b <= 1 by JORDAN5A:2;
then A2: b < 1 by A1,REAL_1:def 5;
      ]. 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_2:def 2;
      then consider r being Real such that
A3:   x = r & a < r & r <= b;
        0 < r & r < 1 by A2,A3,AXIOMS:22,JORDAN5A:2;
      hence thesis by A3,Th60;
    end;
    hence thesis by A1,RCOMP_2:4;
  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
A1: a < b & a <> 0;
A2: 0 <= a & b <= 1 by JORDAN5A:2;
      [. 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_2:def 1;
      then consider r being Real such that
A3:   x = r & a <= r & r < b;
        0 < r & r < 1 by A1,A2,A3,AXIOMS:22;
      hence thesis by A3,Th60;
    end;
    hence thesis by A1,RCOMP_2: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;
    consider f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|D
      such that
A1: f is_homeomorphism by TOPREAL2:def 1;
    thus thesis by A1,T_0TOPSP:def 1;
end;

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

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

theorem
    for p1, p2 being Point of TOP-REAL 2 st p1 <> p2 holds
    I[01], (TOP-REAL 2) | LSeg (p1, p2) are_homeomorphic
  proof
    let p1, p2 be Point of TOP-REAL 2;
    assume p1 <> p2;
    then LSeg (p1, p2) is_an_arc_of p1, p2 by TOPREAL1:15;
    hence thesis by Th65;
  end;

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 & E = [. p1,p2 .];
    reconsider T = I(01)|E as SubSpace of I[01] by TSEP_1:7;
      0 <= p1 & p2 <= 1 by JORDAN5A:2;
    then reconsider S = Closed-Interval-TSpace(p1,p2) as SubSpace of I[01]
      by A1,TOPMETR:27,TREAL_1:6;
A2: the carrier of S = E by A1,TOPMETR:25;
      the carrier of T = E by JORDAN1:1;
then A3: S = T by A2,TSEP_1:5;
    set f = L[01]((#)(p1,p2), (p1,p2)(#));
      f is_homeomorphism by A1,TREAL_1:20;
    hence thesis by A3,TOPMETR:27,T_0TOPSP:def 1;
  end;

theorem Th68:
  for A being non empty Subset of TOP-REAL 2,
      p, q being Point of TOP-REAL 2,
      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 map of I[01]|E, (TOP-REAL 2)|A st
    E = [. a, b .] & f is_homeomorphism & f.a = p & f.b = q
  proof
    let A be non empty Subset of TOP-REAL 2,
        p, q be Point of TOP-REAL 2,
        a, b be Point of I[01];
    assume that
A1: A is_an_arc_of p, q and
A2: a < b;
    reconsider E = [. a, b .] as non empty Subset of I[01] by A2,Th49;
    take E;
    consider f being map of I[01], (TOP-REAL 2)|A such that
A3: f is_homeomorphism & f.0 = p & f.1 = q by A1,TOPREAL1:def 2;
    0 <= a & b <= 1 by JORDAN5A:2;
then A5: I[01]|E = Closed-Interval-TSpace(a,b) by A2,JGRAPH_5:7;
    then reconsider e = P[01](a,b,(#)(0,1),(0,1)(#)) as map of I[01]|E, I[01]
      by TOPMETR:27;
    set g = f * e;
A6: e is_homeomorphism by A2,A5,TOPMETR:27,TREAL_1:20;
    reconsider g as map of I[01]|E, (TOP-REAL 2)|A;
    take g;
    thus E = [. a, b .];
    thus g is_homeomorphism by A3,A6,TOPS_2:71;
A7: 0 = (#)(0,1) & a = (#)(a,b) by A2,TREAL_1:def 1;
A8: 1 = (0,1)(#) & b = (a,b)(#) by A2,TREAL_1:def 2;
      a in E by A2,RCOMP_1:15;
    then a in the carrier of I[01]|E by JORDAN1:1;
    hence g.a = f.(e.a) by FUNCT_2:21
             .= p by A2,A3,A7,TREAL_1:16;
      b in E by A2,RCOMP_1:15;
    then b in the carrier of I[01]|E by JORDAN1:1;
    hence g.b = f.(e.b) by FUNCT_2:21
             .= q by A2,A3,A8,TREAL_1:16;
  end;

theorem Th69:
  for A being TopSpace, B being non empty TopSpace,
      f being map of A, B,
      C being TopSpace, X being Subset of A st
   f is continuous &
   C is SubSpace of B holds
  for h being map 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 map 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;
    let h be map of A|X, C;
    assume
A3: h = f|X;
      the carrier of A|X = X by JORDAN1:1;
    then f|X is Function of the carrier of A|X, the carrier of B
      by FUNCT_2:38;
    then reconsider g = f|X as map of A|X, B;
      g is continuous by A1,TOPMETR:10;
    hence thesis by A2,A3,TOPMETR:8;
  end;

theorem Th70:
  for X being Subset of I[01],
      a, b being Point of I[01] st
   a <= b & X = ]. a, b .[ holds X is open
  proof
    let X be Subset of I[01],
        a, b be Point of I[01];
    assume
A1: a <= b & X = ]. a, b .[;
    per cases;
    suppose a <> b;
then A2: a < b by A1,REAL_1:def 5;
A3: 0 in the carrier of I[01] & 1 in the carrier of I[01] by JORDAN5A:2;
A4: 0 <= a by JORDAN5A:2;
    reconsider A = [. 0, a .] as Subset of I[01] by A3,Th43;
A5: b <= 1 by JORDAN5A:2;
    reconsider B = [. b, 1 .] as Subset of I[01] by A3,Th43;
A6: A is closed by A4,Th48;
      B is closed by A5,Th48;
then A7: A \/ B is closed by A6,TOPS_1:36;
A8: X = [. 0, 1 .] \ (A \/ B) by A1,A2,A4,A5,Th37;
      [#] I[01] = [. 0, 1 .] by BORSUK_1:83,PRE_TOPC:12;
    then X = (A \/ B)` by A8,PRE_TOPC:17;
    hence thesis by A7,TOPS_1:29;
    suppose a = b;
    then X = {} by A1,RCOMP_1:12;
    then X in the topology of I[01] by PRE_TOPC:5;
    hence thesis by PRE_TOPC:def 5;
  end;

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

theorem Th72:
  for X being non empty Subset of I(01),
      a being Point of I[01] st
    0 < a & X = ]. 0, a .] holds X is closed
  proof
    let X be non empty Subset of I(01),
        a be Point of I[01];
    assume A1: 0 < a & X = ]. 0, a .];
A2: 1 in the carrier of I[01] by JORDAN5A:2;
A3: a <= 1 by JORDAN5A:2;
      a <> 1
    proof
      assume
A4:   a = 1;
        a in X by A1,RCOMP_2:4;
      hence contradiction by A4,Th60;
    end;
then A5: a < 1 by A3,REAL_1:def 5;
  [#] I(01) = the carrier of I(01) by PRE_TOPC:12 .= ]. 0, 1 .[ by Def1;
    then [#] I(01) \ X = ]. a, 1 .[ by A1,A5,Th41;
    then [#] I(01) \ X is open by A2,A3,Th71;
    hence thesis by PRE_TOPC:def 6;
  end;

theorem Th73:
  for X being non empty Subset of I(01),
      a being Point of I[01] st
    X = [. a, 1 .[ holds X is closed
  proof
    let X be non empty Subset of I(01),
        a be Point of I[01];
    assume A1: X = [. a, 1 .[;
A2: 1 in the carrier of I[01] & 0 in the carrier of I[01] by JORDAN5A:2;
A3: a <> 1 by A1,RCOMP_2:7;
      a <= 1 by JORDAN5A:2;
then A4: a < 1 by A3,REAL_1:def 5;
A5: [#] I(01) = the carrier of I(01) by PRE_TOPC:12
             .= ]. 0, 1 .[ by Def1;
A6: a <> 0
    proof
      assume a = 0;
      then 0 in X by A1,RCOMP_2:3;
      then 0 in the carrier of I(01);
      then 0 in ]. 0, 1 .[ by Def1;
      hence thesis by JORDAN6:45;
    end;
A7: 0 <= a by JORDAN5A:2;
    then [#] I(01) \ X = ]. 0, a .[ by A1,A4,A5,A6,Th42;
    then [#] I(01) \ X is open by A2,A7,Th71;
    hence thesis by PRE_TOPC:def 6;
  end;

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

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

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

theorem Th79:
  for C being non empty Subset of TOP-REAL 2,
      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 2)|C are_homeomorphic holds
  ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of s1,s2
  proof
    let C be non empty Subset of TOP-REAL 2,
        E be Subset of I(01);
    given p1, p2 being Point of I[01] such that
A1: p1 < p2 & E = [. p1,p2 .];
A2: the carrier of I(01)|E = E by JORDAN1:1;
      E is non empty by A1,Th49;
then A3: I(01)|E is non empty by A2,STRUCT_0:def 1;
    assume
A4: I(01)|E, (TOP-REAL 2)|C are_homeomorphic;
      I[01], I(01)|E are_homeomorphic by A1,Th67;
    then I[01], (TOP-REAL 2)|C are_homeomorphic by A3,A4,BORSUK_3:3;
    then consider g being map of I[01], (TOP-REAL 2)|C such that
A5: g is_homeomorphism by T_0TOPSP:def 1;
    set s1 = g.0, s2 = g.1;
A6: the carrier of (TOP-REAL 2)|C c= the carrier of TOP-REAL 2
      by BORSUK_1:35;
      0 in the carrier of I[01] by JORDAN5A:2;
then A7: g.0 in the carrier of (TOP-REAL 2)|C by FUNCT_2:7;
      1 in the carrier of I[01] by JORDAN5A:2;
    then g.1 in the carrier of (TOP-REAL 2)|C by FUNCT_2:7;
    then reconsider s1, s2 as Point of TOP-REAL 2 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 map of (TOP-REAL 2) | Dp, I(01),
      C being non empty Subset of TOP-REAL 2 st
    f is_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 map of (TOP-REAL 2) | Dp, I(01),
        C be non empty Subset of TOP-REAL 2;
    assume
A1: f is_homeomorphism & C c= Dp;
    given p1, p2 being Point of I[01] such that
A2: p1 < p2 & f.:C = [. p1,p2 .];
    reconsider E = [. p1,p2 .] as Subset of I(01) by A2;
    set g = f"| E;
      f" is_homeomorphism by A1,TOPS_2:70;
then A3: f" is one-to-one by TOPS_2:def 5;
A4: f is continuous one-to-one by A1,TOPS_2:def 5;
A5: f"(f.:C) = C
    proof
      thus f"(f.:C) c= C by A4,FUNCT_1:152;
        dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
      then C c= dom f by A1,JORDAN1:1;
      hence C c= f"(f.:C) by FUNCT_1:146;
    end;
A6: rng f = [#] I(01) by A1,TOPS_2:def 5;
then A7: f".:E = C by A2,A4,A5,TOPS_2:68;
A8: rng g = f".:E by RELAT_1:148
         .= the carrier of ((TOP-REAL 2)|C) by A7,JORDAN1:1
         .= [#] ((TOP-REAL 2)|C) by PRE_TOPC:12;
      the carrier of (I(01)|E) = E by JORDAN1:1;
    then g is Function of the carrier of I(01)|E,
      the carrier of (TOP-REAL 2)|Dp by FUNCT_2:38;
    then g is Function of the carrier of I(01)|E,
      the carrier of (TOP-REAL 2)|C by A8,FUNCT_2:8;
    then reconsider g as map of I(01)|E, (TOP-REAL 2)|C;
      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 JORDAN1:1;
then A9: dom g = [#] (I(01)|E) by PRE_TOPC:12;
A10: g is one-to-one by A3,FUNCT_1:84;
      the carrier of (TOP-REAL 2)|C = C & the carrier of (TOP-REAL 2)|Dp = Dp
      by JORDAN1:1;
then A11: (TOP-REAL 2)|C is SubSpace of (TOP-REAL 2) | Dp by A1,TOPMETR:4;
      f" is continuous by A1,TOPS_2:def 5;
then A12: g is continuous by A11,Th69;
A13: g" = (g qua Function)" by A8,A10,TOPS_2:def 4
      .= ((f" qua Function)")|((f").:E) by A3,RFUNCT_2:40
      .= ((f qua Function)"")|((f").:E) by A4,A6,TOPS_2:def 4
      .= f|C by A4,A7,FUNCT_1:65;
    then reconsider t = f|C as map of (TOP-REAL 2) | C, I(01)|E;
      C c= the carrier of ((TOP-REAL 2) | Dp) by A1,JORDAN1:1;
    then reconsider C' = C as Subset of (TOP-REAL 2) | Dp;
  ((TOP-REAL 2) | Dp)|C' = (TOP-REAL 2) | C by A1,JORDAN6:47;
    then t is continuous by A4,Th69;
    then g is_homeomorphism by A8,A9,A10,A12,A13,TOPS_2:def 5;
    then I(01)|E, (TOP-REAL 2)|C are_homeomorphic by T_0TOPSP:def 1;
    hence thesis by A2,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;
     suppose C is non trivial;
     then consider d1,d2 being Point of TOP-REAL 2 such that
A3:  d1 in C & d2 in C & d1 <> d2 by SPPOL_1:4;
       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 & C c= D \ {p} by Th1;
A5:  d1 in D \ {p} & d2 in D \ {p} by A3,A4;
     reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2 by A3,A4;
       (TOP-REAL 2) | Dp, I(01) are_homeomorphic by A4,Th77;
     then consider f being map of (TOP-REAL 2) | Dp, I(01) such that
A6:  f is_homeomorphism by T_0TOPSP:def 1;
A7:  C c= the carrier of (TOP-REAL 2) | Dp by A4,JORDAN1:1;
     then reconsider C' = C as Subset of (TOP-REAL 2) | Dp;
     set fC = f.:C';
       C c= [#] ((TOP-REAL 2) | Dp) by A7,PRE_TOPC:12;
then A8:  C' is compact by COMPTS_1:11;
A9:  C' is connected by CONNSP_1:24;
A10:  f is continuous by A6,TOPS_2:def 5;
       rng f = [#] I(01) by A6,TOPS_2:def 5;
     then reconsider fC as compact connected Subset of I(01)
       by A8,A9,A10,COMPTS_1:24,TOPREAL5:5;
     reconsider fC' = fC as Subset of I[01] by PRE_TOPC:39;
       fC' c= the carrier of I(01);
then A11:  fC' c= [#] I(01) by PRE_TOPC:12;
A12:  for P being Subset of I(01) st P=fC' holds P is compact;
A13:  d1 in the carrier of (TOP-REAL 2) | Dp by A5,JORDAN1:1;
A14:  f.d1 in f.:C' by A3,FUNCT_2:43;
A15:  d2 in the carrier of (TOP-REAL 2) | Dp by A5,JORDAN1:1;
A16:  f.d2 in f.:C' by A3,FUNCT_2:43;
     then reconsider fC' as non empty compact connected Subset of I[01]
       by A11,A12,COMPTS_1:11,CONNSP_1:24;
A17:  d1 in dom f by A13,FUNCT_2:def 1;
A18:  d2 in dom f by A15,FUNCT_2:def 1;
     consider p1, p2 being Point of I[01] such that
A19:  p1 <= p2 & fC' = [. p1,p2 .] by Th56;
A20:  f is one-to-one by A6,TOPS_2:def 5;
       p1 <> p2
     proof
       assume p1 = p2;
then A21:    fC' = {p1} by A19,RCOMP_1:14;
then A22:    f.d1 = p1 by A14,TARSKI:def 1;
         f.d2 = p1 by A16,A21,TARSKI:def 1;
       hence thesis by A3,A17,A18,A20,A22,FUNCT_1:def 8;
     end;
     then p1 < p2 by A19,REAL_1:def 5;
     then consider s1, s2 being Point of TOP-REAL 2 such that
A23:  C is_an_arc_of s1,s2 by A4,A6,A19,Th80;
     thus thesis by A23;
  end;


Back to top