:: Topological Properties of Subsets in Real Numbers
::  by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, SEQ_1, ORDINAL2, NAT_1, XXREAL_1, REAL_1,
      XXREAL_0, TARSKI, ARYTM_3, ARYTM_1, COMPLEX1, RELAT_1, VALUED_0, SEQ_2,
      XXREAL_2, FUNCT_1, CARD_1, XBOOLE_0, SEQ_4, RCOMP_1, ASYMPT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, SEQ_1,
      SEQ_2, COMSEQ_2, VALUED_0, SEQ_4, XXREAL_0, XXREAL_1, XXREAL_2, RECDEF_1;
 constructors FUNCOP_1, REAL_1, NAT_1, XXREAL_1, COMPLEX1, PARTFUN1, SEQ_2,
      SEQM_3, SEQ_4, RECDEF_1, XXREAL_2, MEMBERED, RELSET_1, RVSUM_1, BINOP_2,
      COMSEQ_2, SEQ_1;
 registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0,
      XXREAL_2, FUNCT_2, SEQ_1, SEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, SEQ_2;
 equalities XBOOLE_0, SUBSET_1, XXREAL_1;
 expansions TARSKI, SEQ_2, XBOOLE_0;
 theorems TARSKI, SUBSET_1, NAT_1, FUNCT_1, FUNCT_2, SEQ_2, SEQM_3, SEQ_4,
      ABSVALUE, RELAT_1, XREAL_0, XBOOLE_0, XCMPLX_0, XCMPLX_1, XREAL_1,
      COMPLEX1, XXREAL_0, NUMBERS, XXREAL_1, VALUED_0, XXREAL_2, ORDINAL1,
      SEQ_1;
 schemes SUBSET_1, FUNCT_2, SEQ_1;

begin

reserve n,n1,m,k for Nat;
reserve x,y for set;
reserve s,g,g1,g2,r,p,p2,q,t for Real;
reserve s1,s2,s3 for Real_Sequence;
reserve Nseq for increasing sequence of NAT;
reserve X for Subset of REAL;

definition
  let g,s be Real;
  redefine func [. g,s .] -> Subset of REAL equals
  {r: g<=r & r<=s };
  coherence
  proof
    now
      let x be object;
      assume x in [. g,s .];
      then
A1:   ex r being Element of ExtREAL st x = r & g <= r & r<=s;
      g in REAL & s in REAL by XREAL_0:def 1;
      hence x in REAL by A1,XXREAL_0:45;
    end;
    hence thesis by TARSKI:def 3;
  end;
  compatibility
  proof
    set Y = {r: g<=r & r<=s };
    let X be Subset of REAL;
A2: [. g,s .] c= Y
    proof
      let x be object;
      assume x in [. g,s .];
      then consider r being Element of ExtREAL such that
A3:   x = r and
A4:   g <= r & r<=s;
      g in REAL & s in REAL by XREAL_0:def 1;
      then r in REAL by A4,XXREAL_0:45;
      hence thesis by A3,A4;
    end;
    Y c= [. g,s .]
    proof
      let x be object;
      assume x in Y;
      then consider r such that
A5:   x = r & g <= r & r<=s;
      r in REAL by XREAL_0:def 1;
      hence thesis by A5,NUMBERS:31;
    end;
    hence thesis by A2;
  end;
end;

