The Mizar article:

Infimum and Supremum of the Set of Real Numbers. Measure Theory

by
Jozef Bialas

Received September 27, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: SUPINF_1
[ MML identifier index ]


environ

 vocabulary BOOLE, ARYTM_3, SEQ_2, ARYTM, LATTICES, ORDINAL2, TARSKI, SUPINF_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
      REAL_1;
 constructors REAL_1, XREAL_0, MEMBERED, XBOOLE_0;
 clusters XREAL_0, SUBSET_1, XBOOLE_0, MEMBERED, ZFMISC_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0;
 theorems AXIOMS, TARSKI, ZFMISC_1, REAL_1, XREAL_0, XBOOLE_0, XBOOLE_1;
 schemes XBOOLE_0;

begin

::
:: -infty , +infty and ExtREAL enlarged set of real numbers
::

definition
   func +infty -> set equals
:Def1: REAL;
correctness;
end;

canceled;

theorem Th2:
   not +infty in REAL by Def1;

definition let IT be set;
  attr IT is +Inf-like means
:Def2:IT = +infty;
end;

definition
  cluster +Inf-like set;
existence proof take +infty; thus thesis by Def2; end;
end;

definition
   mode +Inf is +Inf-like set;
end;

canceled;

theorem
     +infty is +Inf by Def2;

definition
   func -infty -> set equals
:Def3: {REAL};
correctness;
end;

canceled;

theorem Th6:
   not -infty in REAL by Def3,TARSKI:def 1;

definition let IT be set;
   attr IT is -Inf-like means
:Def4:IT = -infty;
end;

definition
   cluster -Inf-like set;
existence proof take -infty; thus thesis by Def4; end;
end;

definition
   mode -Inf is -Inf-like set;
end;

canceled;

theorem
     -infty is -Inf by Def4;

definition let IT be set;
   attr IT is ext-real means
:Def5: IT in REAL \/ {-infty,+infty};
end;

definition
   cluster ext-real set;
existence
proof
   set x = -infty;
A1:   x in {-infty,+infty} by TARSKI:def 2;
   take x;
   thus x in REAL \/ {-infty,+infty} by A1,XBOOLE_0:def 2;
end;
end;

definition
   func ExtREAL -> set equals
:Def6: REAL \/ {-infty,+infty};
correctness;
end;

definition
  cluster -> ext-real Element of ExtREAL;
coherence by Def5,Def6;
end;

definition
   mode R_eal is Element of ExtREAL;
end;

definition
  cluster -> ext-real Real;
  coherence
  proof
    let r be Real;
      r in REAL \/ {-infty,+infty} by XBOOLE_0:def 2;
    hence thesis by Def5;
  end;
end;

canceled;

theorem
     for x being Real holds x is R_eal by Def5,Def6;

theorem Th11:
   for x being set holds
   x = -infty or x = +infty implies x is R_eal
proof
   let x be set;
   assume x = -infty or x = +infty;
   then x in {-infty,+infty} by TARSKI:def 2;
   hence thesis by Def6,XBOOLE_0:def 2;
end;

definition
   redefine func +infty -> R_eal;
coherence by Th11;
   redefine func -infty -> R_eal;
coherence by Th11;
end;

canceled 2;

theorem Th14:
   -infty <> +infty
proof
   assume A1: -infty = +infty;
   consider x being Element of REAL;
A2: x = REAL by A1,Def1,Def3,TARSKI:def 1;
     for X,Y be set holds not ( X in Y & Y in X);
   hence thesis by A2;
end;

::
::       Relations " <=' "," < " in the set of r_eal numbers
::

Lm1:
 for x being R_eal holds
  x in REAL or x = +infty or x = -infty
proof let x be R_eal;
    x in REAL or x in {-infty,+infty} by Def6,XBOOLE_0:def 2;
 hence x in REAL or x = +infty or x = -infty by TARSKI:def 2;
end;

definition
   let x,y be R_eal;
   pred x <=' y means
:Def7: ex p,q being Real st p = x & q = y & p <= q if x in REAL & y in REAL
    otherwise x = -infty or y = +infty;
  consistency;
  reflexivity by Lm1;
  connectedness
   proof let x,y be R_eal;
    assume
A1:     not(x in REAL & y in REAL implies
       ex p,q being Real st p = x & q = y & p <= q) or
       not (not(x in REAL & y in REAL) implies x = -infty or y = +infty);
    per cases by A1;
    suppose that
A2:  x in REAL & y in REAL and
A3:  not ex p,q being Real st p = x & q = y & p <= q;
    thus y in REAL & x in REAL implies
       ex p,q being Real st p = y & q = x & p <= q
     proof assume y in REAL & x in REAL;
       then reconsider a = x, b = y as Real;
      take b,a;
      thus thesis by A3;
     end;
    thus thesis by A2;
    suppose not(x in REAL & y in REAL) & not(x = -infty or y = +infty);
    hence thesis by Lm1;
   end;
  antonym y <' x;
end;

canceled;

