:: Some Properties of the Intervals
::  by J\'ozef Bia\las
::
:: Received February 5, 1994
:: Copyright (c) 1994-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, FUNCT_1, ZFMISC_1, RELAT_1, SUPINF_2, XXREAL_0, CARD_1,
      SUPINF_1, SUBSET_1, NAT_1, ARYTM_3, ORDINAL1, XXREAL_2, ORDINAL2,
      XBOOLE_0, REAL_1, ARYTM_1, MEASURE5, XXREAL_1, MEMBERED, MEMBER_1,
      TARSKI, XCMPLX_0, FREEALG, QUANTAL1, SETFAM_1, FINSET_1, COMPLEX1, SEQ_1,
      SEQ_2, VALUED_0, SEQ_4, PSCOMP_1, RCOMP_1, PRALG_1, PRE_TOPC, PARTFUN1,
      INT_1, ASYMPT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, FINSET_1,
      NUMBERS, MEMBERED, ABSVALUE, COMPLEX1, VALUED_0, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, MEMBER_1, FUNCT_3, XXREAL_0,
      XXREAL_1, XXREAL_2, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1,
      SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, SUPINF_1, SUPINF_2, MEASURE5,
      VALUED_1;
 constructors WELLORD2, DOMAIN_1, REAL_1, NAT_1, CARD_1, SUPINF_2, MEASURE5,
      SUPINF_1, RCOMP_1, RELSET_1, COMPLEX1, SEQ_2, SEQM_3, VALUED_0, VALUED_1,
      FUNCOP_1, SEQ_4, BINOP_2, LIMFUNC1, MEMBER_1, FUNCT_3, COMSEQ_2, SEQ_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XREAL_0,
      MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, VALUED_0, VALUED_1, NAT_1, INT_1,
      FINSET_1, MEMBER_1, RCOMP_1, SEQ_2, SEQ_4, FCONT_3, FUNCT_2, MEASURE5,
      RELSET_1, XCMPLX_0, SEQ_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions SEQ_2, TARSKI, XBOOLE_0, XXREAL_2, FINSET_1, RCOMP_1;
 equalities SUPINF_2, SUBSET_1, XXREAL_3, RCOMP_1, VALUED_1, XCMPLX_0,
      MEMBER_1;
 expansions SEQ_2, TARSKI, XBOOLE_0, XXREAL_2, RCOMP_1;
 theorems SUPINF_2, FUNCT_1, MEASURE5, FUNCT_2, NAT_1, CARD_4, WELLORD2,
      XREAL_0, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, MEMBERED,
      XXREAL_1, XXREAL_2, XXREAL_3, SETFAM_1, TARSKI, COMPLEX1, ABSVALUE,
      VALUED_1, SEQ_1, XCMPLX_1, SEQ_4, SEQ_2, RCOMP_1, RELSET_1, INT_1,
      SUBSET_1, MEMBER_1;
 schemes RECDEF_1, NAT_1, FINSET_1, FUNCT_2, BINOP_2, DOMAIN_1, FUNCT_1;

begin :: Some theorems about R_eal numbers

theorem
  ex F being sequence of [:NAT,NAT:]
  st F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:]
proof
  consider F being Function such that
A1: F is one-to-one and
A2: dom F = NAT & rng F = [:NAT,NAT:] by CARD_4:5,WELLORD2:def 4;
  F is sequence of [:NAT,NAT:] by A2,FUNCT_2:1;
  hence thesis by A1,A2;
end;

theorem
  for F being sequence of ExtREAL st F is nonnegative holds 0. <= SUM(F)
proof
  let F be sequence of ExtREAL;
  assume F is nonnegative;
  then 0. <= Ser(F).0 by SUPINF_2:40;
  hence thesis by FUNCT_2:4,XXREAL_2:4;
end;

theorem
  for F being sequence of ExtREAL, x being R_eal st
  (ex n being Element of NAT st x <= F.n) & F is nonnegative holds x <= SUM(F)
proof
  let F be sequence of ExtREAL;
  let x be R_eal;
  assume that
A1: ex n being Element of NAT st x <= F.n and
A2: F is nonnegative;
  consider n being Element of NAT such that
A3: x <= F.n by A1;
A4: Ser(F).n <= SUM(F) by FUNCT_2:4,XXREAL_2:4;
  per cases by NAT_1:6;
  suppose
    n = 0;
    then Ser(F).n = F.n by SUPINF_2:def 11;
    hence thesis by A3,A4,XXREAL_0:2;
  end;
  suppose
    ex k being Nat st n = k + 1;
    then consider k being Nat such that
A5: n = k + 1;
    reconsider k as Element of NAT by ORDINAL1:def 12;
A6: 0. <= Ser(F).k by A2,SUPINF_2:40;
    Ser(F).n = Ser(F).k + F.(k + 1) by A5,SUPINF_2:def 11;
    then 0. + x <= Ser(F).n by A3,A5,A6,XXREAL_3:36;
    then x <= Ser(F).n by XXREAL_3:4;
    hence thesis by A4,XXREAL_0:2;
  end;
end;

definition
::$CD
end;

theorem
  for eps being ExtReal st 0. < eps ex F being sequence of ExtREAL st
  (for n being Nat holds 0. < F.n) & SUM(F) < eps
proof
  defpred P[set,set,set] means for a,b being R_eal,s being Nat
  holds (s = $1 & a = $2 & b = $3 implies b = a/2);
  let eps be ExtReal;
  assume 0. < eps;
  then consider x0 being Real such that
A1: 0. < x0 and
A2: x0 < eps by XXREAL_3:3;
  consider x being Real such that
A3: 0. < x and
A4: x + (x qua ExtReal) < x0 by A1,XXREAL_3:50;
  reconsider x as Element of ExtREAL by XXREAL_0:def 1;
A5: for n being Nat for x being Element of ExtREAL ex y being
  Element of ExtREAL st P[n,x,y]
  proof
    let n be Nat;
    let x be Element of ExtREAL;
    reconsider m = x/2 as Element of ExtREAL by XXREAL_0:def 1;
    take m;
    thus thesis;
  end;
  consider F being sequence of ExtREAL such that
A6: F.0 = x & for n being Nat holds P[n,F.n,F.(n+1)] from
  RECDEF_1:sch 2(A5);
  take F;
  defpred P[Nat] means 0. < F.$1;
A7: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A8: 0. < F.k;
    F.(k+1) = (F.k)/2 by A6;
    hence thesis by A8;
  end;
A9: P[0] by A3,A6;
  thus
A10: for n being Nat holds P[n] from NAT_1:sch 2(A9,A7);
  then for n being Element of NAT holds 0. <= F.n;
  then
A11: F is nonnegative by SUPINF_2:39;
  for s being ExtReal holds s in rng Ser(F) implies s <= x0
  proof
    defpred P[Nat] means Ser(F).$1 + F.$1 < x0;
    let s be ExtReal;
    assume s in rng Ser(F);
    then consider n being object such that
A12: n in dom Ser(F) and
A13: s = Ser(F).n by FUNCT_1:def 3;
    reconsider n as Element of NAT by A12;
A14: for l being Nat st P[l] holds P[l+1]
    proof
      let l be Nat;
      F.(l+1) = (F.l)/2 by A6;
      then
A15:  Ser(F).l + (F.(l+1) + F.(l+1)) <= Ser(F).l + F.l by XXREAL_3:105;
      0. <= Ser(F).l & 0. <= F.(l+1) by A10,A11,SUPINF_2:40;
      then
A16:  Ser(F).(l+1) + F.(l+1) = (Ser(F).l + F.(l+1)) + F.(l+1) & Ser(F).l
      + F.(l+1) + F.(l+1) <= Ser(F).l + F.l by A15,SUPINF_2:def 11,
XXREAL_3:44;
      assume Ser(F).l + F.l < x0;
      hence thesis by A16,XXREAL_0:2;
    end;
A17: P[0] by A4,A6,SUPINF_2:def 11;
    for k being Nat holds P[k] from NAT_1:sch 2(A17,A14);
    then
A18: Ser(F).n + F.n < x0;
    0. <= Ser(F).n & 0. <= F.n by A10,A11,SUPINF_2:40;
    hence thesis by A13,A18,XXREAL_3:48;
  end;
  then x0 is UpperBound of rng Ser(F) by XXREAL_2:def 1;
  then
A19: sup(rng Ser(F)) <= x0 by XXREAL_2:def 3;
  per cases by A19,XXREAL_0:1;
  suppose
    SUM(F) < x0;
    hence thesis by A2,XXREAL_0:2;
  end;
  suppose
    SUM(F) = x0;
    hence thesis by A2;
  end;
end;

theorem
  for eps being ExtReal, X being non empty Subset of ExtREAL st
  0. < eps & inf X is Real holds
  ex x being ExtReal st x in X & x < inf X + eps
proof
  let eps be ExtReal;
  let X be non empty Subset of ExtREAL;
  assume that
A1: 0. < eps and
A2: inf X is Real;
A3: inf X in REAL by A2,XREAL_0:def 1;
  assume not ex x being ExtReal st x in X & x < inf X + eps;
  then inf X + eps is LowerBound of X by XXREAL_2:def 2;
  then
A4: inf X + eps <= inf X by XXREAL_2:def 4;
  per cases by XXREAL_0:4;
  suppose
    eps < +infty;
    then reconsider a = inf X, b = eps as Element of REAL by A1,A3,XXREAL_0:48;
    inf X + eps = a + b by SUPINF_2:1;
    then b <= a - a by A4,XREAL_1:19;
    hence thesis by A1;
  end;
  suppose
    eps = +infty;
    then inf X + eps = +infty by A3,XXREAL_3:def 2;
    hence thesis by A3,A4,XXREAL_0:4;
  end;
end;

theorem
  for eps being ExtReal, X being non empty Subset of ExtREAL st
  0. < eps & sup X is Real holds ex x being ExtReal st
  x in X & sup X - eps < x
proof
  let eps be ExtReal;
  let X be non empty Subset of ExtREAL;
  assume that