definition
  let g,s be ExtReal;
  redefine func ]. g,s .[ -> Subset of REAL equals
  {r : g<r & r<s };
  coherence
  proof
    now
      let x be object;
      assume x in ]. g,s .[;
      then ex r being Element of ExtREAL st x = r & g < r & r<s;
      hence x in REAL by XXREAL_0:48;
    end;
    hence thesis by TARSKI:def 3;
  end;
  compatibility
  proof
    set Y = {r: g<r & r<s };
    let X be Subset of REAL;
A1: Y c= ]. g,s .[
    proof
      let x be object;
      assume x in Y;
      then consider r such that
A2:   x = r & g < r & r<s;
      r in REAL by XREAL_0:def 1;
      hence thesis by A2,NUMBERS:31;
    end;
    ]. g,s .[ c= Y
    proof
      let x be object;
      assume x in ]. g,s .[;
      then consider r being Element of ExtREAL such that
A3:   x = r and
A4:   g < r & r<s;
      r in REAL by A4,XXREAL_0:48;
      hence thesis by A3,A4;
    end;
    hence thesis by A1;
  end;
end;

theorem Th1:
  r in ].p-g,p+g.[ iff |.r-p.|<g
proof
  thus r in ].p-g,p+g.[ implies |.r-p.|<g
  proof
    assume r in ].p-g,p+g.[;
    then
A1: ex s st r=s & p-g<s & s<p+g;
    then p+-g<r;
    then
A2: -g<r-p by XREAL_1:20;
    r-p<g by A1,XREAL_1:19;
    hence thesis by A2,SEQ_2:1;
  end;
  assume
A3: |.r-p.|<g;
  then r-p<g by SEQ_2:1;
  then
A4: r<p+g by XREAL_1:19;
  -g<r-p by A3,SEQ_2:1;
  then r is Real & p+-g<r by XREAL_1:20;
  hence thesis by A4;
end;

theorem
  r in [.p,g.] iff |.p+g-2*r.|<=g-p
proof
  thus r in [.p,g.] implies |.p+g-2*r.|<=g-p
  proof
    assume r in [.p,g.];
    then
A1: ex s st s=r & p<=s & s<=g;
    then 2*r<=2*g by XREAL_1:64;
    then -2*r>=-2*g by XREAL_1:24;
    then (p+g)+-2*r>=(p+g)+-2*g by XREAL_1:7;
    then
A2: p+g-2*r>=-(g-p);
    2*p<=2*r by A1,XREAL_1:64;
    then -2*p>=-2*r by XREAL_1:24;
    then (p+g)+-2*p>=(p+g)+-2*r by XREAL_1:7;
    hence thesis by A2,ABSVALUE:5;
  end;
  assume
A3: |.p+g-2*r.|<=g-p;
  then p+g-2*r>=-(g-p) by ABSVALUE:5;
  then p+g>=p-g+2*r by XREAL_1:19;
  then p+g-(p-g)>=2*r by XREAL_1:19;
  then
A4: 1/2*(2*g)>=1/2*(2*r) by XREAL_1:64;
  g-p>=p+g-2*r by A3,ABSVALUE:5;
  then 2*r+(g-p)>=p+g by XREAL_1:20;
  then 2*r>=p+g-(g-p) by XREAL_1:20;
  then 1/2*(2*r)>=1/2*(2*p) by XREAL_1:64;
 hence r in [.p,g.] by A4;
end;

theorem
  r in ].p,g.[ iff |.p+g-2*r.|<g-p
proof
  thus r in ].p,g.[ implies |.p+g-2*r.|<g-p
  proof
    assume r in ].p,g.[;
    then
A1: ex s st s=r & p<s & s<g;
    then 2*r<2*g by XREAL_1:68;
    then -2*r>-2*g by XREAL_1:24;
    then (p+g)+-2*r>(p+g)+-2*g by XREAL_1:6;
    then
A2: p+g-2*r>-(g-p);
    2*p<2*r by A1,XREAL_1:68;
    then -2*p>-2*r by XREAL_1:24;
    then (p+g)+-2*p>(p+g)+-2*r by XREAL_1:6;
    hence thesis by A2,SEQ_2:1;
  end;
  assume
A3: |.p+g-2*r.|<g-p;
  then p+g-2*r>-(g-p) by SEQ_2:1;
  then p+g>p-g+2*r by XREAL_1:20;
  then p+g-(p-g)>2*r by XREAL_1:20;
  then
A4: 1/2*(2*g)>1/2*(2*r) by XREAL_1:68;
  g-p>p+g-2*r by A3,SEQ_2:1;
  then 2*r+(g-p)>p+g by XREAL_1:19;
  then 2*r>p+g-(g-p) by XREAL_1:19;
  then 1 /2*(2*r)>1/2*(2*p) by XREAL_1:68;
  hence thesis by A4;
end;

definition
  let X;
  attr X is compact means

  for s1 st rng s1 c= X ex s2 st s2 is
  subsequence of s1 & s2 is convergent & lim s2 in X;
end;

definition
  let X;
  attr X is closed means

  for s1 st rng s1 c= X & s1 is convergent holds lim s1 in X;
end;

definition
  let X;
  attr X is open means
  :Def5:
  X` is closed;
end;

theorem Th4:
  for s1 st rng s1 c= [.s,g.] holds s1 is bounded
proof
  let s1 such that
A1: rng s1 c= [.s,g.];
  thus s1 is bounded_above
  proof
    take r = g + 1;
A2: for t st t in rng s1 holds t < r
    proof
      let t;
      assume t in rng s1;
      then t in [.s,g.] by A1;
      then
A3:   ex p st t = p & s <= p & p<=g;
      g < r by XREAL_1:29;
      hence thesis by A3,XXREAL_0:2;
    end;
      let n;
      n in NAT by ORDINAL1:def 12;
      then n in dom s1 by FUNCT_2:def 1;
      then s1.n in rng s1 by FUNCT_1:def 3;
      hence thesis by A2;
  end;
    take r = s - 1;
A4: r + 1 = s - (1-1);
A5: for t st t in rng s1 holds r < t
    proof
      let t;
      assume t in rng s1;
      then t in [.s,g.] by A1;
      then
A6:   ex p st t = p & s <= p & p<=g;
      r < s by A4,XREAL_1:29;
      hence thesis by A6,XXREAL_0:2;
    end;
      let n;
      n in NAT by ORDINAL1:def 12;
      then n in dom s1 by FUNCT_2:def 1;
      then s1.n in rng s1 by FUNCT_1:def 3;
      hence thesis by A5;
end;

theorem Th5:
  [.s,g.] is closed
proof
  for s1 st rng s1 c= [.s,g.] & s1 is convergent holds lim s1 in [.s,g.]
  proof
    let s1;
    assume that
A1: rng s1 c= [.s,g.] and
A2: s1 is convergent;
A3: s <= lim s1
    proof
      set s2 = seq_const s;
A4:   now
        let n;
     n in NAT by ORDINAL1:def 12;
        then n in dom s1 by FUNCT_2:def 1;
        then s1.n in rng s1 by FUNCT_1:def 3;
        then s1.n in [.s,g.] by A1;
        then ex p st s1.n = p & s <= p & p<=g;
        hence s2.n<=s1.n by SEQ_1:57;
      end;
      s2.0 = s by SEQ_1:57;
      then lim s2 = s by SEQ_4:25;
      hence thesis by A2,A4,SEQ_2:18;
    end;
    lim s1 <= g
    proof
      set s2 = seq_const g;
A5:   now
        let n;
     n in NAT by ORDINAL1:def 12;
        then n in dom s1 by FUNCT_2:def 1;
        then s1.n in rng s1 by FUNCT_1:def 3;
        then s1.n in [.s,g.] by A1;
        then ex p st s1.n = p & s <= p & p<=g;
        hence s1.n<=s2.n by SEQ_1:57;
      end;
      s2.0 = g by SEQ_1:57;
      then lim s2 = g by SEQ_4:25;
      hence thesis by A2,A5,SEQ_2:18;
    end;
    hence thesis by A3;
  end;
  hence thesis;
end;

theorem
  [.s,g.] is compact
proof
  for s1 st rng s1 c= [.s,g.] ex s2 st s2 is subsequence of s1 & s2 is
  convergent & lim s2 in [.s,g.]
  proof
    let s1;
A1: [.s,g.] is closed by Th5;
    assume
A2: (rng s1) c= [.s,g.];
    then consider s2 be Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent by Th4,SEQ_4:40;
    take s2;
    ex Nseq st s2 = s1*Nseq by A3,VALUED_0:def 17;
    then rng s2 c= rng s1 by RELAT_1:26;
    then rng s2 c= [.s,g.] by A2;
    hence thesis by A3,A4,A1;
  end;
  hence thesis;
end;

theorem Th7:
  ].p,q.[ is open
proof
  defpred P[Real] means $1<=p or q<=$1;
  consider X such that
A1: for r be Element of REAL holds r in X iff P[r] from SUBSET_1:sch 3;
  now
    let s1 such that
A2: (rng s1) c= X and
A3: s1 is convergent;
A4: lim s1 in REAL by XREAL_0:def 1;
    lim s1<=p or q<=lim s1
    proof
      assume
A5:   not thesis;
      then 0<lim s1 - p by XREAL_1:50;
      then consider n1 such that
A6:   for m st n1<=m holds |.s1.m-lim s1.|<lim s1-p by A3,SEQ_2:def 7;
      0<q - lim s1 by A5,XREAL_1:50;
      then consider n such that
A7:   for m st n<=m holds |.s1.m-lim s1.|<q-lim s1 by A3,SEQ_2:def 7;
      consider k such that
A8:   max(n,n1)<k by SEQ_4:3;
      n1<=max(n,n1) by XXREAL_0:25;
      then n1<=k by A8,XXREAL_0:2;
      then
A9:   |.s1.k-lim s1.|<lim s1 - p by A6;
      -|.s1.k-lim s1.| <= s1.k-lim s1 by ABSVALUE:4;
      then -(s1.k-lim s1) <= -(-|.s1.k-lim s1.|) by XREAL_1:24;
      then -(s1.k-lim s1)<lim s1 - p by A9,XXREAL_0:2;
      then -(lim s1 - p)< -(-(s1.k-lim s1)) by XREAL_1:24;
      then p - lim s1 < s1.k-lim s1;
      then
A10:   p < s1.k by XREAL_1:9;
      n<=max(n,n1) by XXREAL_0:25;
      then n<=k by A8,XXREAL_0:2;
      then
      s1.k-lim s1 <= |.s1.k-lim s1.| & |.s1.k-lim s1.|<q-lim s1 by A7,
ABSVALUE:4;
      then s1.k-lim s1 < q-lim s1 by XXREAL_0:2;
      then
A11:  s1.k < q by XREAL_1:9;
A12:   k in NAT by ORDINAL1:def 12;
A13:   s1.k in REAL by XREAL_0:def 1;
      dom s1 = NAT by FUNCT_2:def 1;
      then s1.k in rng s1 by FUNCT_1:def 3,A12;
      hence contradiction by A1,A2,A11,A10,A13;
    end;
    hence lim s1 in X by A1,A4;
  end;
  then
A14: X is closed;
  now
    let r;
A15: r in REAL by XREAL_0:def 1;
    assume r in ].p,q.[`;
    then not r in ].p,q.[ by XBOOLE_0:def 5;
    then r<=p or q<=r;
    hence r in X by A1,A15;
  end;
  then
A16: ].p,q.[` c= X;
  now
    let r;
    assume r in X;
    then not ex s st s=r & p<s & s<q by A1;
    then r in REAL & not r in ].p,q.[ by XREAL_0:def 1;
    hence r in ].p,q.[` by XBOOLE_0:def 5;
  end;
  then X c= ].p,q.[`;
  then ].p,q.[` = X by A16;
  hence thesis by A14;
end;

registration
  let p, q be Real;
  cluster ].p,q.[ -> open for Subset of REAL;
  coherence by Th7;
  cluster [.p,q.] -> closed for Subset of REAL;
  coherence by Th5;
end;

theorem Th8:
  X is compact implies X is closed
proof
  assume
A1: X is compact;
  assume not X is closed;
  then consider s1 such that
A2: rng s1 c= X and
A3: s1 is convergent & not lim s1 in X;
  ex s2 st s2 is subsequence of s1 & s2 is convergent & (lim s2) in X by A1,A2;
  hence contradiction by A3,SEQ_4:17;
end;

registration
  cluster compact -> closed for Subset of REAL;
  coherence by Th8;
end;

theorem Th9:
  (for p st p in X ex r,n st 0<r & (for m st n<m holds r<|.s1.m-p.|))
  implies for s2 st s2 is subsequence of s1 holds not (s2 is convergent &
  lim s2 in X)
proof
  assume that
A1: for p st p in X ex r,n st 0<r & for m st n<m holds r<|.s1.m-p.| and
A2: not for s2 st s2 is subsequence of s1 holds not (s2 is convergent &
  lim s2 in X);
  consider s2 such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent and
A5: lim s2 in X by A2;
  consider r,n such that
A6: 0<r and
A7: for m st n<m holds r<|.s1.m - lim s2.| by A1,A5;
  consider n1 such that
A8: for m st n1<=m holds |.s2.m-(lim s2).|<r by A4,A6,SEQ_2:def 7;
  consider NS being increasing sequence of NAT such that
A9: s2 = s1*NS by A3,VALUED_0:def 17;
  reconsider k = n + 1 + n1 as Element of NAT by ORDINAL1:def 12;
  |.(s1*NS).k-(lim s2).|<r by A8,A9,NAT_1:11;
  then
A10: |.s1.(NS.k)-(lim s2).|<r by FUNCT_2:15;
  n + 1 <= k by NAT_1:11;
  then
A11: n < k by NAT_1:13;
  k<=NS.k by SEQM_3:14;
  then n<NS.k by A11,XXREAL_0:2;
  hence contradiction by A7,A10;
end;

theorem Th10:
  X is compact implies X is real-bounded
proof
  assume
A1: X is compact;
  assume
A2: not X is real-bounded;
    per cases by A2;
    suppose
A3:   not X is bounded_above;
      defpred P[Element of NAT,Element of REAL] means ex q st q =$2 & q in X &
      $1<q;
A4:   for n being Element of NAT ex p being Element of REAL st P[n,p]
      proof
        let n be Element of NAT;
        n is not UpperBound of X by A3,XXREAL_2:def 10;
        then consider t being ExtReal such that
A5:     t in X & n<t by XXREAL_2:def 1;
        take t;
        thus thesis by A5;
      end;
      consider f being sequence of REAL such that
A6:   for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A4);
A7:   now
        let n;
        n in NAT by ORDINAL1:def 12;
        then ex q st q=f.n & q in X & n<q by A6;
        hence f.n in X & n<f.n;
      end;