theorem
     for x,y being R_eal holds
   ((x is Real & y is Real) implies
   (x <=' y iff ex p,q being Real st (p = x & q = y & p <= q)))
      by Def7;

theorem Th17:
   for x being R_eal holds (x in REAL implies not (x <=' -infty))
      by Def7,Th6,Th14;

theorem Th18:
   for x being R_eal holds x in REAL implies not +infty <=' x
     by Def7,Th2,Th14;

theorem
     not +infty <=' -infty by Def7,Th2,Th14;

theorem
     for x being R_eal holds x <=' +infty by Def7,Th2;

theorem
     for x being R_eal holds -infty <=' x by Def7,Th6;

theorem Th22:
   for x,y being R_eal holds x <=' y & y <=' x implies x = y
proof
   let x,y be R_eal;
   assume that
A1:x <=' y and
A2:y <=' x;
     x in (REAL \/ {-infty,+infty}) & y in (REAL \/ {-infty,+infty}) by Def5;
   then (x in REAL or x in {-infty,+infty}) & (y in REAL or y in {-infty,
+infty
}) by XBOOLE_0:def 2;
   then A3:(x in REAL & y in REAL) or (x in REAL & y = -infty) or (x in
 REAL & y = +infty
) or
   (x = -infty & y in REAL) or (x = -infty & y = -infty) or (x = -infty & y =
+infty) or
   (x = +infty & y in REAL) or (x = +infty & y = -infty) or (x = +infty & y =
+infty) by TARSKI:def 2;
  (x in REAL & y in REAL) implies x = y
   proof
      assume
   A4:x in REAL & y in REAL;
 then A5: ex p0,q0 being Real st x = p0 & y = q0 & p0 <= q0 by A1,Def7;
         ex p1,q1 being Real st y = p1 & x = q1 & p1 <= q1 by A2,A4,Def7;
      hence thesis by A5,AXIOMS:21;
   end;
    hence thesis by A1,A2,A3,Def7,Th14;
end;

theorem
     for x being R_eal holds
   x <=' -infty implies x = -infty
proof
   let x be R_eal;
   assume
A1:x <=' -infty;
     -infty <=' x by Def7,Th6;
   hence thesis by A1,Th22;
end;

theorem Th24:
   for x being R_eal holds
   +infty <=' x implies x = +infty
proof
   let x be R_eal;
   assume
A1:+infty <=' x;
     x <=' +infty by Def7,Th2;
   hence thesis by A1,Th22;
end;

scheme SepR_eal { P[R_eal]}:
   ex X being Subset of REAL \/ {-infty,+infty} st
   for x being R_eal holds x in X iff P[x]
proof defpred Q[set] means ex x being R_eal st x=$1 & P[x];
   consider X being set such that
A1:for r being set holds r in X iff r in REAL \/ {-infty,+infty} & Q[r]
        from Separation;
     X c= REAL \/ {-infty,+infty}
   proof
      let r be set;
      assume r in X;
      hence thesis by A1;
   end;
   then reconsider X as Subset of REAL \/ {-infty,+infty};
   take X;
   let x be R_eal;
   hereby assume x in X;
      then ex y being R_eal st y = x & P[y] by A1;
      hence P[x];
   end;
   assume A2: P[x];
     x in REAL \/ {-infty,+infty} by Def5;
   hence thesis by A1,A2;
end;

canceled;

theorem
     ExtREAL is non empty set by Def6;

theorem
     for x being set holds
   x is R_eal iff x in ExtREAL by Def6;

canceled;

theorem Th29:
   for x,y,z being R_eal holds ((x <=' y & y <=' z) implies x <=' z)
proof
   let x,y,z be R_eal;
   assume that
A1:x <=' y and
A2:y <=' z;
A3:x in (REAL \/ {-infty,+infty}) & y in (REAL \/ {-infty,+infty}) & z in
 (REAL \/ {
-infty,+infty}) by Def5;
A4:(x in REAL & y in REAL & z in REAL) implies x <=' z
   proof
       assume
   A5: x in REAL & y in REAL & z in REAL;
       then consider p0,q0 being Real such that
   A6: x = p0 & y = q0 & p0 <= q0 by A1,Def7;
       consider p1,q1 being Real such that
   A7: y = p1 & z = q1 & p1 <= q1 by A2,A5,Def7;
         p0 <= q1 by A6,A7,AXIOMS:22;
       hence thesis by A6,A7,Def7;
   end;
A8:(x in {-infty,+infty} & y in REAL & z in REAL) implies x <=' z
   proof
       assume x in {-infty,+infty} & y in REAL & z in REAL;
   then ((x = +infty) & y in REAL & z in REAL) or
       ((x = -infty) & y in REAL & z in REAL) by TARSKI:def 2;
       hence thesis by A1,A2,Def7,Th6,Th24;
   end;
A9:(x in REAL & y in {-infty,+infty} & z in REAL) implies x <=' z
   proof
       assume x in REAL & y in {-infty,+infty} & z in REAL;
   then A10: x in REAL & (y = -infty) & z in REAL or x in REAL & (y = +infty
) & z in REAL
       by TARSKI:def 2;
         x in REAL & (y = +infty) & z in REAL implies x <=' z by A2,Th2,Th24;
       hence thesis by A1,A10,Def7,Th6;
   end;
A11:(x in {-infty,+infty} & y in {-infty,+infty} & z in REAL) implies x <=' z
   proof
       assume x in {-infty,+infty} & y in {-infty,+infty} & z in REAL;
   then (x = -infty) & (y = -infty) & z in REAL or
       (x = -infty) & (y = +infty) & z in REAL or
       (x = +infty) & (y = -infty) & z in REAL or
       (x = +infty) & (y = +infty) & z in REAL by TARSKI:def 2;
       hence thesis by A1,A2,Def7,Th2;
   end;
A12:(x in REAL & y in REAL & z in {-infty,+infty}) implies x <=' z
   proof
       assume x in REAL & y in REAL & z in {-infty,+infty};
   then x in REAL & y in REAL & z = -infty or x in REAL & y in
 REAL & z = +infty
       by TARSKI:def 2;
       hence thesis by A2,Def7,Th2,Th6,Th14;
   end;
A13:(x in {-infty,+infty} & y in REAL & z in {-infty,+infty}) implies x <=' z
   proof
       assume x in {-infty,+infty} & y in REAL & z in {-infty,+infty};
   then (x = -infty) & y in REAL & (z = -infty) or
       (x = -infty) & y in REAL & (z = +infty) or
       (x = +infty) & y in REAL & (z = -infty) or
       (x = +infty) & y in REAL & (z = +infty) by TARSKI:def 2;
       hence thesis by A2,Def7,Th6;
   end;
A14:(x in REAL & y in {-infty,+infty} & z in {-infty,+infty}) implies x <=' z
   proof
       assume
     x in REAL & y in {-infty,+infty} & z in {-infty,+infty};
   then x in REAL & (y = -infty) & (z = -infty) or
       x in REAL & (y = -infty) & (z = +infty) or
       x in REAL & (y = +infty) & (z = -infty) or
       x in REAL & (y = +infty) & (z = +infty) by TARSKI:def 2;
       hence thesis by A1,A2,Def7,Th2;
   end;
  (x in {-infty,+infty} & y in {-infty,+infty} & z in {-infty,+infty
}) implies x <=' z
   proof
       assume x in {-infty,+infty} & y in {-infty,+infty} & z in
 {-infty,+infty};
   then (x = +infty) & (y = -infty) & (z = -infty) or
       (x = +infty) & (y = -infty) & (z = +infty) or
       (x = +infty) & (y = +infty) & (z = -infty) or
       (x = +infty) & (y = +infty) & (z = +infty) or
       (x = -infty) & (y = -infty) & (z = -infty) or
       (x = -infty) & (y = -infty) & (z = +infty) or
       (x = -infty) & (y = +infty) & (z = -infty) or
       (x = -infty) & (y = +infty) & (z = +infty) by TARSKI:def 2;
       hence thesis by A1,A2;
   end;
   hence thesis by A3,A4,A8,A9,A11,A12,A13,A14,XBOOLE_0:def 2;
end;

definition
   cluster ExtREAL -> non empty;
coherence by Def6;
end;

canceled;

theorem
     for x being R_eal holds
   x in REAL implies -infty <' x & x <' +infty
proof
   let x be R_eal;
   assume
A1:x in REAL;
  -infty <=' x by Def7,Th6;
   hence -infty <' x by A1,Th6,Th22;
     x <=' +infty by Def7,Th2;
   hence thesis by A1,Th2,Th22;
end;

::
::       Majorant and minorant element of X being SUBDOMAIN of ExtREAL
::

definition
   let X be non empty Subset of ExtREAL;
 canceled;

   mode majorant of X -> R_eal means
:Def9:for x be R_eal holds x in X implies x <=' it;
existence
proof
   take +infty;
   thus thesis by Def7,Th2;
end;
end;

canceled;

theorem Th33:
   for X being non empty Subset of ExtREAL holds
   +infty is majorant of X
proof
   let X be non empty Subset of ExtREAL;
     for x being R_eal holds x in X implies x <=' +infty by Def7,Th2;
   hence thesis by Def9;
end;

theorem Th34:
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   (for UB being R_eal holds UB is majorant of Y implies UB is majorant of X)
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
   let UB be R_eal;
   assume UB is majorant of Y;
   then for x be R_eal st x in X holds x <=' UB by A1,Def9;
   hence thesis by Def9;
end;

definition
   let X be non empty Subset of ExtREAL;
   mode minorant of X -> R_eal means
:Def10:for x be R_eal holds x in X implies it <=' x;
existence
proof
   take -infty;
   thus thesis by Def7,Th6;
end;
end;

canceled;

theorem Th36:
   for X being non empty Subset of ExtREAL holds
   -infty is minorant of X
proof
   let X be non empty Subset of ExtREAL;
     for x being R_eal st x in X holds -infty <=' x by Def7,Th6;
   hence thesis by Def10;
end;

canceled 2;

theorem Th39:
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   (for LB being R_eal holds LB is minorant of Y implies LB is minorant of X)
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
   let LB be R_eal;
   assume LB is minorant of Y;
   then for x be R_eal st x in X holds LB <=' x by A1,Def10;
   hence thesis by Def10;
end;

definition
   redefine func REAL -> non empty Subset of ExtREAL;
coherence by Def6,XBOOLE_1:7;
end;

canceled;

theorem
     +infty is majorant of REAL by Th33;

theorem
     -infty is minorant of REAL by Th36;

::
::       Bounded above, bounded below and bounded sets of r_eal numbers
::

definition
   let X be non empty Subset of ExtREAL;
   attr X is bounded_above means
:Def11: ex UB being majorant of X st UB in REAL;
end;

canceled;

theorem Th44:
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies (Y is bounded_above implies X is bounded_above)
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
   assume Y is bounded_above;
then ex UB being majorant of Y st UB in REAL by Def11;
      then consider UB being R_eal such that
   A2:UB is majorant of Y & UB in REAL;
        UB is majorant of X & UB in REAL by A1,A2,Th34;
   hence thesis by Def11;
end;

theorem
     not REAL is bounded_above
proof
     for X being non empty Subset of ExtREAL holds
   X = REAL implies not X is bounded_above
   proof
      let X be non empty Subset of ExtREAL;
      assume
   A1:X = REAL;
      assume X is bounded_above;
      then consider UB being majorant of X such that
   A2:UB in REAL by Def11;
      reconsider UB as Real by A2;
      consider x being real number such that
   A3:UB < x by REAL_1:76;
      reconsider x as Real by XREAL_0:def 1;
      reconsider x as R_eal by Def5,Def6;
      reconsider UB as R_eal;
   A4:x <=' UB by A1,Def9;
      consider a,b being R_eal such that
   A5:a = UB & b = x;
        a <=' b by A3,A5,Def7;
      hence thesis by A3,A4,A5,Th22;
   end;
   hence thesis;
end;

definition
   let X be non empty Subset of ExtREAL;
   attr X is bounded_below means
:Def12: ex LB being minorant of X st LB in REAL;
end;

canceled;

theorem Th47:
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies (Y is bounded_below implies X is bounded_below)
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
   assume Y is bounded_below;
then ex LB being minorant of Y st LB in REAL by Def12;
   then consider LB being R_eal such that
A2:LB is minorant of Y & LB in REAL;
     LB is minorant of X & LB in REAL by A1,A2,Th39;
   hence thesis by Def12;
end;

theorem
     not REAL is bounded_below
proof
     for X being non empty Subset of ExtREAL holds
   X = REAL implies not X is bounded_below
   proof
      let X be non empty Subset of ExtREAL;
      assume
   A1:X = REAL;
      assume X is bounded_below;
      then consider LB being minorant of X such that
   A2:LB in REAL by Def12;
      reconsider LB as Real by A2;
      consider x being real number such that
   A3:x < LB by REAL_1:77;
      reconsider x as Real by XREAL_0:def 1;
      reconsider x as R_eal by Def5,Def6;
      reconsider LB as R_eal;
   A4:LB <=' x by A1,Def10;
      consider a,b being R_eal such that
   A5:a = x & b = LB;
        a <=' b by A3,A5,Def7;
      hence thesis by A3,A4,A5,Th22;
   end;
   hence thesis;
end;

definition
   let X be non empty Subset of ExtREAL;
   attr X is bounded means
:Def13:X is bounded_above bounded_below;
end;

canceled;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies (Y is bounded implies X is bounded)
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
   assume Y is bounded;
   then Y is bounded_above & Y is bounded_below by Def13;
   then X is bounded_above & X is bounded_below by A1,Th44,Th47;
   hence thesis by Def13;
end;

theorem Th51:
   for X being non empty Subset of ExtREAL holds
   ex Y being non empty Subset of ExtREAL st
   for x being R_eal holds x in Y iff x is majorant of X
proof
   let X be non empty Subset of ExtREAL;
    defpred P[R_eal] means $1 is majorant of X;
     ex Y being Subset of REAL \/ {-infty,+infty} st
   for x being R_eal holds x in Y iff P[x] from SepR_eal;
   then consider Y being Subset of REAL \/ {-infty,+infty} such that
A1:for x being R_eal holds x in Y iff x is majorant of X;
     +infty is majorant of X by Th33;
   then reconsider Y as non empty set by A1;
   reconsider Y as non empty Subset of ExtREAL by Def6;
   take Y;
   thus thesis by A1;
end;

::
::       Set of majorant and set of minorant of X being SUBDOMAIN of ExtREAL
::

definition
   let X be non empty Subset of ExtREAL;
   func SetMajorant(X) -> Subset of ExtREAL means
:Def14: for x being R_eal holds x in it iff x is majorant of X;
existence
  proof
   consider Y being non empty Subset of ExtREAL such that
A1:   for x being R_eal holds x in Y iff x is majorant of X by Th51;
  take Y;
  thus thesis by A1;
  end;
uniqueness
proof
   let Y1,Y2 be Subset of ExtREAL such that
A2:for x being R_eal holds
   x in Y1 iff x is majorant of X and
A3:for x being R_eal holds
   x in Y2 iff x is majorant of X;
A4:for x being R_eal holds x in Y1 iff x in Y2
   proof
      let x be R_eal;
        x in Y1 iff x is majorant of X by A2;
      hence thesis by A3;
   end;
   thus Y1 c= Y2
   proof
        for x being set holds x in Y1 implies x in Y2 by A4;
      hence thesis by TARSKI:def 3;
   end;
   thus Y2 c= Y1
   proof
        for x being set holds x in Y2 implies x in Y1 by A4;
      hence thesis by TARSKI:def 3;
   end;
end;
end;

definition
   let X be non empty Subset of ExtREAL;
   cluster SetMajorant(X) -> non empty;
   coherence
   proof
      consider x being majorant of X;
        x in SetMajorant(X) by Def14;
      hence thesis;
   end;
end;

canceled 2;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   for x being R_eal holds (x in SetMajorant(Y) implies x in SetMajorant(X))
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
   let x be R_eal;
   assume x in SetMajorant(Y);
   then x is majorant of Y by Def14;
   then x is majorant of X by A1,Th34;
   hence thesis by Def14;
end;

theorem Th55:
   for X being non empty Subset of ExtREAL holds
   ex Y being non empty Subset of ExtREAL st
   for x being R_eal holds x in Y iff x is minorant of X
proof
   let X be non empty Subset of ExtREAL;
    defpred P[R_eal] means $1 is minorant of X;
     ex Y being Subset of REAL \/ {-infty,+infty} st
   for x being R_eal holds x in Y iff P[x] from SepR_eal;
   then consider Y being Subset of REAL \/ {-infty,+infty} such that
A1:for x being R_eal holds x in Y iff x is minorant of X;
     -infty is minorant of X by Th36;
   then reconsider Y as non empty set by A1;
   reconsider Y as non empty Subset of ExtREAL by Def6;
   take Y;
   thus thesis by A1;
end;

definition
   let X be non empty Subset of ExtREAL;
   func SetMinorant(X) -> Subset of ExtREAL means
:Def15: for x being R_eal holds x in it iff x is minorant of X;
existence
 proof
  consider Y being non empty Subset of ExtREAL such that
A1:  for x being R_eal holds x in Y iff x is minorant of X by Th55;
  take Y;
  thus thesis by A1;
 end;
uniqueness
proof
   let Y1,Y2 be Subset of ExtREAL such that
A2:for x being R_eal holds
   x in Y1 iff x is minorant of X and
A3:for x being R_eal holds
   x in Y2 iff x is minorant of X;
A4:for x being R_eal holds x in Y1 iff x in Y2
   proof
      let x be R_eal;
     x in Y1 iff x is minorant of X by A2;
      hence thesis by A3;
   end;
   thus Y1 c= Y2
   proof
        for x being set holds x in Y1 implies x in Y2 by A4;
      hence thesis by TARSKI:def 3;
   end;
   thus Y2 c= Y1
   proof
        for x being set holds x in Y2 implies x in Y1 by A4;
      hence thesis by TARSKI:def 3;
   end;
end;
end;

definition
   let X be non empty Subset of ExtREAL;
   cluster SetMinorant(X) -> non empty;
   coherence
   proof
      consider x being minorant of X;
        x in SetMinorant(X) by Def15;
      hence thesis;
   end;
end;

canceled 2;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies
   for x being R_eal holds (x in SetMinorant(Y) implies x in SetMinorant(X))
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
   let x be R_eal;
   assume x in SetMinorant(Y);
   then x is minorant of Y by Def15;
   then x is minorant of X by A1,Th39;
   hence thesis by Def15;
end;

theorem Th59:
   for X being non empty Subset of ExtREAL holds
   X is bounded_above & not X = {-infty} implies
   ex x being Real st x in X & not x = -infty
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X is bounded_above & not X = {-infty};
     ex x being set st x in X & not x = -infty
   proof
      assume
A2:   not ex x being set st x in X & not x = -infty;
        for x being set holds x in X implies x in {-infty}
      proof
         let x be set;
         assume x in X;
         then x = -infty by A2;
         hence thesis by TARSKI:def 1;
      end;
      then X c= {-infty} by TARSKI:def 3;
      hence thesis by A1,ZFMISC_1:39;
   end;
   then consider x being set such that
A3:x in X & not x = -infty;
     x in REAL
   proof
   A4:not x = +infty
      proof
         assume
      A5:x = +infty;
         then reconsider x as R_eal;
         consider UB0 being majorant of X such that
      A6:UB0 in REAL by A1,Def11;
         reconsider UB0 as Real by A6;
         reconsider UB0 as R_eal;
           x <=' UB0 by A3,Def9;
         hence thesis by A5,Th18;
      end;
        x in REAL or x in {-infty,+infty} by A3,Def6,XBOOLE_0:def 2;
      hence thesis by A3,A4,TARSKI:def 2;
   end;
   then reconsider x as Real;
   take x;
   thus thesis by A3;
end;

theorem Th60:
   for X being non empty Subset of ExtREAL holds
   X is bounded_below & not X = {+infty} implies
   ex x being Real st x in X & not x = +infty
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X is bounded_below & not X = {+infty};
     ex x being set st x in X & not x = +infty
   proof
      assume
A2:   not ex x being set st x in X & not x = +infty;
        for x being set holds x in X implies x in {+infty}
      proof
         let x be set;
         assume x in X;
         then x = +infty by A2;
         hence thesis by TARSKI:def 1;
      end;
      then X c= {+infty} by TARSKI:def 3;
      hence thesis by A1,ZFMISC_1:39;
   end;
   then consider x being set such that
A3:x in X & not x = +infty;
     x in REAL
   proof
   A4:not x = -infty
      proof
         assume
      A5:x = -infty;
         then reconsider x as R_eal;
         consider LB0 being minorant of X such that
      A6:LB0 in REAL by A1,Def12;
         reconsider LB0 as Real by A6;
         reconsider LB0 as R_eal;
           LB0 <=' x by A3,Def10;
         hence thesis by A5,Th17;
      end;
        x in REAL or x in {-infty,+infty} by A3,Def6,XBOOLE_0:def 2;
      hence thesis by A3,A4,TARSKI:def 2;
   end;
   then reconsider x as Real;
   take x;
   thus thesis by A3;
end;

canceled;

theorem Th62:
   for X being non empty Subset of ExtREAL holds
   (X is bounded_above & not X = {-infty}) implies
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)))
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X is bounded_above & not X = {-infty};
   then consider UB0 being majorant of X such that
A2:UB0 in REAL by Def11;
A3:UB0 in SetMajorant(X) by Def14;
   consider x being Real such that
A4:x in X & not x = -infty by A1,Th59;
   reconsider S = X /\ REAL as Subset of REAL by XBOOLE_1:17;
   reconsider Y = REAL /\ SetMajorant(X) as Subset of REAL by XBOOLE_1:17;
   reconsider UB0 as Real by A2;
A5:x in S by A4,XBOOLE_0:def 3;
     now let a,b be real number;
       assume
   A6:a in S & b in Y;
   then A7:a in X by XBOOLE_0:def 3;
   A8:b in SetMajorant(X) by A6,XBOOLE_0:def 3;
A9:  a is Real & b is Real by XREAL_0:def 1;
       then reconsider d = b as R_eal by Def5,Def6;
   A10:d is majorant of X by A8,Def14;
       reconsider c = a as R_eal by A9,Def5,Def6;
         c <=' d by A7,A10,Def9;
       then ex p,q being Real st p = c & q = d & p <= q by A9,Def7;
       hence a <= b;
   end;
   then consider UB being real number such that
A11:for a,b being real number st a in S & b in Y holds a <= UB & UB <= b by
AXIOMS:26;
    set d = UB;
    reconsider UB as Real by XREAL_0:def 1;
    reconsider UB as R_eal by Def5,Def6;
A12:now let a,b be R_eal;
       assume
   A13:a in X & b in SetMajorant(X);
       thus (a <=' UB & UB <=' b)
       proof
       A14:(not a = -infty & b = +infty) implies (a <=' UB & UB <=' b)
           proof
               assume
           A15:not a = -infty & b = +infty;
             a in REAL
               proof
               A16:a <> +infty
                   proof
                       assume
                   A17:a = +infty;
                       reconsider UB0 as R_eal;
                         a <=' UB0 by A13,Def9;
                       hence thesis by A17,Th18;
                   end;
                     a in REAL or a in {-infty,+infty} by Def6,XBOOLE_0:def 2;
                   hence thesis by A15,A16,TARSKI:def 2;
               end;
               then reconsider a as Real;
           A18:a in S by A13,XBOOLE_0:def 3;
                 a <= d & d <= UB0
               proof
                    UB0 in Y by A3,XBOOLE_0:def 3;
                  hence thesis by A11,A18;
               end;
               hence thesis by A15,Def7,Th2;
           end;
       A19:(a = -infty & not b = +infty) implies (a <=' UB & UB <=' b)
           proof
               assume
           A20:a = -infty & b <> +infty;
A21:              b is majorant of X by A13,Def14;
               reconsider x as R_eal by Def5,Def6;
             x <=' b by A4,A21,Def9;
           then A22:not b = -infty by Th17;
                 b in REAL or b in {-infty,+infty} by Def6,XBOOLE_0:def 2;
               then reconsider b as Real by A20,A22,TARSKI:def 2;
           A23:b in Y by A13,XBOOLE_0:def 3;
               reconsider x as Real;
             x <= d & d <= b by A5,A11,A23;
               hence thesis by A20,Def7,Th6;
           end;
         (a <> -infty & b <> +infty) implies (a <=' UB & UB <=' b)
           proof
               assume
           A24:a <> -infty & b <> +infty;
             a in REAL
               proof
               A25:not a = +infty
                   proof
                       assume
                   A26:a = +infty;
                       reconsider UB0 as R_eal;
                         a <=' UB0 by A13,Def9;
                       hence thesis by A26,Th18;
                   end;
                     a in REAL or a in {-infty,+infty} by Def6,XBOOLE_0:def 2;
                   hence thesis by A24,A25,TARSKI:def 2;
               end;
               then reconsider a as Real;
A27:              b is majorant of X by A13,Def14;
               reconsider x as R_eal by Def5,Def6;
             x <=' b by A4,A27,Def9;
           then A28:not b = -infty by Th17;
                 b in REAL or b in {-infty,+infty} by Def6,XBOOLE_0:def 2;
               then reconsider b as Real by A24,A28,TARSKI:def 2;
           A29:b in Y by A13,XBOOLE_0:def 3;
             a in S by A13,XBOOLE_0:def 3;
           then a <= d & d <= b by A11,A29;
               hence thesis by Def7;
           end;
           hence thesis by A14,A19,Def7,Th2,Th6;
       end;
   end;
A30:UB is majorant of X
   proof
        for a being R_eal st a in X holds a <=' UB by A3,A12;
      hence thesis by Def9;
   end;
A31:for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)
   proof
       let y be R_eal;
       assume
     y is majorant of X;
   then y in SetMajorant(X) by Def14;
       hence thesis by A4,A12;
   end;
   take UB;
   thus thesis by A30,A31;
end;

theorem Th63:
   for X being non empty Subset of ExtREAL holds
   (X is bounded_below & not X = {+infty}) implies
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X ) implies (y <=' LB)))
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X is bounded_below & not X = {+infty};
   then consider LB0 being minorant of X such that
A2:LB0 in REAL by Def12;
A3:LB0 in SetMinorant(X) by Def15;
   consider x being Real such that
A4:x in X & not x = +infty by A1,Th60;
   reconsider S = X /\ REAL as Subset of REAL by XBOOLE_1:17;
   reconsider Y = REAL /\ SetMinorant(X) as Subset of REAL by XBOOLE_1:17;
   reconsider LB0 as Real by A2;
A5:x in S by A4,XBOOLE_0:def 3;
     now let b,a be real number;
       assume
   A6:b in Y & a in S;
   then A7:a in X by XBOOLE_0:def 3;
   A8:b in SetMinorant(X) by A6,XBOOLE_0:def 3;
   A9: a is Real & b is Real by XREAL_0:def 1;
       then reconsider d = b as R_eal by Def5,Def6;
   A10:d is minorant of X by A8,Def15;
       reconsider c = a as R_eal by A9,Def5,Def6;
         d <=' c by A7,A10,Def10;
       then ex p,q being Real st p = d & q = c & p <= q by A9,Def7;
       hence b <= a;
   end;
   then consider LB being real number such that
A11:for b,a being real number st b in Y & a in S holds b <= LB & LB <= a by
AXIOMS:26;
   reconsider LB as Real by XREAL_0:def 1;
   set d = LB;
   reconsider LB as R_eal by Def5,Def6;
A12:for b,a being R_eal st b in SetMinorant(X) & a in
 X holds b <=' LB & LB <=' a
   proof
       let b,a be R_eal;
       assume
   A13:b in SetMinorant(X) & a in X;
   A14:(b = -infty & a <> +infty) implies (b <=' LB & LB <=' a)
       proof
           assume
       A15:b = -infty & not a = +infty;
         a in REAL
           proof
           A16:a <> -infty
               proof
                   assume
               A17:a = -infty;
                   reconsider LB0 as R_eal;
                     LB0 <=' a by A13,Def10;
                   hence thesis by A17,Th17;
               end;
                 a in REAL or a in {-infty,+infty} by Def6,XBOOLE_0:def 2;
               hence thesis by A15,A16,TARSKI:def 2;
           end;
           then reconsider a as Real;
       A18:a in S by A13,XBOOLE_0:def 3;
             LB0 <= d & d <= a
           proof
                LB0 in Y by A3,XBOOLE_0:def 3;
              hence thesis by A11,A18;
           end;
           hence thesis by A15,Def7,Th6;
       end;
   A19:(not b = -infty & a = +infty) implies (b <=' LB & LB <=' a)
       proof
           assume
       A20:not b = -infty & a = +infty;
A21:       b is minorant of X by A13,Def15;
           reconsider x as R_eal by Def5,Def6;
         b <=' x by A4,A21,Def10;
       then A22:not b = +infty by Th18;
             b in REAL or b in {-infty,+infty} by Def6,XBOOLE_0:def 2;
           then reconsider b as Real by A20,A22,TARSKI:def 2;
       A23:b in Y by A13,XBOOLE_0:def 3;
           reconsider x as Real;
         b <= d & d <= x by A5,A11,A23;
           hence thesis by A20,Def7,Th2;
       end;
     (not b = -infty & not a = +infty) implies (b <=' LB & LB <=' a)
       proof
           assume
       A24:not b = -infty & not a = +infty;
         a in REAL
           proof
           A25:not a = -infty
               proof
                   assume
               A26:a = -infty;
                   reconsider LB0 as R_eal;
                     LB0 <=' a by A13,Def10;
                   hence thesis by A26,Th17;
               end;
                 a in REAL or a in {-infty,+infty} by Def6,XBOOLE_0:def 2;
               hence thesis by A24,A25,TARSKI:def 2;
           end;
           then reconsider a as Real;
A27:              b is minorant of X by A13,Def15;
           reconsider x as R_eal by Def5,Def6;
         b <=' x by A4,A27,Def10;
       then A28:not b = +infty by Th18;
             b in REAL or b in {-infty,+infty} by Def6,XBOOLE_0:def 2;
           then reconsider b as Real by A24,A28,TARSKI:def 2;
       A29:b in Y by A13,XBOOLE_0:def 3;
         a in S by A13,XBOOLE_0:def 3;
       then b <= d & d <= a by A11,A29;
           hence thesis by Def7;
       end;
       hence thesis by A14,A19,Def7,Th2,Th6;
   end;
   take LB;
     for a being R_eal st a in X holds LB <=' a by A3,A12;
   hence LB is minorant of X by Def10;
   let y be R_eal;
   assume
  y is minorant of X;
then y in SetMinorant(X) by Def15;
   hence thesis by A4,A12;
end;

theorem Th64:
   for X being non empty Subset of ExtREAL holds
   X = {-infty} implies X is bounded_above
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X = {-infty};
   consider x being Element of REAL;
   reconsider x as R_eal;
     now let a be R_eal;
      assume a in X;
      then a = -infty by A1,TARSKI:def 1;
      hence a <=' x by Def7,Th6;
   end;
   then x is majorant of X by Def9;
   hence thesis by Def11;
end;

theorem Th65:
   for X being non empty Subset of ExtREAL holds
   X = {+infty} implies X is bounded_below
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X = {+infty};
   consider x being Element of REAL;
   reconsider x as R_eal;
     now let a be R_eal;
      assume a in X;
      then a = +infty by A1,TARSKI:def 1;
      hence x <=' a by Def7,Th2;
   end;
   then x is minorant of X by Def10;
   hence thesis by Def12;
end;

theorem Th66:
   for X being non empty Subset of ExtREAL holds
   X = {-infty} implies
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)))
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X = {-infty};
   set UB = -infty;