A1: 0. < eps and
A2: sup X is Real;
A3: sup X in REAL by A2,XREAL_0:def 1;
  assume not ex x being ExtReal st x in X & sup X - eps < x;
  then sup X - eps is UpperBound of X by XXREAL_2:def 1;
  then
A4: sup X <= sup X - eps by XXREAL_2:def 3;
  per cases by XXREAL_0:4;
  suppose
    eps < +infty;
    then reconsider a = sup X, b = eps as Element of REAL by A1,A3,XXREAL_0:48;
    a <= a - b by A4,SUPINF_2:3;
    hence thesis by A1,XREAL_1:44;
  end;
  suppose
    eps = +infty;
    then sup X - eps = -infty by A3,XXREAL_3:13;
    hence thesis by A3,A4,XXREAL_0:6;
  end;
end;

theorem
  for F being sequence of  ExtREAL st F is nonnegative & SUM(F) < +infty
    holds for n being Element of NAT holds F.n in REAL
proof
  let F be sequence of ExtREAL;
  assume that
A1: F is nonnegative and
A2: SUM(F) < +infty;
  let n be Element of NAT;
  defpred P[Nat] means F.$1 <= Ser(F).$1;
A3: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume F.k <= Ser(F).k;
    reconsider x = Ser(F).k as R_eal;
    x + F.(k+1) = Ser(F).(k+1) by SUPINF_2:def 11;
    hence thesis by A1,SUPINF_2:40,XXREAL_3:39;
  end;
A4: P[0] by SUPINF_2:def 11;
  for n being Nat holds P[n] from NAT_1:sch 2(A4,A3);
  then
A5: F.n <= Ser(F).n;
  Ser(F).n <= SUM(F) by FUNCT_2:4,XXREAL_2:4;
  then F.n <= SUM(F) by A5,XXREAL_0:2;
  then
A6: F.n < +infty by A2,XXREAL_0:2;
A7: 0 in REAL by XREAL_0:def 1;
  0. = 0 & 0. <= F.n by A1,SUPINF_2:39;
  hence thesis by A6,XXREAL_0:46,A7;
end;

:: PROPERTIES OF THE INTERVALS

registration
  cluster non empty interval for Subset of REAL;
  existence
  proof
    take [#]REAL;
    thus thesis;
  end;
end;

theorem
  for A being non empty Interval, a being ExtReal st
 ex b being ExtReal st a
  <= b & A = ].a,b.[ holds a = inf A by XXREAL_1:28,XXREAL_2:28;

theorem
  for A being non empty Interval, a being ExtReal st
   ex b being ExtReal st a
  <= b & A = ].a,b.] holds a = inf A by XXREAL_1:26,XXREAL_2:27;

theorem
  for A being non empty Interval, a being ExtReal
    st ex b being ExtReal st a <= b & A = [.a,b.]
 holds a = inf A by XXREAL_2:25;

theorem Th11:
  for A being non empty Interval, a being ExtReal st
   ex b being ExtReal st a <= b & A = [.a,b.[ holds a = inf A
proof
  let A be non empty Interval, IT be ExtReal;
  given b being ExtReal such that
A1: IT <= b and
A2: A = [.IT,b.[;
  IT <> b by A2;
  then IT < b by A1,XXREAL_0:1;
  hence thesis by A2,XXREAL_2:26;
end;

theorem
  for A being non empty Interval, b being ExtReal
   st ex a being ExtReal st a
  <= b & A = ].a,b.[ holds b = sup A by XXREAL_1:28,XXREAL_2:32;

theorem Th13:
  for A being non empty Interval, b being ExtReal st ex a being
  ExtReal st a <= b & A = ].a,b.] holds b = sup A
proof
  let A be non empty Interval, IT be ExtReal;
  given a being ExtReal such that
A1: a <= IT and
A2: A = ].a,IT.];
  a <> IT by A2;
  then a < IT by A1,XXREAL_0:1;
  hence thesis by A2,XXREAL_2:30;
end;

theorem
  for A being non empty Interval, b being ExtReal st
  ex a being ExtReal st a <= b & A = [.a,b.] holds b = sup A
   by XXREAL_2:29;