A8:   for p st p in X ex r,n st 0<r & for m st n<m holds r<|.f.m-p.|
      proof
        let p such that
        p in X;
        consider q such that
A9:     q = 1;
        take r = q;
        consider k such that
A10:    p+1<k by SEQ_4:3;
        take n = k;
        thus 0 < r by A9;
        let m;
        assume n<m;
        then p+1 < m by A10,XXREAL_0:2;
        then p+1 < f.m by A7,XXREAL_0:2;
        then 1 < f.m - p by XREAL_1:20;
        hence thesis by A9,ABSVALUE:def 1;
      end;
      rng f c= X
      proof
        let x be object;
        assume x in rng f;
        then consider y being object such that
A11:    y in dom f and
A12:    x = f.y by FUNCT_1:def 3;
        reconsider y as Element of NAT by A11,FUNCT_2:def 1;
        f.y in X by A7;
        hence thesis by A12;
      end;
      then
      ex s2 st s2 is subsequence of f & s2 is convergent & lim s2 in X by A1;
      hence contradiction by A8,Th9;
    end;
    suppose
A13:  not X is bounded_below;
      defpred P[Element of NAT,Element of REAL] means ex q st q=$2 & q in X &
      q<-$1;
A14:  for n being Element of NAT ex p being Element of REAL st P[n,p]
      proof
        let n be Element of NAT;
        -n is not LowerBound of X by A13,XXREAL_2:def 9;
        then consider t being ExtReal such that