A2:for a being R_eal holds a in X implies a <=' UB by A1,TARSKI:def 1;
   take UB;
   thus thesis by A2,Def7,Def9,Th6;
end;

theorem Th67:
   for X being non empty Subset of ExtREAL holds
   X = {+infty} implies
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X ) implies (y <=' LB)))
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X = {+infty};
   set LB = +infty;
A2:   for a being R_eal holds a in X implies LB <=' a by A1,TARSKI:def 1;
   take LB;
   thus thesis by A2,Def7,Def10,Th2;
end;

theorem Th68:
   for X being non empty Subset of ExtREAL holds
   X is bounded_above implies
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   y is majorant of X implies UB <=' y))
proof
   let X be non empty Subset of ExtREAL;
   assume X is bounded_above;
then (X is bounded_above & not X = {-infty}) or (X is bounded_above & X = {
-infty});
   hence thesis by Th62,Th66;
end;

theorem Th69:
   for X being non empty Subset of ExtREAL holds
   X is bounded_below implies
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X ) implies (y <=' LB)))
proof
   let X be non empty Subset of ExtREAL;
   assume X is bounded_below;
then (X is bounded_below & not X = {+infty}) or (X is bounded_below & X = {
+infty});
   hence thesis by Th63,Th67;
end;

theorem Th70:
   for X being non empty Subset of ExtREAL holds
   not X is bounded_above implies
   (for y being R_eal holds
   (y is majorant of X implies y = +infty))
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:not X is bounded_above;
     for y being R_eal holds
   (y is majorant of X implies y = +infty)
   proof
      let y be R_eal;
      assume
   A2:y is majorant of X;
   then not y in REAL by A1,Def11;
      then A3: y in {-infty,+infty} by Def6,XBOOLE_0:def 2;

     not y = -infty
      proof
         assume
      A4:y = -infty;
           for a being set holds a in X implies a in {-infty}
         proof
            let a be set;
            assume
         A5:a in X;
            then a in REAL or a in {-infty,+infty} by Def6,XBOOLE_0:def 2;
            then A6:a in REAL or a = -infty or a = +infty by TARSKI:def 2;
            reconsider a as R_eal by A5;
          a <=' -infty by A2,A4,A5,Def9;
            hence thesis by A6,Def7,Th6,Th14,TARSKI:def 1;
         end;
         then X c= {-infty} by TARSKI:def 3;
         then X = {} or X = {-infty} by ZFMISC_1:39;
         hence thesis by A1,Th64;
      end;
      hence thesis by A3,TARSKI:def 2;
   end;
   hence thesis;
end;

theorem Th71:
   for X being non empty Subset of ExtREAL holds
   not X is bounded_below implies
   (for y being R_eal holds
   (y is minorant of X implies y = -infty))
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:not X is bounded_below;

     for y being R_eal holds
   (y is minorant of X implies y = -infty)
   proof
      let y be R_eal;
      assume
   A2:y is minorant of X;
   then not y in REAL by A1,Def12;
      then A3: y in {-infty,+infty} by Def6,XBOOLE_0:def 2;
     not y = +infty
      proof
         assume
      A4:y = +infty;
           for a being set holds a in X implies a in {+infty}
         proof
            let a be set;
            assume
         A5:a in X;

            then a in REAL or a in {-infty,+infty} by Def6,XBOOLE_0:def 2;
            then A6:a in REAL or a = -infty or a = +infty by TARSKI:def 2;
            reconsider a as R_eal by A5;
          +infty <=' a by A2,A4,A5,Def10;
            hence thesis by A6,Def7,Th2,Th14,TARSKI:def 1;
         end;
         then X c= {+infty} by TARSKI:def 3;
         then X = {} or X = {+infty} by ZFMISC_1:39;
         hence thesis by A1,Th65;
      end;
      hence thesis by A3,TARSKI:def 2;
   end;
   hence thesis;
end;

theorem Th72:
   for X being non empty Subset of ExtREAL holds
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)))
proof
   let X be non empty Subset of ExtREAL;
  not X is bounded_above implies
   ex UB being R_eal st ((UB is majorant of X) &
   (for y being R_eal holds
   (y is majorant of X ) implies (UB <=' y)))
   proof
      assume
A1:   not X is bounded_above;
      set UB = +infty;
      take UB;
      thus thesis by A1,Th33,Th70;
   end;
   hence thesis by Th68;
end;

theorem Th73:
   for X being non empty Subset of ExtREAL holds
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X) implies (y <=' LB)))
proof
   let X be non empty Subset of ExtREAL;
  not X is bounded_below implies
   ex LB being R_eal st ((LB is minorant of X) &
   (for y being R_eal holds
   (y is minorant of X ) implies (y <=' LB)))
   proof
      assume
A1:   not X is bounded_below;
      set LB = -infty;
      take LB;
      thus thesis by A1,Th36,Th71;
   end;
   hence thesis by Th69;
end;

::
::       sup X, inf X least upper bound and greatest lower bound of set X
::

definition
   let X be non empty Subset of ExtREAL;
   func sup X -> R_eal means
:Def16: it is majorant of X &
      for y being R_eal holds
      y is majorant of X implies it <=' y;
existence by Th72;
uniqueness
proof
   let S1,S2 be R_eal such that
A1:S1 is majorant of X &
   for y being R_eal holds
   (y is majorant of X ) implies (S1 <=' y) and
A2:S2 is majorant of X &
   for y being R_eal holds
   (y is majorant of X ) implies (S2 <=' y);
     S1 <=' S2 & S2 <=' S1 by A1,A2;
   hence thesis by Th22;
end;
end;

canceled 2;

theorem Th76:
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   x in X implies x <=' sup X
proof
   let X be non empty Subset of ExtREAL;
   let x be R_eal;
   assume
A1:x in X;
     sup X is majorant of X by Def16;
   hence thesis by A1,Def9;
end;

definition
   let X be non empty Subset of ExtREAL;
   func inf X -> R_eal means
:Def17: it is minorant of X &
      for y being R_eal holds
      y is minorant of X implies y <=' it;
existence by Th73;
uniqueness
proof
   let S1,S2 be R_eal such that
A1:S1 is minorant of X &
   for y being R_eal holds
   (y is minorant of X ) implies (y <=' S1) and
A2:S2 is minorant of X &
   for y being R_eal holds
   (y is minorant of X ) implies (y <=' S2);
     S1 <=' S2 & S2 <=' S1 by A1,A2;
   hence thesis by Th22;
end;
end;

canceled 2;

theorem Th79:
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   x in X implies inf X <=' x
proof
   let X be non empty Subset of ExtREAL;
   let x be R_eal;
   assume
A1:x in X;
     inf X is minorant of X by Def17;
   hence thesis by A1,Def10;
end;

theorem Th80:
   for X being non empty Subset of ExtREAL holds
   for x being majorant of X holds
   x in X implies x = sup X
proof
   let X be non empty Subset of ExtREAL;
   let x be majorant of X;
   assume x in X;
   then for y being R_eal holds
   (y is majorant of X) implies (x <=' y) by Def9;
   hence thesis by Def16;
end;

theorem Th81:
   for X being non empty Subset of ExtREAL holds
   for x being minorant of X holds
   x in X implies x = inf X
proof
   let X be non empty Subset of ExtREAL;
   let x be minorant of X;
   assume x in X;
   then for y being R_eal holds
   (y is minorant of X) implies (y <=' x) by Def10;
   hence thesis by Def17;
end;

theorem
     for X being non empty Subset of ExtREAL holds
   sup X = inf SetMajorant(X) & inf X = sup SetMinorant(X)
proof
   let X be non empty Subset of ExtREAL;
     sup X is majorant of X by Def16;
then A1:sup X in SetMajorant(X) by Def14;
     for y being R_eal holds (y in SetMajorant(X)) implies
   sup X <=' y
   proof
      let y be R_eal;
      assume y in SetMajorant(X);
      then y is majorant of X by Def14;
      hence thesis by Def16;
   end;
   then A2: sup X is minorant of SetMajorant(X) by Def10;
     inf X is minorant of X by Def17;
then A3:inf X in SetMinorant(X) by Def15;
     for y being R_eal holds (y in SetMinorant(X)) implies
   (y <=' inf X)
   proof
      let y be R_eal;
      assume y in SetMinorant(X);
      then y is minorant of X by Def15;
      hence thesis by Def17;
   end;
   then inf X is majorant of SetMinorant(X) by Def9;
   hence thesis by A1,A2,A3,Th80,Th81;
end;

theorem
     for X being non empty Subset of ExtREAL holds
   X is bounded_above & not X = {-infty} implies sup X in REAL
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X is bounded_above & not X = {-infty};
   then consider UB0 being majorant of X such that
A2:UB0 in REAL by Def11;
A3:sup X <=' UB0 by Def16;
   consider x being Real such that
A4:x in X & not x = -infty by A1,Th59;
   reconsider x as R_eal by Def5,Def6;
  sup X is majorant of X by Def16;
then x <=' sup X by A4,Def9;
then not sup X = -infty by Th17;
   hence thesis by A2,A3,Def7,Th2;
end;

theorem
     for X being non empty Subset of ExtREAL holds
   X is bounded_below & not X = {+infty} implies inf X in REAL
proof
   let X be non empty Subset of ExtREAL;
   assume
A1:X is bounded_below & not X = {+infty};
   then consider LB0 being minorant of X such that
A2:LB0 in REAL by Def12;
A3:LB0 <=' inf X by Def17;
   consider x being Real such that
A4:x in X & not x = +infty by A1,Th60;
   reconsider x as R_eal by Def5,Def6;
  inf X is minorant of X by Def17;
then inf X <=' x by A4,Def10;
then not inf X = +infty by Th18;
   hence thesis by A2,A3,Def7,Th6;
end;

definition let x be R_eal;
  redefine func {x} -> Subset of ExtREAL;
coherence by ZFMISC_1:37;
end;

definition let x,y be R_eal;
  redefine func {x,y} -> Subset of ExtREAL;
coherence by ZFMISC_1:38;
end;

theorem Th85:
   for x being R_eal holds sup{x} = x
proof
   let x be R_eal;
A1:sup{x} is majorant of {x} by Def16;
  x is majorant of {x}
   proof
        for a being R_eal holds a in {x} implies a <=' x by TARSKI:def 1;
      hence thesis by Def9;
   end;
then A2:sup{x} <=' x by Def16;
     x in {x} by TARSKI:def 1;
   then x <=' sup{x} by A1,Def9;
   hence thesis by A2,Th22;
end;

theorem Th86:
   for x being R_eal holds inf{x} = x
proof
   let x be R_eal;
A1:inf{x} is minorant of {x} by Def17;
  x is minorant of {x}
   proof
        for a being R_eal holds a in {x} implies x <=' a by TARSKI:def 1;
      hence thesis by Def10;
   end;
then A2:x <=' inf{x} by Def17;
     x in {x} by TARSKI:def 1;
   then inf{x} <=' x by A1,Def10;
   hence thesis by A2,Th22;
end;

theorem
     sup {-infty} = -infty by Th85;

theorem
     sup {+infty} = +infty by Th85;

theorem
     inf {-infty} = -infty by Th86;

theorem
     inf {+infty} = +infty by Th86;

theorem Th91:
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies sup X <=' sup Y
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
      set S2 = sup Y;
     S2 is majorant of Y &
      for y being R_eal holds
      (y is majorant of Y implies (S2 <=' y)) by Def16;
   then S2 is majorant of X by A1,Th34;
      hence thesis by Def16;
end;

theorem Th92:
   for x,y being R_eal holds
   for a being R_eal holds
   (x <=' a & y <=' a implies sup{x,y} <=' a)
proof
   let x,y be R_eal;
   let a be R_eal;
   assume x <=' a & y <=' a;
   then for c being R_eal holds c in {x,y} implies c <=' a by TARSKI:def 2;
   then a is majorant of {x,y} by Def9;
   hence thesis by Def16;
end;

theorem
     for x,y being R_eal holds
   (x <=' y implies sup{x,y} = y) & (y <=' x implies sup{x,y} = x)
proof
   let x,y be R_eal;
   thus x <=' y implies sup{x,y} = y
   proof
      assume x <=' y;
   then A1:sup{x,y} <=' y by Th92;
   A2:y in {x,y} by TARSKI:def 2;
        sup{x,y} is majorant of {x,y} by Def16;
      then y <=' sup{x,y} by A2,Def9;
      hence thesis by A1,Th22;
   end;
      assume y <=' x;
   then A3:sup{x,y} <=' x by Th92;
   A4:x in {x,y} by TARSKI:def 2;
        sup{x,y} is majorant of {x,y} by Def16;
      then x <=' sup{x,y} by A4,Def9;
      hence thesis by A3,Th22;
end;

theorem Th94:
   for X,Y being non empty Subset of ExtREAL holds
   X c= Y implies inf Y <=' inf X
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:X c= Y;
     inf Y <=' inf X
   proof
      set S2 = inf Y;
     S2 is minorant of Y &
      for y being R_eal holds
      (y is minorant of Y implies (y <=' S2)) by Def17;
   then S2 is minorant of X by A1,Th39;
      hence thesis by Def17;
   end;
   hence thesis;
end;

theorem Th95:
   for x,y being R_eal holds
   for a being R_eal holds
   (a <=' x & a <=' y implies a <=' inf{x,y})
proof
   let x,y be R_eal;
   let a be R_eal;
   assume a <=' x & a <=' y;
   then for c being R_eal holds c in {x,y} implies a <=' c by TARSKI:def 2;
   then a is minorant of {x,y} by Def10;
   hence thesis by Def17;
end;

theorem
     for x,y being R_eal holds
   (x <=' y implies inf{x,y} = x) & (y <=' x implies inf{x,y} = y)
proof
   let x,y be R_eal;
   thus x <=' y implies inf{x,y} = x
   proof
      assume x <='y;
   then A1:x <=' inf{x,y} by Th95;
   A2:x in {x,y} by TARSKI:def 2;
        inf{x,y} is minorant of {x,y} by Def17;
      then inf{x,y} <=' x by A2,Def10;
      hence thesis by A1,Th22;
   end;
      assume y <='x;
   then A3:y <=' inf{x,y} by Th95;
   A4:y in {x,y} by TARSKI:def 2;
        inf{x,y} is minorant of {x,y} by Def17;
      then inf{x,y} <=' y by A4,Def10;
      hence thesis by A3,Th22;
end;

theorem Th97:
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   ((ex y being R_eal st (y in X & x <=' y)) implies x <=' sup X)
proof
   let X be non empty Subset of ExtREAL;
   let x be R_eal;
   given y being R_eal such that
A1:y in X & x <=' y;
     sup X is majorant of X by Def16;
   then y <=' sup X by A1,Def9;
   hence thesis by A1,Th29;
end;

theorem Th98:
   for X being non empty Subset of ExtREAL holds
   for x being R_eal holds
   ((ex y being R_eal st (y in X & y <=' x)) implies inf X <=' x)
proof
   let X be non empty Subset of ExtREAL;
   let x be R_eal;
   given y being R_eal such that
A1:y in X & y <=' x;
     inf X is minorant of X by Def17;
   then inf X <=' y by A1,Def10;
   hence thesis by A1,Th29;
end;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   (for x being R_eal st x in X holds
   (ex y being R_eal st y in Y & x <=' y)) implies
   sup X <=' sup Y
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:for x being R_eal st x in X holds (ex y being R_eal st y in Y & x <=' y);
     for x being R_eal st x in X holds x <=' sup Y
   proof
      let x be R_eal;
      assume x in X;
      then consider y being R_eal such that
   A2:y in Y & x <=' y by A1;
        y <=' sup Y by A2,Th76;
      hence thesis by A2,Th29;
   end;
   then sup Y is majorant of X by Def9;
   hence thesis by Def16;
end;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   (for y being R_eal st y in Y holds
   (ex x being R_eal st x in X & x <=' y)) implies
   inf X <=' inf Y
proof
   let X,Y be non empty Subset of ExtREAL;
   assume
A1:for y being R_eal st y in Y holds (ex x being R_eal st x in X & x <=' y);
     for y being R_eal st y in Y holds inf X <=' y
   proof
      let y be R_eal;
      assume y in Y;
      then consider x being R_eal such that
   A2:x in X & x <=' y by A1;
        inf X <=' x by A2,Th79;
      hence thesis by A2,Th29;
   end;
   then inf X is minorant of Y by Def10;
   hence thesis by Def17;
end;

theorem Th101:
   for X,Y being non empty Subset of ExtREAL holds
   for UB1 being majorant of X holds
   for UB2 being majorant of Y holds
   sup{UB1,UB2} is majorant of X \/ Y
proof
   let X,Y be non empty Subset of ExtREAL;
   let UB1 be majorant of X;
   let UB2 be majorant of Y;
     for a being R_eal holds
   a in X \/ Y implies a <=' sup{UB1,UB2}
   proof
      let a be R_eal;
      assume
A1:   a in X \/ Y;
   A2:a in X implies a <=' sup{UB1,UB2}
      proof
         assume a in X;
      then A3:a <=' UB1 by Def9;
      A4:UB1 in {UB1,UB2} by TARSKI:def 2;
           sup{UB1,UB2} is majorant of {UB1,UB2} by Def16;
         then UB1 <=' sup{UB1,UB2}by A4,Def9;
         hence thesis by A3,Th29;
      end;
     a in Y implies a <=' sup{UB1,UB2}
      proof
         assume a in Y;
      then A5:a <=' UB2 by Def9;
      A6:UB2 in {UB1,UB2} by TARSKI:def 2;
           sup{UB1,UB2} is majorant of {UB1,UB2} by Def16;
         then UB2 <=' sup{UB1,UB2}by A6,Def9;
         hence thesis by A5,Th29;
      end;
      hence thesis by A1,A2,XBOOLE_0:def 2;
   end;
   hence thesis by Def9;
end;

theorem Th102:
   for X,Y being non empty Subset of ExtREAL holds
   for LB1 being minorant of X holds
   for LB2 being minorant of Y holds
   inf{LB1,LB2} is minorant of X \/ Y
proof
   let X,Y be non empty Subset of ExtREAL;
   let LB1 be minorant of X;
   let LB2 be minorant of Y;
     for a being R_eal holds
   a in X \/ Y implies inf{LB1,LB2} <=' a
   proof
      let a be R_eal;
      assume
A1:   a in X \/ Y;

   A2:a in X implies inf{LB1,LB2} <=' a
      proof
         assume a in X;
      then A3:LB1 <=' a by Def10;
      A4:LB1 in {LB1,LB2} by TARSKI:def 2;
           inf{LB1,LB2} is minorant of {LB1,LB2} by Def17;
         then inf{LB1,LB2} <=' LB1 by A4,Def10;
         hence thesis by A3,Th29;
      end;
     a in Y implies inf{LB1,LB2} <=' a
      proof
         assume a in Y;
      then A5:LB2 <=' a by Def10;
      A6:LB2 in {LB1,LB2} by TARSKI:def 2;
           inf{LB1,LB2} is minorant of {LB1,LB2} by Def17;
         then inf{LB1,LB2} <=' LB2 by A6,Def10;
         hence thesis by A5,Th29;
      end;
      hence thesis by A1,A2,XBOOLE_0:def 2;
   end;
   hence thesis by Def10;
end;

theorem Th103:
   for X,Y,S being non empty Subset of ExtREAL holds
   for UB1 being majorant of X holds
   for UB2 being majorant of Y holds
   S = X /\ Y implies inf{UB1,UB2} is majorant of S
proof
   let X,Y,S be non empty Subset of ExtREAL;
   let UB1 be majorant of X;
   let UB2 be majorant of Y;
   assume
A1:S = X /\ Y;
     now let a be R_eal;
      assume a in S;
      then a in X & a in Y by A1,XBOOLE_0:def 3;
      then a <=' UB1 & a <=' UB2 by Def9;
      hence a <=' inf{UB1,UB2} by Th95;
   end;
   hence thesis by Def9;
end;

theorem Th104:
   for X,Y,S being non empty Subset of ExtREAL holds
   for LB1 being minorant of X holds
   for LB2 being minorant of Y holds
   S = X /\ Y implies sup{LB1,LB2} is minorant of S
proof
   let X,Y,S be non empty Subset of ExtREAL;
   let LB1 be minorant of X;
   let LB2 be minorant of Y;
   assume
A1:S = X /\ Y;
     now let a be R_eal;
      assume a in S;
      then a in X & a in Y by A1,XBOOLE_0:def 3;
      then LB1 <=' a & LB2 <=' a by Def10;
      hence sup{LB1,LB2} <=' a by Th92;
   end;
   hence thesis by Def10;
end;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   sup(X \/ Y) = sup{sup X,sup Y}
proof
    let X,Y be non empty Subset of ExtREAL;
    set a = sup(X \/ Y);
 A1:sup X is majorant of X by Def16;
   sup Y is majorant of Y by Def16;
 then sup{sup X,sup Y} is majorant of X \/ Y by A1,Th101;
 then A2:a <=' sup{sup X,sup Y} by Def16;
      X c= X \/ Y by XBOOLE_1:7;
 then A3:sup X <=' a by Th91;
      Y c= X \/ Y by XBOOLE_1:7;
    then sup Y <=' a by Th91;
    then sup{sup X,sup Y} <=' a by A3,Th92;
    hence thesis by A2,Th22;
end;

theorem
     for X,Y being non empty Subset of ExtREAL holds
   inf(X \/ Y) = inf{inf X,inf Y}
proof
    let X,Y be non empty Subset of ExtREAL;
    set a = inf(X \/ Y);
 A1:inf X is minorant of X by Def17;
   inf Y is minorant of Y by Def17;
 then inf{inf X,inf Y} is minorant of X \/ Y by A1,Th102;
 then A2:inf{inf X,inf Y} <=' a by Def17;
      X c= X \/ Y by XBOOLE_1:7;
 then A3:a <=' inf X by Th94;
      Y c= X \/ Y by XBOOLE_1:7;
then a <=' inf Y by Th94;
    then a <=' inf{inf X,inf Y} by A3,Th95;
    hence thesis by A2,Th22;
end;

theorem
     for X,Y,S being non empty Subset of ExtREAL holds
   S = X /\ Y implies sup(S) <=' inf{sup X,sup Y}
proof
   let X,Y,S be non empty Subset of ExtREAL;
   assume
A1:S = X /\ Y;
     sup(S) <=' inf{sup X,sup Y}
   proof
   A2:sup X is majorant of X by Def16;
     sup Y is majorant of Y by Def16;
  then inf{sup X,sup Y} is majorant of S by A1,A2,Th103;
      hence thesis by Def16;
   end;
   hence thesis;
end;

theorem
     for X,Y,S being non empty Subset of ExtREAL holds
   S = X /\ Y implies sup{inf X,inf Y} <=' inf(S)
proof
   let X,Y,S be non empty Subset of ExtREAL;
   assume
A1:S = X /\ Y;
     sup{inf X,inf Y} <=' inf(S)
   proof
   A2:inf X is minorant of X by Def17;
     inf Y is minorant of Y by Def17;
  then sup{inf X,inf Y} is minorant of S by A1,A2,Th104;
      hence thesis by Def17;
   end;
   hence thesis;
end;

definition
   let X be non empty set;
   mode bool_DOMAIN of X -> set means
:Def18: it is non empty Subset of bool X &
        for A being set holds
        A in it implies A is non empty set;
existence
proof
   set F = {X};
 A1: for x being set holds x in F implies x in bool X
   proof
      let x be set;
      assume
   A2:x in F;
       X in bool X by ZFMISC_1:def 1;
      hence thesis by A2,TARSKI:def 1;
   end;
   take F;
   thus thesis by A1,TARSKI:def 1,def 3;
end;
end;

definition
   let F be bool_DOMAIN of ExtREAL;
   func SUP(F) -> Subset of ExtREAL means
:Def19:for a being R_eal holds
         a in it iff ex A being non empty Subset of ExtREAL st
          A in F & a = sup A;
existence
proof
 defpred P[R_eal] means
   ex A being non empty Subset of ExtREAL st A in F & $1 = sup A;
 ex S being Subset of REAL \/ {-infty,+infty} st
   for a being R_eal holds a in S iff P[a] from SepR_eal;
   then consider S being Subset of ExtREAL such that
A1:for a being R_eal holds a in S iff
   ex A being non empty Subset of ExtREAL st (A in F & a = sup A) by Def6;
   reconsider S as Subset of ExtREAL;
   take S;
   thus thesis by A1;
end;
uniqueness
proof
   let S1,S2 be Subset of ExtREAL such that
A2:for a being R_eal holds a in S1 iff
   ex A being non empty Subset of ExtREAL st (A in F & a = sup A) and
A3:for a being R_eal holds a in S2 iff
   ex A being non empty Subset of ExtREAL st (A in F & a = sup A);
  for a being set holds (a in S1 iff a in S2)
   proof
      let a be set;
      hereby assume
       a in S1;
         then ex A being non empty Subset of ExtREAL st A in F & a = sup A by
A2;
         hence a in S2 by A3;
      end;
      assume
   A4:a in S2;
      then reconsider a as R_eal;
        ex A being non empty Subset of ExtREAL st A in F & a = sup A by A3,A4;
      hence thesis by A2;
   end;
   hence thesis by TARSKI:2;
end;
end;

definition
   let F be bool_DOMAIN of ExtREAL;
   cluster SUP(F) -> non empty;
   coherence
   proof
A1:F is non empty Subset of bool ExtREAL &
   for A being set holds A in F implies A is non empty set by Def18;
   consider A being Element of F;
   reconsider A as non empty Subset of ExtREAL by A1,TARSKI:def 3;
     sup A = sup A;
   hence thesis by A1,Def19;
   end;
end;

canceled 3;

theorem Th112:
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies sup S is majorant of SUP(F)
proof
   let F be bool_DOMAIN of ExtREAL;
   let S be non empty Subset of ExtREAL;
   assume
A1:S = union F;
     for x being R_eal holds x in SUP(F) implies x <=' sup S
   proof
      let x be R_eal;
      assume x in SUP(F);
      then consider A being non empty Subset of ExtREAL such that
   A2:A in F & x = sup A by Def19;
        A c= S
      proof
         let a be set; assume a in A;
         hence thesis by A1,A2,TARSKI:def 4;
      end;
      hence thesis by A2,Th91;
   end;
   hence thesis by Def9;
end;

theorem Th113:
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies sup SUP(F) is majorant of S
proof
   let F be bool_DOMAIN of ExtREAL;
   let S be non empty Subset of ExtREAL;
   assume
A1:S = union F;
     for x being R_eal holds
   x in S implies x <=' sup SUP(F)
   proof
      let x be R_eal;
      assume
     x in S;
      then consider Z being set such that
   A2:x in Z & Z in F by A1,TARSKI:def 4;
        F is non empty Subset of bool ExtREAL by Def18;
      then reconsider Z as non empty Subset of ExtREAL by A2;
      consider a being set such that
   A3:a = sup Z;
      reconsider a as R_eal by A3;
        sup Z is majorant of Z by Def16;
   then A4:x <=' sup Z by A2,Def9;
        a in SUP(F) by A2,A3,Def19;
      hence thesis by A3,A4,Th97;
   end;
   hence thesis by Def9;
end;

theorem
     for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies sup S = sup SUP(F)
proof
   let F be bool_DOMAIN of ExtREAL;
   let S be non empty Subset of ExtREAL;
   assume
A1:S = union F;
   set a = sup S;
   set b = sup SUP(F);
A2:sup SUP(F) is majorant of S by A1,Th113;
     sup S is majorant of SUP(F) by A1,Th112;
   then a <=' b & b <=' a by A2,Def16;
   hence thesis by Th22;
end;

definition
   let F be bool_DOMAIN of ExtREAL;
   func INF(F) -> Subset of ExtREAL means
:Def20:for a being R_eal holds
        a in it iff ex A being non empty Subset of ExtREAL st A in
 F & a = inf A;
existence
proof defpred P[R_eal] means
   ex A being non empty Subset of ExtREAL st A in F & $1 = inf A;
A1:ex S being Subset of REAL \/ {-infty,+infty} st
   for a being R_eal holds a in S iff P[a] from SepR_eal;
A2:F is non empty Subset of bool ExtREAL &
   for A being set holds A in F implies A is non empty set by Def18;
   consider A being Element of F;
   reconsider A as non empty Subset of ExtREAL by A2,TARSKI:def 3;
A3:inf A = inf A;
   consider S being Subset of ExtREAL such that
A4:for a being R_eal holds a in S iff
   ex A being non empty Subset of ExtREAL st (A in F & a = inf A) by A1,Def6;
   reconsider S as non empty set by A2,A3,A4;
   reconsider S as non empty Subset of ExtREAL;
   take S;
   thus thesis by A4;
end;
uniqueness
proof
   let S1,S2 be Subset of ExtREAL such that
A5:for a being R_eal holds a in S1 iff
   ex A being non empty Subset of ExtREAL st (A in F & a = inf A) and
A6:for a being R_eal holds a in S2 iff
   ex A being non empty Subset of ExtREAL st (A in F & a = inf A);
  for a being set holds a in S1 iff a in S2
   proof
      let a be set;
      hereby assume
      A7:a in S1;
         then reconsider a' = a as R_eal;
           ex A being non empty Subset of ExtREAL st A in
 F & a' = inf A by A5,A7;
         hence a in S2 by A6;
      end;
         assume
      A8:a in S2;
         then reconsider a as R_eal;
           ex A being non empty Subset of ExtREAL st A in F & a = inf A by A6,
A8
;
         hence thesis by A5;
   end;
   hence thesis by TARSKI:2;
end;
end;

definition
   let F be bool_DOMAIN of ExtREAL;
   cluster INF(F) -> non empty;
coherence
proof
A1:F is non empty Subset of bool ExtREAL &
   for A being set holds A in F implies A is non empty set by Def18;
   consider A being Element of F;
   reconsider A as non empty Subset of ExtREAL by A1,TARSKI:def 3;
     inf A = inf A;
   hence thesis by A1,Def20;
end;
end;

canceled 2;

theorem Th117:
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies inf S is minorant of INF(F)
proof
   let F be bool_DOMAIN of ExtREAL;
   let S be non empty Subset of ExtREAL;
   assume
A1:S = union F;
     for x being R_eal holds x in INF(F) implies inf S <=' x
   proof
      let x be R_eal;
      assume x in INF(F);
      then consider A being non empty Subset of ExtREAL such that
   A2:A in F & x = inf A by Def20;
     A c= S
      proof
         let a be set; assume a in A;
         hence thesis by A1,A2,TARSKI:def 4;
      end;
      hence thesis by A2,Th94;
   end;
   hence thesis by Def10;
end;

theorem Th118:
   for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies inf INF(F) is minorant of S
proof
   let F be bool_DOMAIN of ExtREAL;
   let S be non empty Subset of ExtREAL;
   assume
A1:S = union F;
     for x being R_eal holds
   x in S implies inf INF(F) <=' x
   proof
      let x be R_eal;
      assume
     x in S;
         then consider Z being set such that
      A2:x in Z & Z in F by A1,TARSKI:def 4;
           F is non empty Subset of bool ExtREAL by Def18;
         then reconsider Z as non empty Subset of ExtREAL by A2;
         consider a being set such that
      A3:a = inf Z;
         reconsider a as R_eal by A3;
           inf Z is minorant of Z by Def17;
      then A4:inf Z <=' x by A2,Def10;
        a in INF(F) by A2,A3,Def20;
         hence thesis by A3,A4,Th98;
   end;
   hence thesis by Def10;
end;

theorem
     for F being bool_DOMAIN of ExtREAL holds
   for S being non empty Subset of ExtREAL holds
   S = union F implies inf S = inf INF(F)
proof
   let F be bool_DOMAIN of ExtREAL;
   let S be non empty Subset of ExtREAL;
   assume
A1:S = union F;
   set a = inf S;
   set b = inf INF(F);
A2:   inf INF(F) is minorant of S by A1,Th118;
     inf S is minorant of INF(F) by A1,Th117;
   then a <=' b & b <=' a by A2,Def17;
   hence thesis by Th22;
end;

Back to top