theorem Th15:
  for A being non empty Interval, b being ExtReal st
    ex a being ExtReal st a <= b & A = [.a,b.[ holds b = sup A
proof
  let A be non empty Interval, IT be ExtReal;
  given a being ExtReal such that
A1: a <= IT and
A2: A = [.a,IT.[;
  a <> IT by A2;
  then a < IT by A1,XXREAL_0:1;
  hence thesis by A2,XXREAL_2:31;
end;

theorem
  for A being non empty Interval st A is open_interval
     holds A = ].inf A,sup A.[
proof
  let A be non empty Interval;
  assume A is open_interval;
  then consider a,b being R_eal such that
A1: A = ].a,b.[ by MEASURE5:def 2;
  sup A = b by A1,XXREAL_1:28,XXREAL_2:32;
  hence thesis by A1,XXREAL_1:28,XXREAL_2:28;
end;

theorem
  for A being non empty Interval st A is closed_interval holds
    A = [.inf A,sup A.]
proof
  let A be non empty Interval;
  assume A is closed_interval;
  then consider a,b being Real such that
A1: A = [.a,b.] by MEASURE5:def 3;
A2: a <= b by A1,XXREAL_1:29;
  reconsider b as R_eal by XXREAL_0:def 1;
  sup A = b by A1,A2,XXREAL_2:29;
  hence thesis by A1,A2,XXREAL_2:25;
end;

theorem
  for A being non empty Interval st A is right_open_interval holds
  A = [.inf A,sup A.[
proof
  let A be non empty Interval;
  assume A is right_open_interval;
  then consider a being Real,b being R_eal such that
A1: A = [.a,b.[ by MEASURE5:def 4;
  reconsider a as R_eal by XXREAL_0:def 1;
A2: a <= b by A1,XXREAL_1:27;
  then sup A = b by A1,Th15;
  hence thesis by A1,A2,Th11;
end;

theorem
  for A being non empty Interval st A is left_open_interval holds
   A = ].inf A,sup A.]
proof
  let A be non empty Interval;
  assume A is left_open_interval;
  then consider a being R_eal,b being Real such that
A1: A = ].a,b.] by MEASURE5:def 5;
A2: a <= b by A1,XXREAL_1:26;
  reconsider b as R_eal by XXREAL_0:def 1;
  sup A = b by A2,A1,Th13;
  hence thesis by A1,XXREAL_1:26,XXREAL_2:27;
end;

theorem
  for A,B being non empty Interval, a,b being Real st
    a in A & b in B & sup A <= inf B holds a <= b
proof
  let A,B be non empty Interval, a,b be Real;
  assume that
A1: a in A and
A2: b in B;
A3: inf B <= b by A2,XXREAL_2:3;
  assume
A4: sup A <= inf B;
  a <= sup A by A1,XXREAL_2:4;
  then a <= inf B by A4,XXREAL_0:2;
  hence thesis by A3,XXREAL_0:2;
end;

theorem
  for A,B be real-membered set holds for y being Real holds y in B ++ A iff
    ex x,z being Real st x in B & z in A & y = x + z
  proof
    let A,B be real-membered set;
    let y be Real;
    hereby assume y in B++A; then
      consider x,w being Complex such that
A1:   y = x+w & x in B & w in A;
      reconsider x,w as Real by A1;
      take x,w;
      thus x in B & w in A & y = x + w by A1;
    end;
    given w,z being Real such that
A2: w in B & z in A & y = w + z;
    thus thesis by A2;
  end;

theorem
  for A,B being non empty Interval holds sup A = inf B &
  (sup A in A or inf B in B) implies A \/ B is Interval
by XXREAL_2:def 5,XXREAL_2:def 6,XXREAL_2:90,XXREAL_2:91;

definition
  let A be real-membered set;
  let x be Real;
  redefine func x ++ A -> Subset of REAL;
  coherence by MEMBERED:3;
end;

Lm1:
  for A be real-membered set, x be Real holds
  for y being Real holds y in x ++ A iff
    ex z being Real st z in A & y = x + z
  proof
    let A be real-membered set,
        x be Real;
    let y be Real;
    hereby assume y in x++A; then
      consider w being Complex such that
A1:   y = x+w & w in A by MEMBER_1:143;
      reconsider w as Real by A1;
      take w;
      thus w in A & y = x + w by A1;
    end;
    given z being Real such that
A2: z in A & y = x + z;
    thus thesis by A2,MEMBER_1:141;
  end;

theorem Th23:
  for A being Subset of REAL, x being Real holds -x ++ (x ++ A) = A
proof
  let A be Subset of REAL, x be Real;
  thus -x ++ (x ++ A) c= A
  proof
    let y be object;
    assume
A1: y in -x ++ (x ++ A);
    then reconsider y as Real;
    consider z being Real such that
A2: z in x ++ A and
A3: y = -x + z by A1,Lm1;
    ex t being Real st t in A & z = x + t by A2,Lm1;
    hence thesis by A3;
  end;
  let y be object;
  assume
A4: y in A;
  then reconsider y as Real;
  reconsider t = y - -x as Real;
  reconsider z = t -x as Real;
A5: z = -x + t;
  t in x ++ A by A4,Lm1;
  hence thesis by A5,Lm1;
end;

theorem
  for x being Real, A being Subset of REAL st A = REAL holds x ++ A = A
proof
  let x be Real, A be Subset of REAL;
  assume
A1: A = REAL;
  A c= x ++ A
  proof
    let y be object;
    assume y in A;
    then reconsider y as Real;
    reconsider z = y - x as Element of REAL by XREAL_0:def 1;
    y = x + z;
    hence thesis by A1,Lm1;
  end;
  hence thesis by A1;
end;

theorem
  for x being Real holds x ++ {} = {};

theorem Th26:
  for A being Interval, x being Real holds
    A is open_interval iff x ++ A is open_interval
proof
  let A be Interval, x be Real;
  reconsider y = -x as Element of REAL by XREAL_0:def 1;
A1: for B being Interval, y being Real st
    B is open_interval holds y ++ B is open_interval
  proof
    let B be Interval;
    let y be Real;
    reconsider y as Element of REAL by XREAL_0:def 1;
    reconsider z = y as R_eal by XXREAL_0:def 1;
    assume B is open_interval;
    then consider a,b being R_eal such that
A2: B = ].a,b.[ by MEASURE5:def 2;
    reconsider s = z + a, t = z + b as R_eal;
 y ++ B = ].s,t.[
    proof
      thus y ++ B c= ].s,t.[
      proof
        let c be object;
        assume
A3:     c in y ++ B;
        then reconsider c as Element of REAL;
        consider d being Real such that
A4:     d in B and
A5:     c = y + d by A3,Lm1;
        reconsider d1 = d as R_eal by XXREAL_0:def 1;
        a < d1 by A2,A4,MEASURE5:def 1; then
A6:     s < z + d1 by XXREAL_3:43;
        d1 < b by A2,A4,MEASURE5:def 1;
        then
A7:     z + d1 < t by XXREAL_3:43;
        z + d1 = c by A5,SUPINF_2:1;
        hence thesis by A6,A7;
      end;
      let c be object;
      assume
A8:  c in ].s,t.[;
      then reconsider c as Element of REAL;
      reconsider c1 = c as R_eal by XXREAL_0:def 1;
A9:  c = y + (c - y);
      c1 < z + b by A8,MEASURE5:def 1;
      then c1 - z < (b + z) - z by XXREAL_3:43;
      then
A10:  c1 - z < b by XXREAL_3:22;
      z + a < c1 by A8,MEASURE5:def 1;
      then (a + z) - z < c1 - z by XXREAL_3:43;
      then
A11:  a < c1 - z by XXREAL_3:22;
      c1 - z = c - y by SUPINF_2:3;
      then c - y in B by A2,A11,A10;
      hence thesis by A9,Lm1;
    end;
    hence thesis by MEASURE5:def 2;
  end;
  hence A is open_interval implies x ++ A is open_interval;
  assume
A12: x ++ A is open_interval;
  then reconsider B = x ++ A as Interval;
  y ++ B = A by Th23;
  hence thesis by A1,A12;
end;

theorem Th27:
  for A being Interval, x being Real holds
    A is closed_interval iff x ++ A is closed_interval
proof
  let A be Interval;
  let x be Real;
A1: for B being Interval, y being Real st B is closed_interval
    holds y ++ B is closed_interval
  proof
    let B be Interval;
    let y be Real;
    reconsider y as Real;
    reconsider z = y as R_eal by XXREAL_0:def 1;
    assume B is closed_interval;
    then consider a1,b1 being Real such that
A2: B = [.a1,b1.] by MEASURE5:def 3;
    reconsider a=a1,b=b1 as R_eal by XXREAL_0:def 1;
    reconsider s = z + a, t = z + b as R_eal;
 y ++ B = [.s,t.]
    proof
      thus y ++ B c= [.s,t.]
      proof
        let c be object;
        assume
A3:     c in y ++ B;
        then reconsider c as Real;
        consider d being Real such that
A4:     d in B and
A5:     c = y + d by A3,Lm1;
        reconsider d1 = d as R_eal by XXREAL_0:def 1;
        a <= d1 by A2,A4,XXREAL_1:1; then
A6:     s <= z + d1 by XXREAL_3:36;
        d1 <= b by A2,A4,XXREAL_1:1;
        then
A7:     z + d1 <= t by XXREAL_3:36;
        z + d1 = c by A5,SUPINF_2:1;
        hence thesis by A6,A7,XXREAL_1:1;
      end;
      reconsider a,b as R_eal;
      let c be object;
      assume
A8:  c in [.s,t.];
      then reconsider c as Real;
      reconsider c1 = c as R_eal by XXREAL_0:def 1;
A9:  c = y + (c - y);
      c1 <= z + b by A8,XXREAL_1:1;
      then c1 - z <= (b + z) - z by XXREAL_3:36;
      then
A10:  c1 - z <= b by XXREAL_3:22;
      z + a <= c1 by A8,XXREAL_1:1;
      then (a + z) - z <= c1 - z by XXREAL_3:36;
      then
A11:  a <= c1 - z by XXREAL_3:22;
      c1 - z = c - y by SUPINF_2:3;
      then c - y in B by A2,A11,A10;
      hence thesis by A9,Lm1;
    end;
    hence thesis by MEASURE5:def 3;
  end;
  x ++ A is closed_interval implies A is closed_interval
  proof
    reconsider y = -x as Real;
    assume
A12: x ++ A is closed_interval;
    then reconsider B = x ++ A as Interval;
    y ++ B = A by Th23;
    hence thesis by A1,A12;
  end;
  hence thesis by A1;
end;

theorem Th28:
  for A being Interval, x being Real holds
    A is right_open_interval iff x ++ A is right_open_interval
proof
  let A be Interval;
  let x be Real;
A1: for B being Interval, y being Real st
    B is right_open_interval holds y ++ B is right_open_interval
  proof
    let B be Interval;
    let y be Real;
    reconsider y as Element of REAL by XREAL_0:def 1;
    reconsider z = y as R_eal by XXREAL_0:def 1;
    assume B is right_open_interval;
    then consider a1 being Real,b being R_eal such that
A2: B = [.a1,b.[ by MEASURE5:def 4;
    reconsider a=a1 as R_eal by XXREAL_0:def 1;
    reconsider s = z + a, t = z + b as R_eal;
 y ++ B = [.s,t.[
    proof
      thus y ++ B c= [.s,t.[
      proof
        let c be object;
        assume
A3:     c in y ++ B;
        then reconsider c as Element of REAL;
        consider d being Real such that
A4:     d in B and
A5:     c = y + d by A3,Lm1;
        reconsider d1 = d as R_eal by XXREAL_0:def 1;
        a <= d1 by A2,A4,XXREAL_1:3;
        then
A6:     s <= z + d1 by XXREAL_3:36;
        d1 < b by A2,A4,XXREAL_1:3;
        then
A7:     z + d1 < t by XXREAL_3:43;
        z + d1 = c by A5,SUPINF_2:1;
        hence thesis by A6,A7,XXREAL_1:3;
      end;
      let c be object;
      assume
A8:  c in [.s,t.[;
      then reconsider c as Element of REAL by XREAL_0:def 1;
      reconsider c1 = c as R_eal by XXREAL_0:def 1;
A9:  c = y + (c - y);
      c1 < z + b by A8,XXREAL_1:3;
      then c1 - z < (b + z) - z by XXREAL_3:43;
      then
A10:  c1 - z < b by XXREAL_3:22;
      z + a <= c1 by A8,XXREAL_1:3;
      then (a + z) - z <= c1 - z by XXREAL_3:36;
      then
A11:  a <= c1 - z by XXREAL_3:22;
      c1 - z = c - y by SUPINF_2:3;
      then c - y in B by A2,A11,A10;
      hence thesis by A9,Lm1;
    end;
    hence thesis by MEASURE5:def 4;
  end;
  x ++ A is right_open_interval implies A is right_open_interval
  proof
    reconsider y = -x as Real;
    assume
A12: x ++ A is right_open_interval;
    then reconsider B = x ++ A as Interval;
    y ++ B = A by Th23;
    hence thesis by A1,A12;
  end;
  hence thesis by A1;
end;

theorem Th29:
  for A being Interval, x being Real holds
    A is left_open_interval iff x ++ A is left_open_interval
proof
  let A be Interval, x be Real;
A1: for B being Interval, y being Real st B is
  left_open_interval holds y ++ B is left_open_interval
  proof
    let B be Interval, y be Real;
    reconsider y as Element of REAL by XREAL_0:def 1;
    reconsider z = y as R_eal by XXREAL_0:def 1;
    assume B is left_open_interval;
    then consider a being R_eal,b1 being Real such that
A2: B = ].a,b1.] by MEASURE5:def 5;
    reconsider b = b1 as R_eal by XXREAL_0:def 1;
    set s = z + a, t = z + b;
    y ++ B = ].s,t.]
    proof
      thus y ++ B c= ].s,t.]
      proof
        let c be object;
        assume
A3:     c in y ++ B;
        then reconsider c as Element of REAL;
        consider d being Real such that
A4:     d in B and
A5:     c = y + d by A3,Lm1;
        reconsider d1 = d as R_eal by XXREAL_0:def 1;
        a < d1 by A2,A4,XXREAL_1:2;
        then
A6:     s < z + d1 by XXREAL_3:43;
        d1 <= b by A2,A4,XXREAL_1:2; then
A7:     z + d1 <= t by XXREAL_3:36;
        z + d1 = c by A5,SUPINF_2:1;
        hence thesis by A6,A7,XXREAL_1:2;
      end;
      let c be object;
      assume
A8:  c in ].s,t.];
      then reconsider c as Real;
      reconsider c1 = c as R_eal by XXREAL_0:def 1;
A9:  c = y + (c - y);
      c1 <= z + b by A8,XXREAL_1:2;
      then c1 - z <= (b + z) - z by XXREAL_3:36;
      then
A10:  c1 - z <= b by XXREAL_3:22;
      z + a < c1 by A8,XXREAL_1:2;
      then (a + z) - z < c1 - z by XXREAL_3:43;
      then
A11:  a < c1 - z by XXREAL_3:22;
      c1 - z = c - y by SUPINF_2:3;
      then c - y in B by A2,A11,A10;
      hence thesis by A9,Lm1;
    end;
    hence thesis by MEASURE5:def 5;
  end;
  x ++ A is left_open_interval implies A is left_open_interval
  proof
    reconsider y = -x as Real;
    assume
A12: x ++ A is left_open_interval;
    then reconsider B = x ++ A as Interval;
    y ++ B = A by Th23;
    hence thesis by A1,A12;
  end;
  hence thesis by A1;
end;

theorem
  for A being Interval, x being Real holds x ++ A is Interval
proof
  let A be Interval, x be Real;
  per cases by MEASURE5:1;
  suppose
    A is open_interval;
    then x ++ A is open_interval by Th26;
    hence thesis;
  end;
  suppose
    A is closed_interval;
    then x ++ A is closed_interval by Th27;
    hence thesis;
  end;
  suppose
    A is right_open_interval;
    then x ++ A is right_open_interval by Th28;
    hence thesis;
  end;
  suppose
    A is left_open_interval;
    then x ++ A is left_open_interval by Th29;
    hence thesis;
  end;
end;

theorem Th31:
  for A being real-membered set, x being Real,
      y being R_eal st x = y holds sup(x ++ A) = y + sup A
proof
  let A be real-membered set, x being Real, y being R_eal such that
A1: x = y;
A2: for z being UpperBound of x ++ A holds y + sup A <= z
  proof
    let z be UpperBound of x ++ A;
    reconsider zz = z as R_eal by XXREAL_0:def 1;
    zz - y is UpperBound of A
    proof
      let u be ExtReal;
      reconsider uu = u as R_eal by XXREAL_0:def 1;
      assume
A3:   u in A;
      then reconsider u1 = u as Real;
      y + uu = x + u1 by A1,XXREAL_3:def 2;
      then y + uu in x ++ A by A3,Lm1;
      then y + uu <= z by XXREAL_2:def 1;
      hence thesis by A1,XXREAL_3:45;
    end;
    then sup A <= zz - y by XXREAL_2:def 3;
    hence thesis by A1,XXREAL_3:45;
  end;
  y + sup A is UpperBound of x ++ A
  proof
    let z be ExtReal;
    assume z in x ++ A;
    then consider a being Real such that
A4: a in A and
A5: z = x + a by Lm1;
    reconsider b = a as R_eal by XXREAL_0:def 1;
A6: a <= sup A by A4,XXREAL_2:4;
    ex a,c being Complex st y = a & b = c & y + b = a + c by A1,
XXREAL_3:def 2;
    hence thesis by A1,A5,A6,XXREAL_3:36;
  end;
  hence thesis by A2,XXREAL_2:def 3;
end;

theorem Th32:
  for A being real-membered set, x being Real,
      y being R_eal st x = y holds inf(x ++ A) = y + inf A
proof
  let A be real-membered set, x being Real, y being R_eal such that
A1: x = y;
A2: for z being LowerBound of x ++ A holds z <= y + inf A
  proof
    let z be LowerBound of x ++ A;
    reconsider zz = z as R_eal by XXREAL_0:def 1;
    zz - y is LowerBound of A
    proof
      let u be ExtReal;
      reconsider uu = u as R_eal by XXREAL_0:def 1;
      assume
A3:   u in A;
      then reconsider u1 = u as Real;
      y + uu = x + u1 by A1,XXREAL_3:def 2;
      then y + uu in x ++ A by A3,Lm1;
      then z <= y + uu by XXREAL_2:def 2;
      hence thesis by A1,XXREAL_3:42;
    end;
    then zz - y <= inf A by XXREAL_2:def 4;
    hence thesis by A1,XXREAL_3:41;
  end;
  y + inf A is LowerBound of x ++ A
  proof
    let z be ExtReal;
    assume z in x ++ A;
    then consider a being Real such that
A4: a in A and
A5: z = x + a by Lm1;
    reconsider b = a as R_eal by XXREAL_0:def 1;
A6: inf A <= a by A4,XXREAL_2:3;
    ex a,c being Complex st y = a & b = c & y + b = a + c by A1,
XXREAL_3:def 2;
    hence thesis by A1,A5,A6,XXREAL_3:36;
  end;
  hence thesis by A2,XXREAL_2:def 4;
end;

theorem
  for A being Interval, x being Real holds
    diameter(A) = diameter(x ++ A)
proof
  let A be Interval, x be Real;
  per cases;
  suppose A is empty;
    hence thesis;
  end;
  suppose
A1: A is non empty;
    then consider y being Real such that
A2: y in A;
    reconsider y as Real;
A3: x + y in x ++ A by A2,Lm1;
    reconsider y = x as R_eal by XXREAL_0:def 1;
    thus diameter(A) = sup A - inf A by A1,MEASURE5:def 6
      .= y + sup A - (y + inf A) by XXREAL_3:33
      .= sup(x ++ A) - (y + inf A) by Th31
      .= sup(x ++ A) - inf(x ++ A) by Th32
      .= diameter(x ++ A) by A3,MEASURE5:def 6;
  end;
end;

begin :: from PSCOMP_1, 2010.02.26, A.T.

notation
  let X be set;
  synonym X is without_zero for X is with_non-empty_elements;
  antonym X is with_zero for X is with_non-empty_elements;
end;

definition
  let X be set;
  redefine attr X is without_zero means
  :Def1:
  not 0 in X;
  compatibility by SETFAM_1:def 8;
end;

registration
  cluster REAL -> with_zero;
  coherence by  XREAL_0:def 1;
  cluster NAT -> with_zero;
  coherence;
end;

registration
  cluster non empty without_zero for set;
  existence
  proof
    set s = {1};
    take s;
    thus s is non empty;
    thus thesis;
  end;
  cluster non empty with_zero for set;
  existence by Def1;
end;

registration
  cluster non empty without_zero for Subset of REAL;
  existence
  proof
    set s = {1 qua Real};
    take s;
    thus s is non empty;
    thus thesis;
  end;
  cluster non empty with_zero for Subset of REAL;
  existence
   proof take [#]REAL;
    thus thesis;
   end;
end;

theorem Th34:
  for F being set st
    F is non empty with_non-empty_elements c=-linear holds F is centered
proof
  defpred P[set] means $1 <> {} implies ex x being set st x in $1 &
  for y being set st y in $1 holds x c= y;
  let F be set;
  assume that
A1: F is non empty and
A2: F is with_non-empty_elements and
A3: F is c=-linear;
  thus F <> {} by A1;
  let G be set;
  assume that
A4: G <> {} and
A5: G c= F and
A6: G is finite;
A7: now
    let x, B be set;
    assume that
A8: x in G and
A9: B c= G and
A10: P[B];
    thus P[B \/ {x}]
    proof
      assume B \/ {x} <> {};
      per cases;
      suppose
A11:    B is empty;
        take x9 = x;
        thus x9 in B \/ {x} by A11,TARSKI:def 1;
        let y be set;
        thus thesis by A11,TARSKI:def 1;
      end;
      suppose
    B is non empty;
        then consider z being set such that
A12:    z in B and
A13:    for y being set st y in B holds z c= y by A10;
        thus ex x9 being set st x9 in B \/ {x} & for y being set st y in B \/
        {x} holds x9 c= y
        proof
          z in G by A9,A12; then
A14:      x, z are_c=-comparable by A3,A5,A8,ORDINAL1:def 8;
          per cases by A14;
          suppose
A15:        x c= z;
            take x9 = x;
            x9 in {x} by TARSKI:def 1;
            hence x9 in B \/ {x} by XBOOLE_0:def 3;
            let y be set;
            assume
A16:        y in B \/ {x};
            per cases by A16,XBOOLE_0:def 3;
            suppose
              y in B;
              then z c= y by A13;
              hence thesis by A15;
            end;
            suppose
              y in {x};
              hence thesis by TARSKI:def 1;
            end;
          end;
          suppose
A17:        z c= x;
            take x9 = z;
            thus x9 in B \/ {x} by A12,XBOOLE_0:def 3;
            let y be set;
            assume
A18:        y in B \/ {x};
            per cases by A18,XBOOLE_0:def 3;
            suppose
              y in B;
              hence thesis by A13;
            end;
            suppose
              y in {x};
              hence thesis by A17,TARSKI:def 1;
            end;
          end;
        end;
      end;
    end;
  end;
A19: P[{}];
  P[G] from FINSET_1:sch 2(A6, A19, A7);
  then consider x being set such that
A20: x in G and
A21: for y being set st y in G holds x c= y by A4;
  consider xe being object such that
A22: xe in x by A2,A5,A20,XBOOLE_0:def 1;
  now
    let y be set;
    assume y in G;
    then x c= y by A21;
    hence xe in y by A22;
  end;
  hence thesis by A4,SETFAM_1:def 1;
end;

registration
  let F be set;
  cluster non empty with_non-empty_elements c=-linear -> centered
    for Subset-Family of F;
  coherence by Th34;
end;

registration ::: FUNCT_2
  let X, Y be non empty set, f be Function of X, Y;
  cluster f.:X -> non empty;
  coherence
  proof
    set x = the Element of X;
A1: dom f = X by FUNCT_2:def 1;
    thus thesis by A1;
  end;
end;

definition ::: FUNCT_3
  let X, Y be set, f be Function of X, Y;
  func "f -> Function of bool Y, bool X means  :Def2:
  for y being Subset of Y holds it.y = f"y;
  existence
  proof
    deffunc F(Subset of Y) = f"$1;
    thus ex T be Function of bool Y, bool X st for y be Subset of Y holds T.y
    = F(y) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    deffunc F(Subset of Y) = f"$1;
    thus for T1,T2 be Function of bool Y, bool X st (for y being Subset of Y
holds T1.y = F(y)) & (for y being Subset of Y holds T2.y = F(y)) holds T1 = T2
    from BINOP_2:sch 1;
  end;
end;

theorem
  for X, Y, x being set, S being Subset-Family of Y, f being
  Function of X, Y st x in meet (("f).:S) holds f.x in meet S
proof
  let X, Y, x be set, S be Subset-Family of Y, f be Function of X, Y;
  assume
A1: x in meet (("f).:S);
A2: now
    let SS be set;
    assume
A3: SS in S;
    then ("f).SS in ("f).:S by FUNCT_2:35;
    then
A4: x in ("f).SS by A1,SETFAM_1:def 1;
    ("f).SS = f"SS by A3,Def2;
    hence f.x in SS by A4,FUNCT_1:def 7;
  end;
  ("f).:S is non empty by A1,SETFAM_1:def 1;
  then S is non empty;
  hence thesis by A2,SETFAM_1:def 1;
end;

reserve r, s, t for Real;

theorem Th36: ::: SQUARE_1 or ABSVALUE
  |.r.| + |.s.| = 0 implies r = 0
proof
  set aa = |.r.|, ab = |.s.|;
A1: 0 <= aa & 0 <= ab by COMPLEX1:46;
  assume |.r.|+|.s.| = 0;
  then aa = 0 by A1;
  hence thesis by ABSVALUE:2;
end;

theorem Th37: ::: SQUARE_1 or ABSVALUE
  r < s & s < t implies |.s.| < |.r.| + |.t.|
proof
  assume that
A1: r < s and
A2: s < t;
  per cases;
  suppose
A3: s<0;
    -s < -r by A1,XREAL_1:24; then
A4: -s+0 < -r+|.t.| by COMPLEX1:46,XREAL_1:8;
    -s = |.s.| by A3,ABSVALUE:def 1;
    hence thesis by A1,A3,A4,ABSVALUE:def 1;
  end;
  suppose
A5: 0<=s;
A6: s+0 < t+|.r.| by A2,COMPLEX1:46,XREAL_1:8;
    s = |.s.| by A5,ABSVALUE:def 1;
    hence thesis by A2,A5,A6,ABSVALUE:def 1;
  end;
end;

reserve seq for Real_Sequence,
  X, Y for Subset of REAL;

theorem Th38: ::: SEQ_2
  seq is convergent & seq is non-zero & lim seq = 0 implies seq" is non bounded
proof
  assume that
A1: seq is convergent and
A2: seq is non-zero and
A3: lim seq = 0;
  given r such that
A4: for n being Nat holds (seq").n<r;
  given s such that
A5: for n being Nat holds s<(seq").n;
  set aa = |.r.|, ab = |.s.|;
  set rab = 1/(aa+ab);
A6: 0 <= aa & 0 <= ab by COMPLEX1:46;
A7: now
    let n be Element of NAT;
    set g = seq.n, t = (seq").n;
    set At = |.t.|;
    t= 1/g by VALUED_1:10;
    then
A8: At = 1/|.g.| by ABSVALUE:7;
    t" = g " " by VALUED_1:10;
    then t <> 0 by A2,SEQ_1:5,XCMPLX_1:202; then
A9: 0 < At by COMPLEX1:47;
    s<t & t<r by A4,A5;
    then At < aa+ab by Th37;
    then At" > (aa+ab)" by A9,XREAL_1:88;
    hence |.seq.n.| > rab by A8;
  end;
A10: (seq").1<r by A4;
A11: s<(seq").1 by A5;
  now
    assume 0 >= aa+ab; then
A12: aa+ab = 0 by A6;
    then r = 0 by Th36;
    hence contradiction by A11,A10,A12,Th36;
  end;
  then consider n being Nat such that
A13: for m being Nat st n<=m holds |.seq.m-0 .|<rab by A1,A3,
SEQ_2:def 7;
A14: n in NAT by ORDINAL1:def 12;
  |.seq.n-0 .|<rab by A13;
  hence contradiction by A7,A14;
end;

theorem Th39: ::: SEQ_2
  rng seq is real-bounded iff seq is bounded
proof
  thus rng seq is real-bounded implies seq is bounded
  proof
    given s such that
A1: s is LowerBound of rng seq;
    given t such that
A2: t is UpperBound of rng seq;
    thus seq is bounded_above
    proof
      take t+1;
      let n be Nat;
A3:   n in NAT by ORDINAL1:def 12;
      seq.n <= t & t < t+1 by A2,FUNCT_2:4,XREAL_1:29,XXREAL_2:def 1,A3;
      hence thesis by XXREAL_0:2;
    end;
    take s-1;
    let n be Nat;
    s < s+1 by XREAL_1:29;
    then
A4: s-1 < s by XREAL_1:19;
A5:   n in NAT by ORDINAL1:def 12;
    seq.n >= s by A1,FUNCT_2:4,XXREAL_2:def 2,A5;
    hence thesis by A4,XXREAL_0:2;
  end;
  given t such that
A6: for n being Nat holds seq.n<t;
  given s such that
A7: for n being Nat holds seq.n>s;
  thus rng seq is bounded_below
  proof
    take s;
    let r be ExtReal;
    assume r in rng seq;
    then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
    hence thesis by A7;
  end;
  take t;
  let r be ExtReal;
  assume r in rng seq;
  then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
  hence thesis by A6;
end;

notation
  let X be real-membered set;
  synonym X is with_max for X is right_end;
  synonym X is with_min for X is left_end;
end;

definition
  let X be real-membered set;
  redefine attr X is with_max means
  X is bounded_above & upper_bound X in X;
  compatibility
  proof
   thus X is with_max implies X is bounded_above & upper_bound X in X
    proof assume
A1:    X is with_max;
     hence X is bounded_above;
      reconsider X as non empty bounded_above real-membered set by A1;
      upper_bound X in X by A1;
     hence thesis;
    end;
   assume
A2:   X is bounded_above & upper_bound X in X;
     then reconsider X as non empty bounded_above real-membered set;
    upper_bound X in X by A2;
   hence thesis;
  end;
  redefine attr X is with_min means
  X is bounded_below & lower_bound X in X;
 compatibility
  proof
   thus X is with_min implies X is bounded_below & lower_bound X in X
    proof assume
A3:  X is with_min;
     hence X is bounded_below;
      reconsider X as non empty bounded_below real-membered set by A3;
      lower_bound X in X by A3;
     hence thesis;
    end;
   assume
A4:   X is bounded_below & lower_bound X in X;
     then reconsider X as non empty bounded_below real-membered set;
    lower_bound X in X by A4;
   hence thesis;
  end;
end;

registration
  cluster non empty closed real-bounded for Subset of REAL;
  existence
  proof
    [. 0,0 .] = {0} by XXREAL_1:17;
    hence thesis;
  end;
end;

definition
  let R be Subset-Family of REAL;
  attr R is open means
  for X being Subset of REAL st X in R holds X is open;
  attr R is closed means

  for X being Subset of REAL st X in R holds X is closed;
end;

reserve r3, r1, q3, p3 for Real;

definition let X be Subset of REAL;
  redefine func --X -> Subset of REAL;
  coherence by MEMBERED:3;
end;

theorem
  r in X iff -r in --X by MEMBER_1:11;

Lm2: for X being Subset of REAL st X is bounded_above holds
  --X is bounded_below
proof
  let X be Subset of REAL;
  given s such that
A1: s is UpperBound of X;
  take -s;
  let t be ExtReal;
  assume t in --X;
  then consider r3 be Complex such that
A2: t = -r3 and
A3: r3 in X;
  reconsider r3 as Real by A3;
  r3 <= s by A1,A3,XXREAL_2:def 1;
  hence thesis by A2,XREAL_1:24;
end;

Lm3: for X being Subset of REAL st X is bounded_below holds --X is
bounded_above
proof
  let X be Subset of REAL;
  given s such that
A1: s is LowerBound of X;
  take -s;
  let t be ExtReal;
  assume t in --X;
  then consider r3 be Complex such that
A2: t = -r3 and
A3: r3 in X;
  reconsider r3 as Real by A3;
  r3 >= s by A1,A3,XXREAL_2:def 2;
  hence thesis by A2,XREAL_1:24;
end;

theorem Th41:
  X is bounded_above iff --X is bounded_below
proof
  X = -- --X;
  hence thesis by Lm2,Lm3;
end;

theorem
  X is bounded_below iff --X is bounded_above
proof
  X = -- --X;
  hence thesis by Th41;
end;

theorem Th43:
  for X being non empty Subset of REAL st X is bounded_below holds
  lower_bound X = - upper_bound --X
proof
  let X be non empty Subset of REAL;
  set r = - upper_bound --X;
A1: now
    let t;
    assume
A2: for s st s in X holds s >= t;
    now
      let s;
      assume s in --X;
      then -s in -- --X;
      then -s >= t by A2;
      then - -s <= -t by XREAL_1:24;
      hence s <= -t;
    end;
    then -r <= -t by SEQ_4:45;
    hence r >= t by XREAL_1:24;
  end;
  assume X is bounded_below;
  then
A3: --X is bounded_above by Lm3;
  now
    let s;
    assume s in X;
    then -s in --X;
    then -s <= -r by A3,SEQ_4:def 1;
    hence s >= r by XREAL_1:24;
  end;
  hence thesis by A1,SEQ_4:44;
end;

theorem Th44:
  for X being non empty Subset of REAL st X is bounded_above holds
  upper_bound X = - lower_bound --X
proof
  let X be non empty Subset of REAL;
  set r = - lower_bound --X;
A1: now
    let s;
    assume
A2: for t st t in X holds t <= s;
    now
      let t;
      assume t in --X;
      then -t in -- --X;
      then -t <= s by A2;
      then - -t >= -s by XREAL_1:24;
      hence t >= -s;
    end;
    then -r >= -s by SEQ_4:43;
    hence r <= s by XREAL_1:24;
  end;
  assume X is bounded_above;
  then
A3: --X is bounded_below by Lm2;
  now
    let t;
    assume t in X;
    then -t in --X;
    then -t >= -r by A3,SEQ_4:def 2;
    hence t <= r by XREAL_1:24;
  end;
  hence thesis by A1,SEQ_4:46;
end;

Lm4: for X being Subset of REAL st X is closed holds --X is closed
proof
  let X be Subset of REAL;
  assume
A1: X is closed;
  let s1 be Real_Sequence;
  assume that
A2: rng s1 c= --X and
A3: s1 is convergent;
A4: - lim s1 = lim -s1 by A3,SEQ_2:10;
A5: rng -s1 c= X
  proof
    let x be object;
    assume x in rng -s1;
    then consider n being object such that
A6: n in dom -s1 and
A7: x = (-s1).n by FUNCT_1:def 3;
    reconsider n as Element of NAT by A6;
A8: s1.n in rng s1 by FUNCT_2:4;
    x = -(s1.n) by A7,SEQ_1:10;
    then x in -- --X by A2,A8;
    hence thesis;
  end;
  -s1 is convergent by A3;
  then lim -s1 in X by A1,A5;
  then - -lim s1 in --X by A4;
  hence thesis;
end;

theorem
  X is closed iff --X is closed
proof
  ----X = X;
  hence thesis by Lm4;
end;

Lm5:
  for X be Subset of REAL, p be Real holds p++X = { p+r3 : r3 in X}
proof
  let X be Subset of REAL, p be Real;
  thus p++X c= { p+r3 : r3 in X }
  proof
    let x be object;
    assume
A1: x in p++X;
    then reconsider x9 = x as Real;
    ex z being Real st z in X & x9 = p + z by A1,Lm1;
    hence thesis;
  end;
  let x be object;
  assume x in { p+r3 : r3 in X };
  then ex r3 be Real st x = p + r3 & r3 in X;
  hence thesis by Lm1;
end;

theorem Th46:
  r in X iff q3+r in q3++X
proof
  thus r in X implies q3+r in q3++X by MEMBER_1:141;
  assume q3+r in q3++X; then
  q3+r in { q3 + r3 : r3 in X } by Lm5;
  then ex mr being Real st q3+r = q3+mr & mr in X;
  hence thesis;
end;

theorem
  X = 0++X by MEMBER_1:146;

theorem
  q3++(p3++X) = (q3+p3)++X by MEMBER_1:147;

Lm6: for X being Subset of REAL, s being Real st X is bounded_above
   holds s++X is bounded_above
proof
  let X be Subset of REAL, p be Real;
  given s such that
A1: s is UpperBound of X;
  take p+s;
  let t be ExtReal;
  assume t in p++X; then
  t in { p+r3 : r3 in X} by Lm5;
  then consider r3 such that
A2: t = p+r3 and
A3: r3 in X;
  r3 <= s by A1,A3,XXREAL_2:def 1;
  hence thesis by A2,XREAL_1:6;
end;

theorem
  X is bounded_above iff q3++X is bounded_above
proof
  -q3++(q3++X) = (-q3+q3)++X by MEMBER_1:147
    .= X by MEMBER_1:146;
  hence thesis by Lm6;
end;

Lm7: for X being Subset of REAL, p being Real st X is bounded_below
   holds p++X is bounded_below
proof
  let X be Subset of REAL, p be Real;
  given s such that
A1: s is LowerBound of X;
  take p+s;
  let t be ExtReal;
  assume t in p++X; then
  t in { p+r3 : r3 in X} by Lm5;
  then consider r3 such that
A2: t = p+r3 and
A3: r3 in X;
  r3 >= s by A1,A3,XXREAL_2:def 2;
  hence thesis by A2,XREAL_1:6;
end;

theorem
  X is bounded_below iff q3++X is bounded_below
proof
  -q3++(q3++X) = (-q3+q3)++X by MEMBER_1:147
    .= X by MEMBER_1:146;
  hence thesis by Lm7;
end;

theorem
  for X being non empty Subset of REAL st X is bounded_below
   holds lower_bound (q3++X) = q3+lower_bound X
proof
  let X be non empty Subset of REAL such that
A1: X is bounded_below;
  set i = q3+lower_bound X;
A2: now
    let t;
    assume
A3: for s st s in q3++X holds s >= t;
    now
      let s;
      assume s in X;
      then t <= q3+s by A3,MEMBER_1:141;
      hence t-q3 <= s by XREAL_1:20;
    end;
    then lower_bound X >= t-q3 by SEQ_4:43;
    hence t <= i by XREAL_1:20;
  end;
  now
    let s;
    assume s in q3++X; then
    s in { q3+r3 : r3 in X} by Lm5;
    then consider r3 such that
A4: q3+r3 = s and
A5: r3 in X;
    r3 >= lower_bound X by A1,A5,SEQ_4:def 2;
    hence s >= i by A4,XREAL_1:6;
  end;
  hence thesis by A2,SEQ_4:44;
end;

theorem
  for X being non empty Subset of REAL st X is bounded_above
  holds upper_bound (q3++X) = q3+upper_bound X
proof
  let X be non empty Subset of REAL such that
A1: X is bounded_above;
  set i = q3+upper_bound X;
A2: now
    let t;
    assume
A3: for s st s in q3++X holds s <= t;
    now
      let s;
      assume s in X;
      then q3+s <= t by A3,MEMBER_1:141;
      hence s <= t-q3 by XREAL_1:19;
    end;
    then upper_bound X <= t-q3 by SEQ_4:45;
    hence i <= t by XREAL_1:19;
  end;
  now
    let s;
    assume s in q3++X; then
    s in { q3+r3 : r3 in X} by Lm5;
    then consider r3 such that
A4: q3+r3 = s and
A5: r3 in X;
    r3 <= upper_bound X by A1,A5,SEQ_4:def 1;
    hence s <= i by A4,XREAL_1:6;
  end;
  hence thesis by A2,SEQ_4:46;
end;

Lm8: for X being Subset of REAL st X is closed holds q3++X is closed
proof
  let X be Subset of REAL;
  assume
A1: X is closed;
A2: q3++X = { q3+r3 : r3 in X} by Lm5;
  reconsider qq3=q3 as Element of REAL by XREAL_0:def 1;
  set s0 = seq_const q3;
  let s1 be Real_Sequence;
  assume that
A3: (rng s1) c= q3++X and
A4: s1 is convergent;
  lim (s1-s0) = (lim s1) - s0.0 by A4,SEQ_4:42
    .= (lim s1) - q3 by SEQ_1:57; then
A5: q3+lim(s1-s0) = lim s1;
A6: rng (s1-s0) c= X
  proof
    let x be object;
    assume
A7: x in rng (s1-s0);
    then consider n being object such that
A8: n in dom (s1-s0) and
A9: x = (s1-s0).n by FUNCT_1:def 3;
    reconsider x9 = x as Real by A7;
    reconsider n as Element of NAT by A8;
A10: s1.n in rng s1 by FUNCT_2:4;
    x = s1.n + (-s0).n by A9,SEQ_1:7
      .= s1.n + -(s0.n) by SEQ_1:10
      .= s1.n - q3 by SEQ_1:57;
    then x9+q3 in q3++X by A3,A10;
    hence thesis by Th46;
  end;
  s1-s0 is convergent by A4;
  then lim (s1-s0) in X by A1,A6;
  hence thesis by A5,A2;
end;

theorem
  X is closed iff q3++X is closed
proof
  -q3++(q3++X) = (-q3+q3)++X by MEMBER_1:147
    .= X by MEMBER_1:146;
  hence thesis by Lm8;
end;

definition
  let X be Subset of REAL;
  func Inv X -> Subset of REAL equals
  { 1/r3 : r3 in X };
  coherence
  proof set Y = { 1/r3 : r3 in X };
    Y c= REAL
    proof let e be object;
      assume e in Y;
      then ex r3 st e = 1/r3 & r3 in X;
      hence thesis by XREAL_0:def 1;
    end;
    hence thesis;
  end;
  involutiveness
  proof
    let Y,X be Subset of REAL;
    assume
A1: Y = { 1/r3 : r3 in X };
    thus X c= { 1/r3 : r3 in Y }
    proof
      let e be object;
      assume
A2:   e in X;
      then reconsider r=e as Element of REAL;
A3:   1/(1/r) = r;
      1/r in Y by A1,A2;
      hence thesis by A3;
    end;
    let e be object;
    assume e in { 1/r3 : r3 in Y };
    then consider r3 such that
A4: e = 1/r3 and
A5: r3 in Y;
    ex r1 st r3 = 1/r1 & r1 in X by A1,A5;
    hence thesis by A4;
  end;
end;

theorem Th54:
  for X being Subset of REAL holds r in X iff 1/r in Inv X
proof
  let X be Subset of REAL;
  thus r in X implies 1/r in Inv X;
  assume 1/r in Inv X;
  then ex mr being Real st 1/r = 1/mr & mr in X;
  hence thesis by XCMPLX_1:59;
end;

registration
  let X be non empty Subset of REAL;
  cluster Inv X -> non empty;
  coherence
  proof
    ex x being Element of REAL st x in X by SUBSET_1:4;
    hence thesis by Th54;
  end;
end;

registration
  let X be without_zero Subset of REAL;
  cluster Inv X -> without_zero;
  coherence
  proof
    now assume 0 in Inv X;
      then ex r3 st 0 = 1/r3 & r3 in X;
      hence contradiction;
    end;
    hence thesis;
  end;
end;

theorem
  for X being without_zero Subset of REAL st X is closed real-bounded
  holds Inv X is closed
proof
  let X be without_zero Subset of REAL;
  assume that
A1: X is closed and
A2: X is real-bounded;
  let s1 be Real_Sequence;
  assume that
A3: (rng s1) c= Inv X and
A4: s1 is convergent;
A5: rng (s1") c= X
  proof
    let x be object;
    assume x in rng (s1");
    then consider n being object such that
A6: n in dom (s1") and
A7: x = (s1").n by FUNCT_1:def 3;
    reconsider n as Element of NAT by A6;
    s1.n in rng s1 by FUNCT_2:4;
    then 1/(s1.n) in Inv Inv X by A3;
    hence thesis by A7,VALUED_1:10;
  end;
A8: not 0 in rng s1 by A3;
A9: now assume not s1 is non-zero;
    then consider n being Nat such that
A10:   s1.n = 0 by SEQ_1:5;
   n in NAT by ORDINAL1:def 12;
    hence contradiction by A8,FUNCT_2:4,A10;
  end;
A11: now
A12: rng (s1") c= X
    proof
      let y be object;
      assume y in rng (s1");
      then consider x being object such that
A13:  x in dom (s1") and
A14:  y = (s1").x by FUNCT_1:def 3;
      reconsider x as Element of NAT by A13;
      s1.x in rng s1 by FUNCT_2:4;
      then 1/(s1.x) in Inv Inv X by A3;
      hence thesis by A14,VALUED_1:10;
    end;
    assume lim s1 = 0;
    then s1" is non bounded by A4,A9,Th38;
    then rng (s1") is non real-bounded by Th39;
    hence contradiction by A2,A12,XXREAL_2:45;
  end;
  then s1" is convergent by A4,A9,SEQ_2:21;
  then lim s1" in X by A1,A5;
  then 1/lim s1 in X by A4,A9,A11,SEQ_2:22;
  then 1/(1/lim s1) in Inv X;
  hence thesis;
end;

theorem Th56:
  for Z being Subset-Family of REAL st Z is closed holds meet Z is closed
proof
  let Z be Subset-Family of REAL;
  assume
A1: Z is closed;
  let seq be Real_Sequence;
  set mZ = meet Z;
  assume that
A2: rng seq c= mZ and
A3: seq is convergent;
  per cases;
  suppose
    Z = {};
    then mZ = {} by SETFAM_1:def 1;
    hence thesis by A2;
  end;
  suppose
A4: Z <> {};
    now
      let X be set;
      assume
A5:   X in Z;
      then reconsider X9 = X as Subset of REAL;
A6:   rng seq c= X
      by A2,A5,SETFAM_1:def 1;
      X9 is closed by A1,A5;
      hence lim seq in X by A3,A6;
    end;
    hence thesis by A4,SETFAM_1:def 1;
  end;
end;

definition
  let X be real-membered set;
  func Cl X -> Subset of REAL equals
  meet { A where A is Subset of REAL : X c= A & A is closed };
  coherence
  proof
    defpred P[Subset of REAL] means X c= $1 & $1 is closed;
    reconsider Z = { A where A is Subset of REAL : P[A] } as Subset-Family of
    REAL from DOMAIN_1:sch 7;
    reconsider Z as Subset-Family of REAL;
    meet Z is Subset of REAL;
    hence thesis;
  end;
  projectivity
  proof
    reconsider W = [#]REAL as Subset of REAL;
    let IT be Subset of REAL, X be real-membered set;
    set ClX = { A where A is Subset of REAL : X c= A & A is closed },
    ClIT = { A where A is Subset of REAL : IT c= A & A is closed };
    assume
A1: IT = meet ClX;
    X c= W by MEMBERED:3; then
A2: W in ClX;
A3: W in ClIT;
    thus IT c= meet { A where A is Subset of REAL : IT c= A & A is closed }
    proof
      let e be object;
      assume
A4:   e in IT;
      for Y being set holds Y in ClIT implies e in Y
      proof
        let Y be set;
        assume Y in ClIT;
        then consider A being Subset of REAL such that
A5:     A = Y and
A6:     IT c= A and
A7:     A is closed;
        for Z being set st Z in ClX holds X c= Z
        proof
          let Z be set;
          assume Z in ClX;
          then ex B being Subset of REAL st Z = B & X c= B & B is closed;
          hence thesis;
        end;
        then X c= IT by A1,A2,SETFAM_1:5;
        then X c= A by A6;
        then A in ClX by A7;
        hence thesis by A1,A4,A5,SETFAM_1:def 1;
      end;
      hence thesis by A3,SETFAM_1:def 1;
    end;
    let e be object;
    assume
A8: e in meet ClIT;
    for Y being set holds Y in ClX implies e in Y
    proof
      let Y be set;
      assume
A9:   Y in ClX;
      then consider A being Subset of REAL such that
A10:  A = Y and
      X c= A and
A11:  A is closed;
      IT c= A by A1,A9,A10,SETFAM_1:3;
      then A in ClIT by A11;
      hence thesis by A8,A10,SETFAM_1:def 1;
    end;
    hence thesis by A1,A2,SETFAM_1:def 1;
  end;
end;

registration
  let X be real-membered set;
  cluster Cl X -> closed;
  coherence
  proof
    defpred P[Subset of REAL] means X c= $1 & $1 is closed;
    reconsider Z = { A where A is Subset of REAL : P[A] } as Subset-Family of
    REAL from DOMAIN_1:sch 7;
    reconsider Z as Subset-Family of REAL;
    Z is closed
    proof
      let Y be Subset of REAL;
      assume Y in Z;
      then ex A being Subset of REAL st Y = A & X c= A & A is closed;
      hence thesis;
    end;
    hence thesis by Th56;
  end;
end;

theorem Th57:
  for Y being closed Subset of REAL st X c= Y holds Cl X c= Y
proof
  let Y be closed Subset of REAL;
  set ClX = { A where A is Subset of REAL : X c= A & A is closed };
  assume X c= Y;
  then Y in ClX;
  hence thesis by SETFAM_1:3;
end;

theorem Th58:
  for X being real-membered set holds X c= Cl X
proof
  let X be real-membered set;
  let x be object;
  set ClX = { A where A is Subset of REAL : X c= A & A is closed };
  assume
A1: x in X;
A2: now
    let Y be set;
    assume Y in ClX;
    then ex YY being Subset of REAL st YY = Y & X c= YY & YY is closed;
    hence x in Y by A1;
  end;
  X c= [#]REAL by MEMBERED:3; then
  [#]REAL in ClX;
  hence thesis by A2,SETFAM_1:def 1;
end;

theorem Th59:
  X is closed iff X = Cl X
proof
  hereby
    set ClX = { A where A is Subset of REAL : X c= A & A is closed };
    assume X is closed;
    then X in ClX; then
A1: Cl X c= X by SETFAM_1:3;
    X c= Cl X by Th58;
    hence X = Cl X by A1;
  end;
  thus thesis;
end;

theorem
  Cl ({}REAL) = {} by Th59;

theorem
  Cl ([#]REAL) = REAL by Th59;

theorem
  for X, Y being real-membered set holds
  X c= Y implies Cl X c= Cl Y
proof
  let X, Y be real-membered set;
  assume
A1: X c= Y;
  set ClX = { A where A is Subset of REAL : X c= A & A is closed };
  Y c= Cl Y by Th58;
  then X c= Cl Y by A1;
  then Cl Y in ClX;
  hence thesis by SETFAM_1:3;
end;

theorem Th63:
  r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
  O /\ X is non empty
proof
  hereby
    assume
A1: r3 in Cl X;
    let O be open Subset of REAL such that
A2: r3 in O and
A3: O /\ X is empty;
    O misses X by A3; then
A4: X c= O` by SUBSET_1:23;
A5: O misses O` by SUBSET_1:24;
    O` is closed by RCOMP_1:def 5;
    then Cl X c= O` by A4,Th57;
    hence contradiction by A1,A2,A5,XBOOLE_0:3;
  end;
A6: (Cl X)` is open;
  X c= Cl X & (Cl X)` /\ X c= X by Th58,XBOOLE_1:17;
  then
A7: (Cl X)` /\ X c= Cl X;
  (Cl X)` /\ X c= (Cl X)` by XBOOLE_1:17; then
A8: (Cl X)` /\ X is empty by A7,SUBSET_1:20;
   reconsider rr3=r3 as Element of REAL by XREAL_0:def 1;
  assume for O being open Subset of REAL st r3 in O holds O /\ X is non empty;
  then not rr3 in (Cl X)` by A6,A8;
  hence thesis by SUBSET_1:29;
end;

theorem
  r3 in Cl X implies ex seq st rng seq c= X & seq is convergent & lim seq = r3
proof
  defpred P[object,object] means
  ex n being Nat st $1 = n & $2 = the Element of X/\].r3-1/(n+1),r3+1/(n+1).[;
  assume
A1: r3 in Cl X;
A2: now
    let x be object;
    assume x in NAT;
    then reconsider n = x as Element of NAT;
    set n1 = n+1;
    set oi = ].r3-1/n1,r3+1/n1.[;
    reconsider u = the Element of X/\oi as object;
    take u;
A3: r3 < r3+1/n1 by XREAL_1:29;
    then r3-1/n1 < r3 by XREAL_1:19;
    then r3 in oi by A3;
    then X/\oi is non empty by A1,Th63;
    then u in X/\oi;
    hence u in REAL;
    thus P[x,u];
  end;
  consider seq being Function such that
A4: dom seq = NAT & rng seq c= REAL and
A5: for x being object st x in NAT holds P[x,seq.x] from FUNCT_1:sch 6(A2);
  reconsider seq as Real_Sequence by A4,FUNCT_2:def 1,RELSET_1:4;
  take seq;
  thus rng seq c= X
  proof
    let y be object;
    assume y in rng seq;
    then consider x being object such that
A6: x in dom seq and
A7: seq.x = y by FUNCT_1:def 3;
    consider n being Nat such that
    x = n and
A8: seq.x = the Element of X/\].r3-1/(n+1),r3+1/(n+1).[ by A5,A6;
    reconsider n as Element of NAT by ORDINAL1:def 12;
    set n1 = n+1;
    set oi = ].r3-1/n1,r3+1/n1.[;
A9: r3 < r3+1/n1 by XREAL_1:29;
    then r3-1/n1 < r3 by XREAL_1:19;
    then r3 in oi by A9;
    then X/\oi is non empty by A1,Th63;
    hence thesis by A7,A8,XBOOLE_0:def 4;
  end;
A10: now
    let p be Real;
    set cp = [/ 1/p \];
A11: 1/p <= cp by INT_1:def 7;
    assume
A12: 0<p;
    then
A13: 0 < cp by INT_1:def 7;
    then reconsider cp as Element of NAT by INT_1:3;
    reconsider n = cp as Nat;
    take n;
    n < n+1 by NAT_1:13;
    then
A14: 1/(n+1) < 1/n by A13,XREAL_1:88;
    1/(1/p) >= 1/cp by A12,A11,XREAL_1:85; then
A15: 1/(n+1) < p by A14,XXREAL_0:2;
    let m be Nat;
    assume n<=m;
    then
A16: n+1 <= m+1 by XREAL_1:6;
    set m1 = m+1;
    1/m1 <= 1/(n+1) by A16,XREAL_1:85;
    then
A17: 1/m1 < p by A15,XXREAL_0:2;
    set oi = ].r3-1/m1,r3+1/m1.[;
A18: r3 < r3+1/m1 by XREAL_1:29;
    then r3-1/m1 < r3 by XREAL_1:19;
    then r3 in oi by A18;
    then
A19: X/\oi is non empty by A1,Th63;
    m in NAT by ORDINAL1:def 12;
    then ex m9 being Nat
   st m9 = m & seq.m = the Element of X/\].r3-1/(m9+ 1),r3+1/(m9+1).[ by A5;
    then seq.m in oi by A19,XBOOLE_0:def 4;
    then consider s such that
A20: seq.m = s and
A21: r3-1/m1 < s & s < r3+1/m1;
    -1/m1 < s-r3 & s-r3 < 1/m1 by A21,XREAL_1:19,20;
    then |.s-r3.| < 1/m1 by SEQ_2:1;
    hence |.seq.m-r3.|<p by A20,A17,XXREAL_0:2;
  end;
  hence seq is convergent;
  hence thesis by A10,SEQ_2:def 7;
end;

begin :: Functions into Reals

definition
  let X be set, f be Function of X, REAL;
  redefine attr f is bounded_below means
  f.:X is bounded_below;
  compatibility
  proof
A1: dom f = X by FUNCT_2:def 1;
    thus f is bounded_below implies f.:X is bounded_below
    proof
      given r such that
A2:   for y being object st y in dom f holds r<f.y;
      take r;
      let s be ExtReal;
      assume s in f.:X;
      then ex x being object st x in X & x in X & s = f.x by FUNCT_2:64;
      hence thesis by A1,A2;
    end;
    given p being Real such that
A3: p is LowerBound of f.:X;
    take p - 1;
    let y be object;
    assume y in dom f;
    then f.y in rng f by FUNCT_1:3;
    then f.y in f.:X by RELSET_1:22;
    then
A4: p <= f.y by A3,XXREAL_2:def 2;
    f.y < f.y + 1 by XREAL_1:29;
    then p < f.y + 1 by A4,XXREAL_0:2;
    hence thesis by XREAL_1:19;
  end;
  redefine attr f is bounded_above means
  f.:X is bounded_above;
  compatibility
  proof
A5: dom f = X by FUNCT_2:def 1;
    thus f is bounded_above implies f.:X is bounded_above
    proof
      given r such that
A6:   for y being object st y in dom f holds r>f.y;
      take r;
      let s be ExtReal;
      assume s in f.:X;
      then ex x being object st x in X & x in X & s = f.x by FUNCT_2:64;
      hence thesis by A5,A6;
    end;
    given p being Real such that
A7: p is UpperBound of f.:X;
    take p + 1;
    let y be object;
    assume y in dom f;
    then f.y in rng f by FUNCT_1:3;
    then f.y in f.:X by RELSET_1:22;
    then p >= f.y by A7,XXREAL_2:def 1;
    then
A8: p+1 >= f.y+1 by XREAL_1:6;
    f.y < f.y + 1 by XREAL_1:29;
    hence thesis by A8,XXREAL_0:2;
  end;
end;

definition
  let X be set, f be Function of X, REAL;
  attr f is with_max means
  f.:X is with_max;
  attr f is with_min means
  f.:X is with_min;
end;

theorem Th65:
  for X, A being set, f being Function of X, REAL holds (-f).:A = --(f.:A)
proof
  let X, A be set, f be Function of X, REAL;
  now
    let x be object;
    hereby
      assume x in (-f).:A;
      then consider x1 being object such that
A1:   x1 in X & x1 in A & x = (-f).x1 by FUNCT_2:64;
      x = -(f.x1) & f.x1 in f.:A by A1,FUNCT_2:35,VALUED_1:8;
      hence x in --(f.:A);
    end;
    assume x in --(f.:A); then
    consider r3 being Complex such that
A2: x = -r3 and
A3: r3 in f.:A;
    reconsider r3 as Real by A3;
    consider x1 being object such that
A4: x1 in X & x1 in A and
A5: r3 = f.x1 by A3,FUNCT_2:64;
    x = (-f).x1 by A2,A5,VALUED_1:8;
    hence x in (-f).:A by A4,FUNCT_2:35;
  end;
  hence thesis by TARSKI:2;
end;

Lm9: for X being non empty set, f being Function of X, REAL st f is with_max
holds -f is with_min
proof
  let X be non empty set, f be Function of X, REAL;
  assume that
A1: f.:X is bounded_above and
A2: upper_bound (f.:X) in f.:X;
A3: --(f.:X) = (-f).:X by Th65;
  hence (-f).:X is bounded_below by A1,Lm2;
  then
A4: lower_bound ((-f).:X) = - upper_bound -- --(f.:X) by A3,Th43
    .= - upper_bound (f.:X);
  - upper_bound (f.:X) in --(f.:X) by A2;
  hence thesis by A4,Th65;
end;

Lm10: for X being non empty set, f being Function of X, REAL st f is with_min
holds -f is with_max
proof
  let X be non empty set, f be Function of X, REAL;
  assume that
A1: f.:X is bounded_below and
A2: lower_bound (f.:X) in f.:X;
A3: --(f.:X) = (-f).:X by Th65;
  hence (-f).:X is bounded_above by A1,Lm3;
  then
A4: upper_bound ((-f).:X) = - lower_bound -- --(f.:X) by A3,Th44
    .= - lower_bound (f.:X);
  - lower_bound (f.:X) in --(f.:X) by A2;
  hence thesis by A4,Th65;
end;

theorem Th66:
  for X being non empty set, f being Function of X, REAL holds
  f is with_min iff -f is with_max
proof
  let X be non empty set, f be Function of X, REAL;
  - -f = f;
  hence thesis by Lm9,Lm10;
end;

theorem
  for X being non empty set, f being Function of X, REAL holds
  f is with_max iff -f is with_min
proof
  let X be non empty set, f be Function of X, REAL;
  - -f = f;
  hence thesis by Th66;
end;

theorem
  for X being set, A being Subset of REAL, f being Function of X, REAL
    holds (-f)"A = f"(--A)
proof
  let X be set, A be Subset of REAL, f be Function of X, REAL;
  now
    let x be object;
     reconsider xx=x as set by TARSKI:1;
    hereby
A1:   (-f).x = -(f.xx) by VALUED_1:8;
      assume
A2:   x in (-f)"A;
      then (-f).x in A by FUNCT_2:38;
      then - -f.xx in --A by A1;
      hence x in f"(--A) by A2,FUNCT_2:38;
    end;
A3: (-f).x = -(f.xx) by VALUED_1:8;
    assume
A4: x in f"(--A);
    then f.x in --A by FUNCT_2:38;
    then (-f).x in -- --A by A3;
    hence x in (-f)"A by A4,FUNCT_2:38;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  for X, A being set, f being Function of X, REAL, s being Real holds
    (s+f).:A = s++(f.:A)
proof
  let X, A be set, f be Function of X, REAL, s be Real;
  now
    let x be object;
    hereby
      assume x in (s+f).:A;
      then consider x1 being object such that
A1:   x1 in X & x1 in A & x = (s+f).x1 by FUNCT_2:64;
      x = s+(f.x1) & f.x1 in f.:A by A1,FUNCT_2:35,VALUED_1:2; then
      x in { s + q3 : q3 in f.:A };
      hence x in s++(f.:A) by Lm5;
    end;
    assume x in s++(f.:A); then
    x in { s + q3 : q3 in f.:A } by Lm5;
    then consider r3 such that
A2: x = s+r3 and
A3: r3 in f.:A;
    consider x1 being object such that
A4: x1 in X and
A5: x1 in A and
A6: r3 = f.x1 by A3,FUNCT_2:64;
    x = (s+f).x1 by A2,A4,A6,VALUED_1:2;
    hence x in (s+f).:A by A4,A5,FUNCT_2:35;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  for X being set, A being Subset of REAL,
      f being Function of X,REAL, q3 holds (q3+f)"A = f"(-q3++A)
proof
  let X be set, A be Subset of REAL, f be Function of X, REAL,
      q3 be Real;
  now
    let x be object;
     reconsider xx=x as set by TARSKI:1;
    hereby
      assume
A1:   x in (q3+f)"A;
      then (q3+f).x in A & (q3+f).x = q3+(f.xx) by FUNCT_2:38,VALUED_1:2;
      then -q3+(q3+(f.xx)) in { -q3 + p3 : p3 in A };
      then -q3+(q3+(f.xx)) in -q3++A by Lm5;
      hence x in f"(-q3++A) by A1,FUNCT_2:38;
    end;
    assume
A2: x in f"(-q3++A);
    then f.x in -q3++A & (q3+f).x = q3+(f.xx) by FUNCT_2:38,VALUED_1:2;
    then (q3+f).x in { q3+p3 : p3 in -q3 ++ A };
    then (q3+f).x in q3++(-q3++A) by Lm5;
    then (q3+f).x in (q3+-q3)++A by MEMBER_1:147;
    then (q3+f).x in A by MEMBER_1:146;
    hence x in (q3+f)"A by A2,FUNCT_2:38;
  end;
  hence thesis by TARSKI:2;
end;

notation
  let f be real-valued Function;
  synonym Inv f for f";
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  redefine func Inv f -> PartFunc of C,REAL;
  coherence
  proof
    f" is PartFunc of C,REAL;
    hence thesis;
  end;
end;

theorem
  for X being set, A being without_zero Subset of REAL,
      f being Function of X, REAL holds (Inv f)"A = f"(Inv A)
proof
  let X be set, A be without_zero Subset of REAL, f be Function of X, REAL;
  now
    let x be object;
     reconsider xx=x as set by TARSKI:1;
    hereby
A1:   (Inv f).x = (f.xx)" by VALUED_1:10;
      assume
A2:   x in (Inv f)"A;
      then (Inv f).x in A by FUNCT_2:38;
      then 1/((f.xx)") in Inv A by A1;
      hence x in f"(Inv A) by A2,FUNCT_2:38;
    end;
A3: (f.xx)" = 1/(f.xx) & (Inv f).x = (f.xx)" by VALUED_1:10;
    assume
A4: x in f"(Inv A);
    then f.x in Inv A by FUNCT_2:38;
    then (Inv f).x in Inv Inv A by A3;
    hence x in (Inv f)"A by A4,FUNCT_2:38;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  for A being Subset of REAL, x being Real st x in --A holds
    ex a being Real st a in A & x = -a
proof
  let A be Subset of REAL,
      x be Real;
  assume x in --A; then
  x in {-a where a is Complex: a in A}; then
  consider a being Complex such that
A1: x = -a & a in A;
  reconsider a as Real by A1;
  take a;
  thus thesis by A1;
end;