A15:    t in X & t<-n by XXREAL_2:def 2;
        take t;
        thus thesis by A15;
      end;
      consider f being sequence of REAL such that
A16:  for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(
      A14);
A17:  now
        let n;
        n in NAT by ORDINAL1:def 12;
        then ex q st q=f.n & q in X & q<-n by A16;
        hence f.n in X & f.n<-n;
      end;
A18:  for p st p in X ex r,n st 0<r & for m st n<m holds r<|.f.m-p.|
      proof
        let p such that
        p in X;
        consider q such that
A19:    q = 1;
        take r = q;
        consider k such that
A20:    |.p-1.| <k by SEQ_4:3;
        take n = k;
        thus 0 < r by A19;
        let m;
        assume n<m;
        then
A21:    -m<-n by XREAL_1:24;
        -k <p-1 by A20,SEQ_2:1;
        then -m < p-1 by A21,XXREAL_0:2;
        then f.m < p-1 by A17,XXREAL_0:2;
        then f.m +1 < p by XREAL_1:20;
        then 1 < p - f.m by XREAL_1:20;
        then r < |.-(f.m-p).| by A19,ABSVALUE:def 1;
        hence thesis by COMPLEX1:52;
      end;
      rng f c= X
      proof
        let x be object;
        assume x in rng f;
        then consider y being object such that
A22:    y in dom f and
A23:    x = f.y by FUNCT_1:def 3;
        reconsider y as Element of NAT by A22,FUNCT_2:def 1;
        f.y in X by A17;
        hence thesis by A23;
      end;
      then
      ex s2 st s2 is subsequence of f & s2 is convergent & lim s2 in X by A1;
      hence contradiction by A18,Th9;
    end;
end;

theorem
  X is real-bounded closed implies X is compact
proof
  assume that
A1: X is real-bounded and
A2: X is closed;
  now
    let s1 such that
A3: rng s1 c= X;
A4: s1 is bounded_below
    proof
      consider p such that
A5:    p is LowerBound of X by A1,XXREAL_2:def 9;
A6:   for q st q in X holds p<=q by A5,XXREAL_2:def 2;
      take r = p - 1;
A7:   r + 1 = p - (1-1);
A8:   for t st t in rng s1 holds r < t
      proof
        let t;
        assume t in rng s1;
        then
A9:     p<=t by A3,A6;
        r < p by A7,XREAL_1:29;
        hence thesis by A9,XXREAL_0:2;
      end;
      for n holds r < s1.n
      proof
        let n;
        n in NAT by ORDINAL1:def 12;
        then n in dom s1 by FUNCT_2:def 1;
        then s1.n in rng s1 by FUNCT_1:def 3;
        hence thesis by A8;
      end;
      hence thesis;
    end;
    s1 is bounded_above
    proof
      consider p such that
A10:    p is UpperBound of X by A1,XXREAL_2:def 10;
A11:   for q st q in X holds q<=p by A10,XXREAL_2:def 1;
      take r = p+1;
A12:  for t st t in rng s1 holds t < r
      proof
        let t;
        assume t in rng s1;
        then
A13:    t<=p by A3,A11;
        p < r by XREAL_1:29;
        hence thesis by A13,XXREAL_0:2;
      end;
      for n holds s1.n < r
      proof
        let n;
        n in NAT by ORDINAL1:def 12;
        then n in dom s1 by FUNCT_2:def 1;
        then s1.n in rng s1 by FUNCT_1:def 3;
        hence thesis by A12;
      end;
      hence thesis;
    end;
    then s1 is bounded by A4;
    then consider s2 be Real_Sequence such that
A14: s2 is subsequence of s1 and
A15: s2 is convergent by SEQ_4:40;
    ex Nseq st s2 = s1*Nseq by A14,VALUED_0:def 17;
    then rng s2 c= rng s1 by RELAT_1:26;
    then rng s2 c= X by A3;
    then lim s2 in X by A2,A15;
    hence ex s2 st s2 is subsequence of s1 & s2 is convergent & lim s2 in X by
A14,A15;
  end;
  hence thesis;
end;

theorem Th12:
  for X st X<>{} & X is closed & X is bounded_above holds upper_bound X in X
proof
  let X such that
A1: X<>{} and
A2: X is closed and
A3: X is bounded_above and
A4: not upper_bound X in X;
  set s1=upper_bound X;
  defpred P[Element of NAT,Element of REAL] means ex q st q=$2 & q in X & s1 -
  q < 1/($1+1);
A5: for n being Element of NAT ex p being Element of REAL st P[n,p]
  proof
    let n be Element of NAT;
    0<(n+1)";
    then 0<1/(n+1) by XCMPLX_1:215;
    then consider t such that
A6: t in X and
A7: s1 -1/(n+1) <t by A1,A3,SEQ_4:def 1;
    take t;
    s1 < t + 1/(n+1) by A7,XREAL_1:19;
    then s1 -t < 1/(n+1) by XREAL_1:19;
    hence thesis by A6;
  end;
  consider f being sequence of REAL such that
A8: for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A5);
A9: now
    let n;
        n in NAT by ORDINAL1:def 12;
    then ex q st q = f.n & q in X & s1 -q < 1/(n+1) by A8;
    hence f.n in X & s1 - f.n<1/(n+1);
  end;
A10: rng f c= X
  proof
    let x be object;
    assume x in rng f;
    then consider y being object such that
A11: y in dom f and
A12: x = f.y by FUNCT_1:def 3;
    reconsider y as Element of NAT by A11,FUNCT_2:def 1;
    f.y in X by A9;
    hence thesis by A12;
  end;
A13: now
    let s;
    assume
A14: 0<s;
    consider n such that
A15: s"<n by SEQ_4:3;
    take k=n;
    let m;
    assume k<=m;
    then k+1<=m+1 by XREAL_1:6;
    then
A16: 1/(m+1)<=1/(k+1) by XREAL_1:118;
    f.m in X by A9;
    then f.m <= s1 by A3,SEQ_4:def 1;
    then
A17: 0 <= s1-f.m by XREAL_1:48;
    s"+0 <n+1 by A15,XREAL_1:8;
    then 1/(n+1)<1/s" by A14,XREAL_1:76;
    then 1/(n+1)<s by XCMPLX_1:216;
    then 1/(m+1)<s by A16,XXREAL_0:2;
    then s1 - f.m<s by A9,XXREAL_0:2;
    then |.-(f.m - s1).|<s by A17,ABSVALUE:def 1;
    hence |.f.m - s1.|<s by COMPLEX1:52;
  end;
  then
A18: f is convergent;
  then lim f=s1 by A13,SEQ_2:def 7;
  hence contradiction by A2,A4,A18,A10;
end;

theorem Th13:
  for X st X<>{} & X is closed & X is bounded_below holds lower_bound X in X
proof
  let X such that
A1: X<>{} and
A2: X is closed and
A3: X is bounded_below and
A4: not lower_bound X in X;
  set i1=lower_bound X;
  defpred P[Element of NAT,Element of REAL] means ex q st q=$2 & q in X & q-i1
  < 1/($1+1);
A5: for n being Element of NAT ex p being Element of REAL st P[n,p]
  proof
    let n be Element of NAT;
    0<(n+1)";
    then 0<1/(n+1) by XCMPLX_1:215;
    then consider t such that
A6: t in X and
A7: t<i1 + 1/(n+1) by A1,A3,SEQ_4:def 2;
    take t;
    t-i1 < 1/(n+1) by A7,XREAL_1:19;
    hence thesis by A6;
  end;
  consider f being sequence of REAL such that
A8: for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A5);
A9: now
    let n;
        n in NAT by ORDINAL1:def 12;
    then ex q st q = f.n & q in X & q-i1 < 1/(n+1) by A8;
    hence f.n in X & f.n-i1<1/(n+1);
  end;
A10: rng f c= X
  proof
    let x be object;
    assume x in rng f;
    then consider y being object such that
A11: y in dom f and
A12: x = f.y by FUNCT_1:def 3;
    reconsider y as Element of NAT by A11,FUNCT_2:def 1;
    f.y in X by A9;
    hence thesis by A12;
  end;
A13: now
    let s;
    assume
A14: 0<s;
    consider n such that
A15: s"<n by SEQ_4:3;
    take k=n;
    let m;
    assume k<=m;
    then k+1<=m+1 by XREAL_1:6;
    then
A16: 1/(m+1)<=1/(k+1) by XREAL_1:118;
    f.m in X by A9;
    then i1<=f.m by A3,SEQ_4:def 2;
    then
A17: 0 <= f.m-i1 by XREAL_1:48;
    s"+0 <n+1 by A15,XREAL_1:8;
    then 1/(n+1)<1/s" by A14,XREAL_1:76;
    then 1/(n+1)<s by XCMPLX_1:216;
    then 1/(m+1)<s by A16,XXREAL_0:2;
    then f.m-i1<s by A9,XXREAL_0:2;
    hence |.f.m-i1.|<s by A17,ABSVALUE:def 1;
  end;
  then
A18: f is convergent;
  then lim f=i1 by A13,SEQ_2:def 7;
  hence contradiction by A2,A4,A18,A10;
end;

theorem
  for X st X<>{} & X is compact holds upper_bound X in X & lower_bound X in X
proof
  let X such that
A1: X<>{} and
A2: X is compact;
  X is real-bounded closed by A2,Th10;
  hence thesis by A1,Th12,Th13;
end;

theorem
  X is compact & (for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c= X)
  implies ex p,g st X = [.p,g.]
proof
  assume that
A1: X is compact and
A2: for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c= X;
  per cases;
  suppose
A3: X={};
    take 1;
    take 0;
    thus thesis by A3,XXREAL_1:29;
  end;
  suppose
A4: X<>{};
    take p=lower_bound X, g=upper_bound X;
A5: X is real-bounded closed by A1,Th10;
    now
      let r be Element of REAL;
      assume r in X;
      then r<=g & p<=r by A5,SEQ_4:def 1,def 2;
      hence r in [.p,g.];
    end;
    then
A6: X c= [.p,g.];
    upper_bound X in X & lower_bound X in X by A4,A5,Th12,Th13;
    then [.p,g.] c= X by A2;
    hence thesis by A6;
  end;
end;

registration
  cluster open for Subset of REAL;
  existence
  proof
    take ].0,1.[;
    thus thesis;
  end;
end;

definition
  let r be Real;

  mode Neighbourhood of r -> Subset of REAL means
    :Def6:
    ex g st 0<g & it = ]. r-g,r+g.[;
  existence
  proof
    take ].r-1,r+1.[;
    thus thesis;
  end;
end;

registration
  let r be Real;
  cluster -> open for Neighbourhood of r;
  coherence
  proof
    let A be Neighbourhood of r;
    ex g st 0<g & A = ].r-g,r+g.[ by Def6;
    hence thesis;
  end;
end;

theorem
  for N being Neighbourhood of r holds r in N
proof
  let N be Neighbourhood of r;
  ( ex g st 0<g & N = ].r-g,r+g.[)& |.r-r.| = 0 by Def6,ABSVALUE:2;
  hence thesis by Th1;
end;

theorem
  for r for N1,N2 being Neighbourhood of r ex N being Neighbourhood of r
  st N c= N1 & N c= N2
proof
  let r;
  let N1,N2 be Neighbourhood of r;
  consider g1 such that
A1: 0<g1 and
A2: ].r-g1,r+g1.[ = N1 by Def6;
  consider g2 such that
A3: 0<g2 and
A4: ].r-g2,r+g2.[ = N2 by Def6;
  set g = min(g1,g2);
  0<g by A1,A3,XXREAL_0:15;
  then reconsider N = ].r-g,r+g.[ as Neighbourhood of r by Def6;
  take N;
A5: g<=g1 by XXREAL_0:17;
  then
A6: r+g<=r+g1 by XREAL_1:7;
  -g1<=-g by A5,XREAL_1:24;
  then
A7: r+-g1<=r+-g by XREAL_1:7;
A8: g<=g2 by XXREAL_0:17;
  then -g2<=-g by XREAL_1:24;
  then
A9: r+-g2<=r+-g by XREAL_1:7;
A10: r+g<=r+g2 by A8,XREAL_1:7;
  now
    per cases;
    suppose
A11:  g1<=g2;
A12:  now
        let y be object;
        assume
A13:    y in ].r-g,r+g.[;
        then reconsider x1=y as Real;
        ex p2 st y = p2 & r-g<p2 & p2<r+g by A13;
        then x1<r+g2 & r-g2<x1 by A10,A9,XXREAL_0:2;
        hence y in ].r-g2,r+g2.[;
      end;
      g1=g by A11,XXREAL_0:def 9;
      hence ].r-g,r+g.[ c= N1 & ].r-g,r+g.[ c= N2 by A2,A4,A12;
    end;
    suppose
A14:  g2<=g1;
A15:  now
        let y be object;
        assume
A16:    y in ].r-g,r+g.[;
        then reconsider x1=y as Real;
        ex p2 st y = p2 & r-g<p2 & p2<r+g by A16;
        then x1<r+g1 & r-g1<x1 by A6,A7,XXREAL_0:2;
        hence y in ].r-g1,r+g1.[;
      end;
      g2=g by A14,XXREAL_0:def 9;
      hence ].r-g,r+g.[ c= N1 & ].r-g,r+g.[ c= N2 by A2,A4,A15;
    end;
  end;
  hence thesis;
end;

theorem Th18:
  for X being open Subset of REAL, r st r in X ex N being
  Neighbourhood of r st N c= X
proof
  let X be open Subset of REAL, r;
  assume that
A1: r in X and
A2: for N be Neighbourhood of r holds not N c= X;
  defpred P[Nat,Real] means $2 in ].r - 1/($1+1),r + 1/($1+1
  ) .[ & $2 in X`;
A3: now
    let N be Neighbourhood of r;
    consider g such that
    0<g and
A4: N = ].r-g,r+g.[ by Def6;
    not N c= X by A2;
    then consider x being object such that
A5: x in N and
A6: not x in X;
    consider s such that
A7: x=s and
    r-g<s and
    s<r+g by A5,A4;
     reconsider s as Element of REAL by XREAL_0:def 1;
    take s;
    thus s in N by A5,A7;
    thus s in X` by A6,A7,XBOOLE_0:def 5;
  end;
A8: for n being Element of NAT  ex s being Element of REAL st P[n,s]
  proof
    let n be Element of NAT;
    0 < 1 * (n + 1)";
    then 0 < 1/(n + 1) by XCMPLX_0:def 9;
    then reconsider N=]. r - 1/(n+1), r + 1/(n+1) .[ as Neighbourhood of r by
Def6;
    ex s be Element of REAL st s in N & s in X` by A3;
    hence thesis;
  end;
  consider s3 such that
A9: for n being Element of NAT holds P[n,s3.n] from FUNCT_2:sch 3(A8);
  deffunc G(Nat)= r + 1/($1+1);
  deffunc F(Nat)= r - 1/($1+1);
  consider s1 be Real_Sequence such that
A10: for n holds s1.n = F(n) from SEQ_1:sch 1;
  consider s2 be Real_Sequence such that
A11: for n holds s2.n = G(n) from SEQ_1:sch 1;
A12: for n holds s1.n <= s3.n & s3.n <= s2.n
  proof
    let n;
    n in NAT by ORDINAL1:def 12;
    then s3.n in].r - 1/(n+1),r + 1/(n+1) .[ by A9;
    then
A13: ex s st s = s3.n & r - 1/(n+1) <s & s<r + 1/(n+1);
    hence s1.n <= s3.n by A10;
    thus thesis by A11,A13;
  end;
A14: rng s3 c= X`
  proof
    let x be object;
    assume x in rng s3;
    then consider y being object such that
A15: y in dom s3 and
A16: s3.y=x by FUNCT_1:def 3;
    reconsider y as Element of NAT by A15,FUNCT_2:def 1;
    s3.y in X` by A9;
    hence thesis by A16;
  end;
A17: X` is closed by Def5;
A18: now
    let s;
    assume
A19: 0<s;
    consider n such that
A20: s"<n by SEQ_4:3;
    take n;
    let m;
    assume n<=m;
    then n + 1 <= m + 1 by XREAL_1:6;
    then
A21: 1/(m+1) <= 1/(n+1) by XREAL_1:118;
    s" + 0 < n + 1 by A20,XREAL_1:8;
    then 1/(n+1) < 1/s" by A19,XREAL_1:76;
    then
A22: 1/(n+1) < s by XCMPLX_1:216;
    |.s2.m - r.| = |.r + 1/(m+1) - r.| by A11
      .= 1/(m+1) by ABSVALUE:def 1;
    hence |.s2.m - r.| <s by A22,A21,XXREAL_0:2;
  end;
  then
A23: s2 is convergent;
  then
A24: lim s2 = r by A18,SEQ_2:def 7;
A25: now
    let s;
    assume
A26: 0<s;
    consider n such that
A27: s"<n by SEQ_4:3;
    take n;
    let m;
    assume n<=m;
    then n + 1 <= m + 1 by XREAL_1:6;
    then
A28: 1/(m+1) <= 1/(n+1) by XREAL_1:118;
    s" + 0 < n + 1 by A27,XREAL_1:8;
    then 1/(n+1) < 1/s" by A26,XREAL_1:76;
    then
A29: 1/(n+1) < s by XCMPLX_1:216;
    |.s1.m - r.| = |.r - 1/(m+1) - r.| by A10
      .= |.- 1/(m+1).|
      .= |.1/(m+1).| by COMPLEX1:52
      .= 1/(m+1) by ABSVALUE:def 1;
    hence |.s1.m - r.| <s by A29,A28,XXREAL_0:2;
  end;
  then
A30: s1 is convergent;
  then lim s1 = r by A25,SEQ_2:def 7;
  then s3 is convergent & lim s3 = r by A30,A23,A24,A12,SEQ_2:19,20;
  then r in X` by A14,A17;
  hence contradiction by A1,XBOOLE_0:def 5;
end;

theorem
  for X being open Subset of REAL, r st r in X ex g st 0<g & ].r-g,r+g.[ c= X
proof
  let X be open Subset of REAL, r;
  assume r in X;
  then consider N be Neighbourhood of r such that
A1: N c= X by Th18;
  consider g such that
A2: 0<g & N = ].r-g,r+g.[ by Def6;
  take g;
  thus thesis by A1,A2;
end;

theorem
  (for r being Element of REAL st r in X
    ex N be Neighbourhood of r st N c= X) implies X
  is open
proof
  assume that
A1: for r being Element of REAL st r in X
    ex N be Neighbourhood of r st N c= X and
A2: not X is open;
  not X` is closed by A2;
  then consider s1 such that
A3: rng s1 c= X` and
A4: s1 is convergent and
A5: not lim s1 in X`;
  reconsider ls = lim s1 as Element of REAL by XREAL_0:def 1;
  consider N be Neighbourhood of ls such that
A6: N c= X by A1,A5,SUBSET_1:29;
  consider g such that
A7: 0<g and
A8: ]. (lim s1) - g, (lim s1) + g .[ = N by Def6;
  consider n such that
A9: for m st n<=m holds |.s1.m - (lim s1).|<g by A4,A7,SEQ_2:def 7;
  n in NAT by ORDINAL1:def 12;
  then n in dom s1 by FUNCT_2:def 1;
  then
A10: s1.n in rng s1 by FUNCT_1:def 3;
A11: |.s1.n - (lim s1).|<g by A9;
  then s1.n - (lim s1) <g by SEQ_2:1;
  then
A12: s1.n <(lim s1) + g by XREAL_1:19;
  -g < s1.n - (lim s1) by A11,SEQ_2:1;
  then (lim s1) +- g < (lim s1) + (s1.n - (lim s1)) by XREAL_1:6;
  then
  s1.n in {s: (lim s1) - g < s & s <(lim s1) + g} by A12;
  hence contradiction by A3,A6,A8,A10,XBOOLE_0:def 5;
end;

theorem Th21:
  X is open bounded_above implies not upper_bound X in X
proof
  assume that
A1: X is open and
A2: X is bounded_above;
  assume upper_bound X in X;
  then consider N being Neighbourhood of upper_bound X such that
A3: N c= X by A1,Th18;
  consider t such that
A4: t>0 and
A5: N = ].upper_bound X-t,upper_bound X+t.[ by Def6;
A6: upper_bound X + t/2 > upper_bound X by A4,XREAL_1:29,215;
A7: upper_bound X + t/2 +t/2 > upper_bound X + t/2 by A4,XREAL_1:29,215;
  upper_bound X - t < upper_bound X by A4,XREAL_1:44;
  then upper_bound X - t < upper_bound X + t/2 by A6,XXREAL_0:2;
  then upper_bound X + t/2 in {s: upper_bound X-t<s & s<
  upper_bound X+t} by A7;
  hence contradiction by A2,A3,A5,A6,SEQ_4:def 1;
end;

theorem Th22:
  X is open bounded_below implies not lower_bound X in X
proof
  assume that
A1: X is open and
A2: X is bounded_below;
  assume lower_bound X in X;
  then consider N being Neighbourhood of lower_bound X such that
A3: N c= X by A1,Th18;
  consider t such that
A4: t>0 and
A5: N = ].lower_bound X-t,lower_bound X+t.[ by Def6;
A6: lower_bound X - t/2 < lower_bound X by A4,XREAL_1:44,215;
A7: lower_bound X - t/2 - t/2 < lower_bound X - t/2 by A4,XREAL_1:44,215;
  lower_bound X < lower_bound X + t by A4,XREAL_1:29;
  then lower_bound X - t/2 < lower_bound X + t by A6,XXREAL_0:2;
  then lower_bound X - t/2 in {s: lower_bound X-t<s & s<
  lower_bound X+t} by A7;
  hence contradiction by A2,A3,A5,A6,SEQ_4:def 2;
end;

theorem
  X is open real-bounded & (for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c=
  X) implies ex p,g st X = ].p,g.[
proof
  assume that
A1: X is open and
A2: X is real-bounded and
A3: for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c= X;
  per cases;
  suppose
A4: X={};
    take 1;
    take 0;
    thus thesis by A4,XXREAL_1:28;
  end;
  suppose
A5: X<>{};
    take p=lower_bound X, g=upper_bound X;
    now
      let r be Element of REAL;
      thus r in X implies r in ].p,g.[
      proof
        assume
A6:     r in X;
        then p<>r & p<=r by A1,A2,Th22,SEQ_4:def 2;
        then
A7:     p<r by XXREAL_0:1;
        g<>r & r<=g by A1,A2,A6,Th21,SEQ_4:def 1;
        then r<g by XXREAL_0:1;
        hence thesis by A7;
      end;
      assume r in ].p,g.[;
      then
A8:   ex s st s=r & p<s & s<g;
      then g-r>0 by XREAL_1:50;
      then consider g2 such that
A9:   g2 in X & g-(g-r)<g2 by A2,A5,SEQ_4:def 1;
      r-p>0 by A8,XREAL_1:50;
      then consider g1 such that
A10:  g1 in X & g1<p+(r-p) by A2,A5,SEQ_4:def 2;
      reconsider g1, g2 as Real;
      r in {s: g1<=s & s<=g2} & [.g1,g2.] c= X by A3,A9,A10;
      hence r in X;
    end;
    hence thesis by SUBSET_1:3;
  end;
end;

:: From RCOMP_2, AG 19.12.2008

definition
  let g be Real,s be ExtReal;
  redefine func [. g,s .[ -> Subset of REAL equals
  { r : g<=r & r<s };
  coherence
  proof
    now
      let e be object;
      assume e in [. g,s .[;
      then
A1:   ex r being Element of ExtREAL st e = r & g <= r & r<s;
      g in REAL by XREAL_0:def 1;
      hence e in REAL by A1,XXREAL_0:46;
    end;
    hence thesis by TARSKI:def 3;
  end;
  compatibility
  proof
    set Y = {r: g<=r & r<s };
    let X be Subset of REAL;
A2: [. g,s .[ c= Y
    proof
      let e be object;
      assume e in [. g,s .[;
      then consider r being Element of ExtREAL such that
A3:   e = r and
A4:   g <= r & r<s;
      g in REAL by XREAL_0:def 1;
      then r in REAL by A4,XXREAL_0:46;
      hence thesis by A3,A4;
    end;
    Y c= [. g,s .[
    proof
      let e be object;
      assume e in Y;
      then consider r such that
A5:   e = r & g <= r & r<s;
      r in REAL by XREAL_0:def 1;
      hence thesis by A5,NUMBERS:31;
    end;
    hence thesis by A2;
  end;
end;

definition
  let g be ExtReal,s be Real;
  redefine func ]. g,s .] -> Subset of REAL equals
  { r: g<r &  r<=s };
  coherence
  proof
    now
      let e be object;
      assume e in ]. g,s .];
      then
A1:   ex r being Element of ExtREAL st e = r & g < r & r<=s;
      s in REAL by XREAL_0:def 1;
      hence e in REAL by A1,XXREAL_0:47;
    end;
    hence thesis by TARSKI:def 3;
  end;
  compatibility
  proof
    set Y = {r: g<r & r<=s };
    let X be Subset of REAL;
A2: ]. g,s .] c= Y
    proof
      let e be object;
      assume e in ]. g,s .];
      then consider r being Element of ExtREAL such that
A3:   e = r and
A4:   g < r & r<=s;
      s in REAL by XREAL_0:def 1;
      then r in REAL by A4,XXREAL_0:47;
      hence thesis by A3,A4;
    end;
    Y c= ]. g,s .]
    proof
      let e be object;
      assume e in Y;
      then consider r such that
A5:   e = r & g < r & r<=s;
      r in REAL by XREAL_0:def 1;
      hence thesis by A5,NUMBERS:31;
    end;
    hence thesis by A2;
  end;
end;