The Mizar article:

Properties of the Intervals of Real Numbers

by
Jozef Bialas

Received January 12, 1993

Copyright (c) 1993 Association of Mizar Users

MML identifier: MEASURE5
[ MML identifier index ]


environ

 vocabulary SUPINF_1, ARYTM_3, RLVECT_1, ARYTM_1, ORDINAL2, RCOMP_1, BOOLE,
      MEASURE5, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, REAL_1, SUPINF_1,
      SUPINF_2;
 constructors REAL_1, SUPINF_2, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, XREAL_0, XBOOLE_0, MEMBERED, ZFMISC_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0;
 theorems TARSKI, SUPINF_1, SUPINF_2, REAL_1, MEASURE3, MEASURE4, XREAL_0,
      XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes SUPINF_1;

begin  :: Some theorems about R_eal numbers

 reserve x,y,a,b,a1,b1,a2,b2 for R_eal;

theorem Th1:
   x <> -infty & x <> +infty & x <=' y implies
   0. <=' y - x
proof
   assume
A1:x <> -infty & x <> +infty & x <=' y;
   consider z being R_eal such that
A2:z = 0.;
     z + x = x by A2,SUPINF_2:18;
   hence thesis by A1,A2,MEASURE4:2;
end;

theorem Th2:
   (not (x = -infty & y = -infty) & not (x = +infty & y = +infty) & x <=' y)
   implies 0. <=' y - x
proof
   assume
A1:not (x = -infty & y = -infty) & not (x = +infty & y = +infty) & x <=' y;
A2:   (x in REAL or x in {-infty,+infty}) & (y in REAL or y in {-infty,+infty})
   by SUPINF_1:def 6,XBOOLE_0:def 2;
   per cases by A1,A2,TARSKI:def 2;
   suppose x in REAL & y in REAL;
   then not x = -infty & not x = +infty by SUPINF_1:31;
   hence thesis by A1,Th1;
   suppose x in REAL & y = -infty;
   hence thesis by A1,SUPINF_1:23;
   suppose x in REAL & y = +infty;
   hence thesis by SUPINF_1:2,SUPINF_2:6,19;
   suppose x = -infty & y in REAL;
   hence thesis by SUPINF_1:6,SUPINF_2:7,19;
   suppose x = -infty & y = +infty;
   hence thesis by SUPINF_2:7,19;
   suppose x = +infty & y in REAL; hence thesis by A1,SUPINF_1:24;
   suppose x = +infty & y = -infty; hence thesis by A1,SUPINF_1:24;
end;

canceled 5;

theorem
     for a,b,c being R_eal holds
   (b <> -infty & b <> +infty &
   not (a = -infty & c = -infty) & not (a = +infty & c = +infty)) implies
   (c - b) + (b - a) = c - a
proof
   let a,b,c be R_eal;
   assume
A1:b <> -infty & b <> +infty &
   not (a = -infty & c = -infty) & not (a = +infty & c = +infty);
A2:(a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
   per cases by A1,A2,TARSKI:def 2;
      suppose
      A3:a in REAL & b in REAL;
A4:         c in REAL or c in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
           now per cases by A3,A4,TARSKI:def 2;
            suppose a in REAL & b in REAL & c in REAL;
               then consider x,y,z being Real such that
            A5:x = a & y = b & z = c;
              c - b = z - y & b - a = y - x by A5,SUPINF_2:5;
               hence (c -b) + (b - a) = (z - y) + (y - x) by SUPINF_2:1
                         .= z - (y - (y - x)) by XCMPLX_1:37
                         .= z - (y - y + x) by XCMPLX_1:37
                         .= z - (y + (-y) + x) by XCMPLX_0:def 8
                         .= z - (0 + x) by XCMPLX_0:def 6
                         .= c - a by A5,SUPINF_2:5;
            suppose
            A6:a in REAL & b in REAL & c = -infty;
            then A7:(c -b) + (b - a) = -infty
 + (b - a) by SUPINF_1:6,SUPINF_2:7;
               consider x,y being Real such that
            A8:x = a & y = b by A6;
              b - a = y - x by A8,SUPINF_2:5;
               then not b - a = +infty by SUPINF_1:2;
               then (c -b) + (b - a) = -infty by A7,SUPINF_2:def 2;
               hence thesis by A6,SUPINF_1:6,SUPINF_2:7;
            suppose
            A9:a in REAL & b in REAL & c = +infty;
            then A10:(c -b) + (b - a) = +infty
 + (b - a) by SUPINF_1:2,SUPINF_2:6;
               consider x,y being Real such that
            A11:x = a & y = b by A9;
              b - a = y - x by A11,SUPINF_2:5;
               then not b - a = -infty by SUPINF_1:6;
               then (c -b) + (b - a) = +infty by A10,SUPINF_2:def 2;
               hence thesis by A9,SUPINF_1:2,SUPINF_2:6;
         end;
         hence thesis;
      suppose
      A12:a = -infty & b in REAL;
A13:     c in REAL or c in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
           now per cases by A1,A12,A13,TARSKI:def 2;
            suppose
            A14:a = -infty & b in REAL & c in REAL;
            then A15:(c -b) + (b - a) = (c - b) + (+infty) by SUPINF_1:6,
SUPINF_2:7;
               consider x,y being Real such that
            A16:x = c & y = b by A14;
                 c - b = x - y by A16,SUPINF_2:5;
               then not c - b = -infty by SUPINF_1:6;
               then (c -b) + (b - a) = +infty by A15,SUPINF_2:def 2;
               hence thesis by A14,SUPINF_1:6,SUPINF_2:7;
            suppose
            A17:a = -infty & b in REAL & c = +infty;
            then A18:(c -b) + (b - a) = (c - b) + (+infty) by SUPINF_1:6,
SUPINF_2:7;
                 c - b = +infty by A17,SUPINF_1:2,SUPINF_2:6;
               then (c -b) + (b - a) = +infty by A18,SUPINF_1:14,SUPINF_2:def 2
;
               hence thesis by A17,SUPINF_1:14,SUPINF_2:7;
         end;
         hence thesis;
      suppose
      A19:a = +infty & b in REAL;
A20:     c in REAL or c in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
           now per cases by A1,A19,A20,TARSKI:def 2;
            suppose
            A21:a = +infty & b in REAL & c in REAL;
then A22:        (c -b) + (b - a) = (c - b) + (-infty) by SUPINF_1:2,SUPINF_2:6
;
               consider x,y being Real such that
            A23:x = c & y = b by A21;
              c - b = x - y by A23,SUPINF_2:5;
               then not c - b = +infty by SUPINF_1:2;
            then (c -b) + (b - a) = -infty by A22,SUPINF_2:def 2;
               hence thesis by A21,SUPINF_1:2,SUPINF_2:6;
            suppose
            A24:a = +infty & b in REAL & c = -infty;
            then A25:(c -b) + (b - a) = (c - b) + (-infty) by SUPINF_1:2,
SUPINF_2:6;
                 c - b = -infty by A24,SUPINF_1:6,SUPINF_2:7;
               then (c -b) + (b - a) = -infty by A25,SUPINF_1:14,SUPINF_2:def 2
;
               hence thesis by A24,SUPINF_1:14,SUPINF_2:6;
         end;
         hence thesis;
end;

theorem
     inf{a1,a2} <=' a1 & inf{a1,a2} <=' a2 &
   a1 <=' sup{a1,a2} & a2 <=' sup{a1,a2}
proof
     a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
   hence thesis by SUPINF_1:76,79;
end;

:: PROPERTIES OF THE INTERVALS

RSetEq {P[set]} : for X1,X2 being Subset of REAL st
 (for x being R_eal holds x in X1 iff P[x]) &
 (for x being R_eal holds x in X2 iff P[x]) holds X1 = X2
proof
   let A1,A2 be Subset of REAL such that
A1:for x being R_eal holds x in A1 iff P[x] and
A2:for x being R_eal holds x in A2 iff P[x];
   thus A1 c= A2
   proof
      let x be set;
      assume
   A3:x in A1;
      then x in REAL;
      then reconsider x as R_eal;
        P[x] by A1,A3;
      hence thesis by A2;
   end;
   let x be set;
   assume
A4:x in A2;
   then x in REAL;
   then reconsider x as R_eal;
     P[x] by A2,A4;
   hence thesis by A1;
end;

definition let a,b be R_eal;
  defpred P[R_eal] means a <=' $1 & $1 <=' b & $1 in REAL;
  func [.a,b.] -> Subset of REAL means
:Def1:for x being R_eal holds
      x in it iff a <=' x & x <=' b & x in REAL;
existence
proof
   consider A being Subset of REAL \/ {-infty,+infty} such that
A1:for x being R_eal holds x in A iff P[x] from SepR_eal;
     for x being set holds x in A implies x in REAL by A1,SUPINF_1:def 6;
   then reconsider A as Subset of REAL by TARSKI:def 3;
   take A;
   thus thesis by A1;
end;
uniqueness
 proof
  thus  for X1,X2 being Subset of REAL st
  (for x being R_eal holds x in X1 iff P[x]) &
  (for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
 end;

   defpred P[R_eal] means a <' $1 & $1 <' b & $1 in REAL;

   func ].a,b.[ -> Subset of REAL means
:Def2:for x being R_eal holds
      x in it iff (a <' x & x <' b & x in REAL);
existence
proof
   consider A being Subset of REAL \/ {-infty,+infty} such that
A2:for x being R_eal holds x in A iff P[x] from SepR_eal;
     for x being set holds x in A implies x in REAL by A2,SUPINF_1:def 6;
   then reconsider A as Subset of REAL by TARSKI:def 3;
   take A;
   thus thesis by A2;
end;
uniqueness
 proof
  thus  for X1,X2 being Subset of REAL st
  (for x being R_eal holds x in X1 iff P[x]) &
  (for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
 end;

   defpred P[R_eal] means a <' $1 & $1 <=' b & $1 in REAL;

  func ].a,b.] -> Subset of REAL means
:Def3:for x being R_eal holds
      x in it iff (a <' x & x <=' b & x in REAL);
existence
proof
   consider A being Subset of REAL \/ {-infty,+infty} such that
A3:for x being R_eal holds x in A iff P[x] from SepR_eal;
     for x being set holds x in A implies x in REAL by A3,SUPINF_1:def 6;
   then reconsider A as Subset of REAL by TARSKI:def 3;
   take A;
   thus thesis by A3;
end;
uniqueness
 proof
  thus  for X1,X2 being Subset of REAL st
  (for x being R_eal holds x in X1 iff P[x]) &
  (for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
 end;

   defpred P[R_eal] means a <=' $1 & $1 <' b & $1 in REAL;

 func [.a,b.[ -> Subset of REAL means
:Def4:for x being R_eal holds
      x in it iff (a <=' x & x <' b & x in REAL);
existence
proof
   consider A being Subset of REAL \/ {-infty,+infty} such that
A4:for x being R_eal holds x in A iff P[x] from SepR_eal;
     for x being set holds x in A implies x in REAL by A4,SUPINF_1:def 6;
   then reconsider A as Subset of REAL by TARSKI:def 3;
   take A;
   thus thesis by A4;
end;
uniqueness
 proof
  thus  for X1,X2 being Subset of REAL st
  (for x being R_eal holds x in X1 iff P[x]) &
  (for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
 end;
end;

definition let IT be Subset of REAL;
  attr IT is open_interval means
:Def5:  ex a,b being R_eal st a <=' b & IT = ].a,b.[;
  attr IT is closed_interval means
:Def6:ex a,b being R_eal st a <=' b & IT = [.a,b.];
end;

definition
  cluster open_interval Subset of REAL;
existence
proof
   consider a,b being R_eal such that
A1:a = -infty & b = +infty;
   take ].a,b.[, a,b;
   thus thesis by A1,SUPINF_1:20;
end;
  cluster closed_interval Subset of REAL;
existence
proof
   consider a,b being R_eal such that
A2:a = -infty & b = +infty;
   take [.a,b.],a,b;
   thus thesis by A2,SUPINF_1:20;
end;
end;

definition let IT be Subset of REAL;
  attr IT is right_open_interval means
:Def7:  ex a,b being R_eal st a <=' b & IT = [.a,b.[;
  synonym IT is left_closed_interval;
end;

definition let IT be Subset of REAL;
  attr IT is left_open_interval means
:Def8:ex a,b being R_eal st a <=' b & IT = ].a,b.];
 synonym IT is right_closed_interval;
end;

definition
  cluster right_open_interval Subset of REAL;
existence
proof
   consider a,b being R_eal such that
A1:a = -infty & b = +infty;
   take [.a,b.[,a,b;
   thus thesis by A1,SUPINF_1:20;
end;
  cluster left_open_interval Subset of REAL;
existence
proof
   consider a,b being R_eal such that
A2:a = -infty & b = +infty;
   take ].a,b.],a,b;
   thus thesis by A2,SUPINF_1:20;
end;
end;

definition let IT be Subset of REAL;
  attr IT is interval means
:Def9:IT is open_interval or IT is closed_interval or
      IT is right_open_interval or IT is left_open_interval;
end;

definition
  cluster interval Subset of REAL;
existence
proof
   consider I being open_interval Subset of REAL;
   take I;
   thus I is open_interval or I is closed_interval
     or I is right_open_interval or I is left_open_interval;
end;
end;

definition
  mode Interval is interval Subset of REAL;
end;

 reserve A,B for Interval;

definition
  cluster open_interval -> interval Subset of REAL;
coherence by Def9;
  cluster closed_interval -> interval Subset of REAL;
coherence by Def9;
  cluster right_open_interval -> interval Subset of REAL;
coherence by Def9;
  cluster left_open_interval -> interval Subset of REAL;
coherence by Def9;
end;

canceled;

theorem Th11:
   for x being set,
       a,b being R_eal st
   (x in ].a,b.[ or x in [.a,b.] or x in [.a,b.[ or x in ].a,b.]) holds
   x is R_eal
proof
   let x be set,
       a,b be R_eal;
   assume x in ].a,b.[ or x in [.a,b.] or x in [.a,b.[ or x in ].a,b.];
   then x in REAL;
   hence thesis;
end;

theorem Th12:
   for a,b being R_eal st b <' a holds
   ].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {}
proof
   let a,b be R_eal;
   assume
A1:b <' a;
   thus ].a,b.[ = {}
   proof assume
A2: not thesis;
    consider x being Element of ].a,b.[;
    reconsider x as R_eal by A2,Th11;
      b <=' a & b <> a & a <=' x & x <=' b by A1,A2,Def2;
    then b <=' a & b <> a & a <=' b by SUPINF_1:29;
    hence thesis by SUPINF_1:22;
   end;
   thus [.a,b.] = {}
   proof assume
A3: not thesis;
    consider x being Element of [.a,b.];
    reconsider x as R_eal by A3,Th11;
      b <=' a & b <> a & a <=' x & x <=' b by A1,A3,Def1;
    then b <=' a & b <> a & a <=' b by SUPINF_1:29;
    hence thesis by SUPINF_1:22;
   end;
   thus [.a,b.[ = {}
   proof assume
A4: not thesis;
    consider x being Element of [.a,b.[;
    reconsider x as R_eal by A4,Th11;
      b <=' a & b <> a & a <=' x & x <=' b by A1,A4,Def4;
    then b <=' a & b <> a & a <=' b by SUPINF_1:29;
    hence thesis by SUPINF_1:22;
   end;
   assume
A5: not thesis;
    consider x being Element of ].a,b.];
    reconsider x as R_eal by A5,Th11;
      b <=' a & b <> a & a <=' x & x <=' b by A1,A5,Def3;
    then b <=' a & b <> a & a <=' b by SUPINF_1:29;
    hence thesis by SUPINF_1:22;
end;

theorem Th13:
   for a being R_eal holds
   ].a,a.[ = {} & [.a,a.[ = {} & ].a,a.] = {}
proof
   let a be R_eal;
   thus ].a,a.[ = {}
   proof assume
A1: not thesis;
    consider x being Element of ].a,a.[;
    reconsider x as R_eal by A1,Th11;
      a <=' x & x <=' a & x <> a by A1,Def2;
    hence thesis by SUPINF_1:22;
   end;
   thus [.a,a.[ = {}
   proof assume
A2: not thesis;
    consider x being Element of [.a,a.[;
    reconsider x as R_eal by A2,Th11;
      a <=' x & x <=' a & x <> a by A2,Def4;
    hence thesis by SUPINF_1:22;
   end;
   assume
A3:not thesis;
   consider x being Element of ].a,a.];
   reconsider x as R_eal by A3,Th11;
     a <=' x & x <=' a & x <> a by A3,Def3;
   hence thesis by SUPINF_1:22;
end;

theorem Th14:
   for a being R_eal holds
   ((a = -infty or a = +infty) implies [.a,a.] = {}) &
   ((a <> -infty & a <> +infty) implies [.a,a.] = {a})
proof
   let a be R_eal;
   thus (a = -infty or a = +infty) implies [.a,a.] = {}
   proof
      assume
   A1:a = -infty or a = +infty;
    assume
A2:  not thesis;
      per cases by A1;
      suppose
      A3:a = -infty;
        consider x being Element of [.a,a.];
        reconsider x as R_eal by A2,Th11;
          a <=' x & x <=' a & x in REAL by A2,Def1;
        hence thesis by A3,SUPINF_1:6,22;
      suppose
      A4:a = +infty;
        consider x being Element of [.a,a.];
        reconsider x as R_eal by A2,Th11;
          a <=' x & x <=' a & x in REAL by A2,Def1;
        hence thesis by A4,SUPINF_1:2,22;
   end;
   assume
A5:a <> -infty & a <> +infty;
        for x being set holds x in [.a,a.] iff x = a
      proof
         let x be set;
         hereby assume
         A6:x in [.a,a.];
          then reconsider x' = x as R_eal by Th11;
            a <=' x' & x' <=' a & x in REAL by A6,Def1;
          hence x = a by SUPINF_1:22;
         end;
         assume
      A7:x = a;
         then reconsider x as R_eal;
           x is Real by A5,A7,MEASURE3:2;
         hence thesis by A7,Def1;
      end;
      hence thesis by TARSKI:def 1;
end;

theorem Th15:
   for a,b being R_eal st b <=' a holds
   ].a,b.[ = {} & [.a,b.[ = {} & ].a,b.] = {} &
    [.a,b.] c= {a} & [.a,b.] c= {b}
proof
   let a,b be R_eal;
   assume
A1:b <=' a;
   thus ].a,b.[ = {} & [.a,b.[ = {} & ].a,b.] = {}
   proof
      per cases;
      suppose b <> a; then b <' a by A1,SUPINF_1:22;hence thesis by Th12;
      suppose b = a;hence thesis by Th13;
   end;
   thus [.a,b.] c= {a}
   proof
      per cases;
      suppose b <> a; then b <' a by A1,SUPINF_1:22;
         then [.a,b.] = {} by Th12;
         hence thesis by XBOOLE_1:2;
      suppose
      A2:b = a;
         thus [.a,b.] c= {a}
         proof
            per cases;
            suppose a = -infty or a = +infty;
               then [.a,b.] = {} by A2,Th14;
               hence thesis by XBOOLE_1:2;
            suppose a <> -infty & a <> +infty;
               hence thesis by A2,Th14;
         end;
   end;
   per cases;
   suppose b <> a; then b <' a by A1,SUPINF_1:22;
   then [.a,b.] = {} by Th12;
   hence thesis by XBOOLE_1:2;
   suppose
   A3:b = a;
   thus [.a,b.] c= {b}
   proof
      per cases;
      suppose b = -infty or b = +infty;
      then [.a,b.] = {} by A3,Th14;
      hence thesis by XBOOLE_1:2;
      suppose b <> -infty & b <> +infty; hence thesis by A3,Th14;
   end;
end;

theorem
     for a,b,c being R_eal st a <' b & b <' c holds b in REAL
proof
   let a,b,c be R_eal;
   assume
A1:a <' b & b <' c;
then A2:b <> -infty by SUPINF_1:21;
     b <> +infty by A1,SUPINF_1:20;
   then b is Real by A2,MEASURE3:2;
   hence thesis;
end;

theorem Th17:
   for a,b being R_eal st a <' b
   ex x being R_eal st a <' x & x <' b & x in REAL
proof
   let a,b be R_eal;
   assume
A1:a <' b;
A2:(a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty})
       by SUPINF_1:def 6,XBOOLE_0:def 2;
A3:   not a = +infty & not b = -infty
      proof
         assume a = +infty or b = -infty;
         hence thesis by A1,SUPINF_1:23,24;
      end;
      per cases by A2,A3,TARSKI:def 2;
      suppose a in REAL & b in REAL;
      then consider x,y being Real such that
      A4:x = a & y = b & x<=y by A1,SUPINF_1:16;
           x<y by A1,A4,REAL_1:def 5;
         then consider z being real number such that
      A5:x<z & z<y by REAL_1:75;
         reconsider z as Real by XREAL_0:def 1;
         reconsider o = z as R_eal by SUPINF_1:10;
         take o;
           o in REAL & a <=' o & o <=' b & a <> o & o <> b
         by A4,A5,SUPINF_1:def 7;
         hence thesis by SUPINF_1:22;
      suppose
      A6:a in REAL & b = +infty;
         then reconsider x = a as Real;
         consider z being real number such that
      A7:x<z by REAL_1:76;
         reconsider z as Real by XREAL_0:def 1;
         reconsider o = z as R_eal by SUPINF_1:10;
         take o;
           o in REAL & a <=' o & a <> o by A7,SUPINF_1:def 7;
         hence thesis by A6,SUPINF_1:22,31;
      suppose
      A8:a = -infty & b in REAL;
         then reconsider y = b as Real;
         consider z being real number such that
      A9:z<y by REAL_1:77;
         reconsider z as Real by XREAL_0:def 1;
         reconsider o = z as R_eal by SUPINF_1:10;
         take o;
           o in REAL & o <=' b & o <> b by A9,SUPINF_1:def 7;
         hence thesis by A8,SUPINF_1:22,31;
      suppose
      A10:a = -infty & b = +infty;
         take 0.;
         thus thesis by A10,SUPINF_1:31,SUPINF_2:def 1;
end;

theorem Th18:
   for a,b,c being R_eal st a <' b & a <' c
   ex x being R_eal st a <' x & x <' b & x <' c & x in REAL
proof
   let a,b,c be R_eal;
   assume
A1:a <' b & a <' c;
        b <=' c or c <=' b;
      then a <' inf{b,c} by A1,SUPINF_1:96;
      then consider x being R_eal such that
   A2:a <' x & x <' inf{b,c} & x in REAL by Th17;
        ex o being R_eal st o in {b,c} & o <=' b
      proof
         take b;
         thus thesis by TARSKI:def 2;
      end;
   then A3:inf{b,c} <=' b by SUPINF_1:98;
        ex o being R_eal st (o in {b,c} & o <=' c)
      proof
         take c;
         thus thesis by TARSKI:def 2;
      end;
   then A4:inf{b,c} <=' c by SUPINF_1:98;
      take x;
      thus thesis by A2,A3,A4,SUPINF_1:29;
end;

theorem Th19:
   for a,b,c being R_eal st a <' c & b <' c
   ex x being R_eal st a <' x & b <' x & x <' c & x in REAL
proof
   let a,b,c be R_eal;
   assume
A1:a <' c & b <' c;
     a <=' b or b <=' a;
   then sup{a,b} <' c by A1,SUPINF_1:93;
   then consider x being R_eal such that
A2:sup{a,b} <' x & x <' c & x in REAL by Th17;
   take x;
     a in {a,b} & b in {a,b} by TARSKI:def 2;
   hence thesis by A2,SUPINF_1:97;
end;

theorem Th20:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ & not x in ].a2,b2.[) or
                         (not x in ].a1,b1.[ & x in ].a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in ].a2,b2.[) or (not x in ].a1,b1.[ & x in ].a2,b2.[))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in ].a1,b1.[ by A3,Def2;
         not x in ].a2,b2.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1;hence thesis by A2;
   suppose
    a2 <' b2;
         then consider x being R_eal such that
     A5:a2 <' x & x <' b2 & x in REAL by Th17;
        now per cases;
      suppose a1 <' b1;hence thesis by A2;
      suppose b1 <=' a1;
         then not x in ].a1,b1.[ & x in ].a2,b2.[ by A5,Def2,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th21:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ &
   not x in ].a2,b2.[) or (not x in ].a1,b1.[ & x in ].a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in ].a2,b2.[) or (not x in ].a1,b1.[ & x in ].a2,b2.[))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in ].a2,b2.[ by A3,Def2;
        not x in ].a1,b1.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2;hence thesis by A2;
      suppose
A6:      b2 <=' a2;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in ].a1,b1.[ & not x in].a2,b2.[ by A6,A7,Def2,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th22:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.] &
   not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in [.a1,b1.] by A3,Def1;
        not x in ].a2,b2.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose a2 <' b2;
    then consider x being R_eal such that
     A5:a2 <' x & x <' b2 & x in REAL by Th17;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: [.a1,b1.] c= {a1} by Th15;
      A7:x in ].a2,b2.[ by A5,Def2;
           not x in [.a1,b1.] by A1,A5,A6,TARSKI:def 1;
         hence thesis by A7;
      end;
      hence thesis;
end;

theorem Th23:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.] &
   not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in ].a2,b2.[ by A3,Def2;
        not x in [.a1,b1.] by A3,Def1;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2; hence thesis by A2;
      suppose
A6:      b2 <=' a2;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in [.a1,b1.] & not x in].a2,b2.[ by A6,A7,Def1,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th24:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in ].a1,b1.[ by A3,Def2;
        not x in [.a2,b2.] by A3,Def1;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: ].a1,b1.[ = {} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
           x in [.a2,b2.] by A7,Def1;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th25:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in [.a2,b2.] by A3,Def1;
        not x in ].a1,b1.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2; hence thesis by A2;
      suppose b2 <=' a2;
      then A6: [.a2,b2.] c= {b2} by Th15;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
     A8:x in ].a1,b1.[ by A7,Def2;
           not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
         hence thesis by A8;
      end;
      hence thesis;
end;

theorem Th26:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in ].a1,b1.[ by A3,Def2;
        not x in [.a2,b2.[ by A3,Def4;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: ].a1,b1.[ = {} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
       x in [.a2,b2.[ by A7,Def4;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th27:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in [.a2,b2.[ by A3,Def4;
        not x in ].a1,b1.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2; hence thesis by A2;
      suppose b2 <=' a2;
      then A6: [.a2,b2.[ = {} by Th15;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
       x in ].a1,b1.[ by A7,Def2;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th28:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.[ &
   not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in [.a1,b1.[ by A3,Def4;
        not x in ].a2,b2.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: [.a1,b1.[ = {} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
           x in ].a2,b2.[ by A7,Def2;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th29:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.[ &
   not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in ].a2,b2.[ by A3,Def2;
        not x in [.a1,b1.[ by A3,Def4;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2; hence thesis by A2;
      suppose
A6:      b2 <=' a2;
         consider x being R_eal such that
      A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in [.a1,b1.[ & not x in].a2,b2.[ by A6,A7,Def4,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th30:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ &
   not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in ].a1,b1.[ by A3,Def2;
        not x in ].a2,b2.] by A3,Def3;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: ].a1,b1.[ = {} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
       x in ].a2,b2.] by A7,Def3;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th31:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.[ &
   not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
   not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in ].a2,b2.] by A3,Def3;
        not x in ].a1,b1.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2; hence thesis by A2;
      suppose b2 <=' a2;
      then A6: ].a2,b2.] = {} by Th15;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in ].a1,b1.[ by A7,Def2;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th32:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in ].a1,b1.] by A3,Def3;
        not x in ].a2,b2.[ by A3,Def2;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: ].a1,b1.] = {} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
           x in ].a2,b2.[ by A7,Def2;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th33:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in ].a2,b2.[ by A3,Def2;
        not x in ].a1,b1.] by A3,Def3;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2;
         hence thesis by A2;
      suppose
A6:      b2 <=' a2;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in ].a1,b1.] & not x in].a2,b2.[ by A6,A7,Def3,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th34:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in [.a1,b1.] by A3,Def1;
        not x in [.a2,b2.] by A3,Def1;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: [.a1,b1.] c= {a1} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
     A8:x in [.a2,b2.] by A7,Def1;
           not x in [.a1,b1.] by A1,A6,A7,TARSKI:def 1;
         hence thesis by A8;
      end;
      hence thesis;
end;

theorem Th35:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in [.a2,b2.] by A3,Def1;
        not x in [.a1,b1.] by A3,Def1;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2;
         hence thesis by A2;
      suppose b2 <=' a2;
      then A6: [.a2,b2.] c= {b2} by Th15;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
     A8:x in [.a1,b1.] by A7,Def1;
           not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
         hence thesis by A8;
      end;
      hence thesis;
end;

theorem Th36:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in [.a1,b1.] by A3,Def1;
        not x in [.a2,b2.[ by A3,Def4;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1; hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1; hence thesis by A2;
      suppose b1 <=' a1;
      then A6: [.a1,b1.] c= {a1} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
     A8:x in [.a2,b2.[ by A7,Def4;
           not x in [.a1,b1.] by A1,A6,A7,TARSKI:def 1;
         hence thesis by A8;
      end;
      hence thesis;
end;

theorem Th37:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.] &
   not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in [.a2,b2.[ by A3,Def4;
        not x in [.a1,b1.] by A3,Def1;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2;
      hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2; hence thesis by A2;
      suppose
A6:      b2 <=' a2;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in [.a1,b1.] & not x in [.a2,b2.[ by A6,A7,Def1,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th38:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.[ &
   not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in [.a1,b1.[ by A3,Def4;
        not x in [.a2,b2.] by A3,Def1;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1;
      hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1;
         hence thesis by A2;
      suppose b1 <=' a1;
      then A6: [.a1,b1.[ = {} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
           x in [.a2,b2.] by A7,Def1;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th39:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a2 <' b2;
      then consider x being R_eal such that
   A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A3:x in [.a2,b2.] by A2,Def1;
        not x in [.a1,b1.[ by A2,Def4;
      hence thesis by A3;
   suppose that
A4: a1 <' b1 and
A5: b2 <=' a2;
     A6: [.a2,b2.] c= {b2} by A5,Th15;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A4,Th17;
     A8:x in [.a1,b1.[ by A7,Def4;
           not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
         hence thesis by A8;
end;

theorem Th40:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in ].a2,b2.]) or (not x in [.a1,b1.] & x in ].a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a1 <' b1;
      then consider x being R_eal such that
   A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A3:x in [.a1,b1.] by A2,Def1;
        not x in ].a2,b2.] by A2,Def3;
      hence thesis by A3;
   suppose that
A4: a2 <' b2 and
A5: b1 <=' a1;
      A6: [.a1,b1.] c= {a1} by A5,Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
     A8:x in ].a2,b2.] by A7,Def3;
           not x in [.a1,b1.] by A1,A6,A7,TARSKI:def 1;
         hence thesis by A8;
end;

theorem Th41:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.] &
   not x in ].a2,b2.]) or (not x in [.a1,b1.] & x in ].a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a2 <' b2;
      then consider x being R_eal such that
   A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A3:x in ].a2,b2.] by A2,Def3;
        not x in [.a1,b1.] by A2,Def1;
      hence thesis by A3;
   suppose that
A4:a1 <' b1 and
A5: b2 <=' a2;
         consider x being R_eal such that
     A6:a1 <' x & x <' b1 & x in REAL by A4,Th17;
            x in [.a1,b1.] & not x in ].a2,b2.] by A5,A6,Def1,Th15;
         hence thesis;
end;

theorem Th42:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in [.a2,b2.]) or (not x in ].a1,b1.] & x in [.a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a1 <' b1;
      then consider x being R_eal such that
   A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A3:x in ].a1,b1.] by A2,Def3;
        not x in [.a2,b2.] by A2,Def1;
      hence thesis by A3;
   suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
      A6: ].a1,b1.] = {} by A5,Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
           x in [.a2,b2.] by A7,Def1;
         hence thesis by A6;
end;

theorem Th43:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in [.a2,b2.]) or (not x in ].a1,b1.] & x in [.a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a2 <' b2;
      then consider x being R_eal such that
   A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A3:x in [.a2,b2.] by A2,Def1;
        not x in ].a1,b1.] by A2,Def3;
      hence thesis by A3;
   suppose that
A4: a1 <' b1 and
A5: b2 <=' a2;
     A6: [.a2,b2.] c= {b2} by A5,Th15;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A4,Th17;
     A8:x in ].a1,b1.] by A7,Def3;
           not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
         hence thesis by A8;
end;

theorem Th44:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in [.a2,b2.[) or (not x in [.a1,b1.[ & x in [.a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a1 <' b1;
      then consider x being R_eal such that
   A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A3:x in [.a1,b1.[ by A2,Def4;
        not x in [.a2,b2.[ by A2,Def4;
      hence thesis by A3;
   suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
      A6:[.a1,b1.[ = {} by A5,Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
       x in [.a2,b2.[ by A7,Def4;
         hence thesis by A6;
end;

theorem Th45:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in [.a2,b2.[) or (not x in [.a1,b1.[ & x in [.a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a2 <' b2;
      then consider x being R_eal such that
   A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A3:x in [.a2,b2.[ by A2,Def4;
        not x in [.a1,b1.[ by A2,Def4;
      hence thesis by A3;
   suppose that
A4:a1 <' b1 and
A5: b2 <=' a2;
      consider x being R_eal such that
   A6:a1 <' x & x <' b1 & x in REAL by A4,Th17;
        x in [.a1,b1.[ & not x in [.a2,b2.[ by A5,A6,Def4,Th15;
      hence thesis;
end;

theorem Th46:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in ].a2,b2.]) or (not x in [.a1,b1.[ & x in ].a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a1 <' b1;
      then consider x being R_eal such that
   A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A3:x in [.a1,b1.[ by A2,Def4;
        not x in ].a2,b2.] by A2,Def3;
      hence thesis by A3;
   suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
      A6: [.a1,b1.[ = {} by A5,Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
       x in ].a2,b2.] by A7,Def3;
         hence thesis by A6;
end;

theorem Th47:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in [.a1,b1.[ &
   not x in ].a2,b2.]) or (not x in [.a1,b1.[ & x in ].a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a2 <' b2;
      then consider x being R_eal such that
   A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A3:x in ].a2,b2.] by A2,Def3;
        not x in [.a1,b1.[ by A2,Def4;
      hence thesis by A3;
   suppose that
A4:a1 <' b1 and
A5:      b2 <=' a2;
         consider x being R_eal such that
     A6:a1 <' x & x <' b1 & x in REAL by A4,Th17;
           x in [.a1,b1.[ & not x in ].a2,b2.] by A5,A6,Def4,Th15;
         hence thesis;
end;

theorem Th48:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
   per cases by A1;
   suppose a1 <' b1;
      then consider x being R_eal such that
   A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A3:x in ].a1,b1.] by A2,Def3;
        not x in [.a2,b2.[ by A2,Def4;
      hence thesis by A3;
   suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
      A6: ].a1,b1.] = {} by A5,Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
           x in [.a2,b2.[ by A7,Def4;
         hence thesis by A6;
end;

theorem Th49:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.] &
   not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in [.a2,b2.[ by A3,Def4;
        not x in ].a1,b1.] by A3,Def3;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2; hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2; hence thesis by A2;
      suppose
A6:      b2 <=' a2;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in ].a1,b1.] & not x in [.a2,b2.[ by A6,A7,Def3,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th50:
   a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
proof
   assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
   proof
      assume a1 <' b1;
      then consider x being R_eal such that
   A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
   A4:x in ].a1,b1.] by A3,Def3;
        not x in ].a2,b2.] by A3,Def3;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a1 <' b1;
      hence thesis by A2;
   suppose
   A5:a2 <' b2;
        now per cases;
      suppose a1 <' b1;
         hence thesis by A2;
      suppose b1 <=' a1;
      then A6: ].a1,b1.] = {} by Th15;
         consider x being R_eal such that
     A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
           x in ].a2,b2.] by A7,Def3;
         hence thesis by A6;
      end;
      hence thesis;
end;

theorem Th51:
   b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
   ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
proof
   assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.] &
   not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
   proof
      assume a2 <' b2;
      then consider x being R_eal such that
   A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
   A4:x in ].a2,b2.] by A3,Def3;
        not x in ].a1,b1.] by A3,Def3;
      hence thesis by A4;
   end;
   per cases by A1;
   suppose a2 <' b2;
      hence thesis by A2;
   suppose
   A5:a1 <' b1;
        now per cases;
      suppose a2 <' b2;
         hence thesis by A2;
      suppose
A6:      b2 <=' a2;
         consider x being R_eal such that
     A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
           x in ].a1,b1.] & not x in ].a2,b2.] by A6,A7,Def3,Th15;
         hence thesis;
      end;
      hence thesis;
end;

theorem Th52:
   (a1 <' b1 &
   ((A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.]) &
   (A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.])))
   implies (a1 = a2 & b1 = b2)
proof assume that
A1: a1 <' b1 and
A2: A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.] and
A3: A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.];
 per cases;
 suppose
A4: A = ].a1,b1.[ & A = ].a2,b2.[;
 thus a1 = a2 & b1 = b2
proof
   assume
A5:a1 <> a2 or b1 <> b2;
   per cases by A5;
   suppose
A6:      a1 <> a2;
        now per cases by A6,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in ].a1,b1.[ &
         not x in ].a2,b2.[) or (not x in ].a1,b1.[ &
         x in ].a2,b2.[)) by A1,Th20;
         hence thesis by A4;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in ].a2,b2.[ &
         not x in ].a1,b1.[) or (not x in ].a2,b2.[ &
         x in ].a1,b1.[)) by A1,Th20;
         hence thesis by A4;
      end;
      hence thesis;
   suppose A7: b1 <> b2;
        now per cases by A7,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st (x in ].a1,b1.[ &
         not x in ].a2,b2.[) or (not x in ].a1,b1.[ &
         x in ].a2,b2.[) by A1,Th21;
         hence thesis by A4;
      suppose b2 <' b1;
         then ex x being R_eal st (x in ].a2,b2.[ &
         not x in ].a1,b1.[) or (not x in ].a2,b2.[ &
         x in ].a1,b1.[) by A1,Th21;
         hence thesis by A4;
      end;
      hence thesis;
end;
 suppose
A8: A <> ].a1,b1.[ or A <> ].a2,b2.[;
A9: for a1,a2,b1,b2 holds
   (((a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.[) implies
   a1 = a2 & b1 = b2)
proof let a1,a2,b1,b2;
   assume that
A10:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.[ and
A11:a1 <> a2 or b1 <> b2;
   per cases by A11;
   suppose
A12:   a1 <> a2;
        now per cases by A12,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st (x in [.a1,b1.] &
         not x in ].a2,b2.[) or (not x in [.a1,b1.] &
         x in ].a2,b2.[) by A10,Th22;
         hence thesis by A10;
      suppose a2 <' a1;
         then ex x being R_eal st (x in ].a2,b2.[ &
         not x in [.a1,b1.]) or (not x in ].a2,b2.[ &
         x in [.a1,b1.]) by A10,Th24;
         hence thesis by A10;
      end;
      hence thesis;
   suppose A13: b1 <> b2;
        now per cases by A13,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st (x in [.a1,b1.] &
         not x in ].a2,b2.[) or (not x in [.a1,b1.] &
         x in ].a2,b2.[) by A10,Th23;
         hence thesis by A10;
      suppose b2 <' b1;
         then ex x being R_eal st (x in ].a2,b2.[ &
         not x in [.a1,b1.]) or (not x in ].a2,b2.[ &
         x in [.a1,b1.]) by A10,Th25;
         hence thesis by A10;
      end;
      hence thesis;
end;
A14: for a1,a2,b1,b2 holds
   (((a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = [.a2,b2.[) implies
   a1 = a2 & b1 = b2)
proof let a1,a2,b1,b2;
   assume that
A15:(a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = [.a2,b2.[ and
A16:a1 <> a2 or b1 <> b2;
   per cases by A16;
   suppose
A17:   a1 <> a2;
        now per cases by A17,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in ].a1,b1.[ &
         not x in [.a2,b2.[) or (not x in ].a1,b1.[ &
         x in [.a2,b2.[)) by A15,Th26;
         hence thesis by A15;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in [.a2,b2.[ &
         not x in ].a1,b1.[) or (not x in [.a2,b2.[ &
         x in ].a1,b1.[)) by A15,Th28;
         hence thesis by A15;
      end;
      hence thesis;
   suppose A18: b1 <> b2;
        now per cases by A18,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st ((x in ].a1,b1.[ &
         not x in [.a2,b2.[) or (not x in ].a1,b1.[ &
         x in [.a2,b2.[)) by A15,Th27;
         hence thesis by A15;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in [.a2,b2.[ &
         not x in ].a1,b1.[) or (not x in [.a2,b2.[ &
         x in ].a1,b1.[)) by A15,Th29;
         hence thesis by A15;
      end;
      hence thesis;
end;
A19:
  for a1,a2,b1,b2 holds
   ((a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = ].a2,b2.]) implies
   a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
   assume
A20:(a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = ].a2,b2.];
   assume
A21:a1 <> a2 or b1 <> b2;
   per cases by A21;
   suppose
A22:   a1 <> a2;
        now per cases by A22,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in ].a1,b1.[ &
         not x in ].a2,b2.]) or (not x in ].a1,b1.[ &
         x in ].a2,b2.])) by A20,Th30;
         hence thesis by A20;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in ].a2,b2.] &
         not x in ].a1,b1.[) or (not x in ].a2,b2.] &
         x in ].a1,b1.[)) by A20,Th32;
         hence thesis by A20;
      end;
      hence thesis;
   suppose A23: b1 <> b2;
        now per cases by A23,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st (((x in ].a1,b1.[) &
         not x in ].a2,b2.]) or (not x in ].a1,b1.[ &
         x in ].a2,b2.])) by A20,Th31;
         hence thesis by A20;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in ].a2,b2.] &
         not x in ].a1,b1.[) or (not x in ].a2,b2.] &
         x in ].a1,b1.[)) by A20,Th33;
         hence thesis by A20;
      end;
      hence thesis;
end;
A24:
   (A = [.a1,b1.] & A = [.a2,b2.]) implies
   a1 = a2 & b1 = b2
proof
   assume
A25: A = [.a1,b1.] & A = [.a2,b2.];
   assume
A26:a1 <> a2 or b1 <> b2;
   per cases by A26;
   suppose
A27:   a1 <> a2;
        now per cases by A27,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in [.a1,b1.] &
         not x in [.a2,b2.]) or (not x in [.a1,b1.] &
         x in [.a2,b2.])) by A1,Th34;
         hence thesis by A25;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in [.a2,b2.] &
         not x in [.a1,b1.]) or (not x in [.a2,b2.] &
         x in [.a1,b1.])) by A1,Th34;
         hence thesis by A25;
      end;
      hence thesis;
   suppose A28: b1 <> b2;
        now per cases by A28,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st ((x in [.a1,b1.] &
         not x in [.a2,b2.]) or (not x in [.a1,b1.] &
         x in [.a2,b2.])) by A1,Th35;
         hence thesis by A25;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in [.a2,b2.] &
         not x in [.a1,b1.]) or (not x in [.a2,b2.] &
         x in [.a1,b1.])) by A1,Th35;
         hence thesis by A25;
      end;
      hence thesis;
end;
A29: for a1,a2,b1,b2 holds
   ((a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = [.a2,b2.[) implies
   a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
   assume
A30:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = [.a2,b2.[;
   assume
A31:a1 <> a2 or b1 <> b2;
   per cases by A31;
   suppose
A32:   a1 <> a2;
        now per cases by A32,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in [.a1,b1.] &
         not x in [.a2,b2.[) or (not x in [.a1,b1.] &
         x in [.a2,b2.[)) by A30,Th36;
         hence thesis by A30;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in [.a2,b2.[ &
         not x in [.a1,b1.]) or (not x in [.a2,b2.[ &
         x in [.a1,b1.])) by A30,Th38;
         hence thesis by A30;
      end;
      hence thesis;
   suppose A33: b1 <> b2;
        now per cases by A33,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st ((x in [.a1,b1.] &
         not x in [.a2,b2.[) or (not x in [.a1,b1.] &
         x in [.a2,b2.[)) by A30,Th37;
         hence thesis by A30;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in [.a2,b2.[ &
         not x in [.a1,b1.]) or (not x in [.a2,b2.[ &
         x in [.a1,b1.])) by A30,Th39;
         hence thesis by A30;
      end;
      hence thesis;
end;
A34: for a1,a2,b1,b2 holds
   ((a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.]) implies
   a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
   assume
A35:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.];
   assume
A36:a1 <> a2 or b1 <> b2;
   per cases by A36;
   suppose
A37:   a1 <> a2;
        now per cases by A37,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in [.a1,b1.] &
         not x in ].a2,b2.]) or (not x in [.a1,b1.] &
         x in ].a2,b2.])) by A35,Th40;
         hence thesis by A35;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in ].a2,b2.] &
         not x in [.a1,b1.]) or (not x in ].a2,b2.] &
         x in [.a1,b1.])) by A35,Th42;
         hence thesis by A35;
      end;
      hence thesis;
   suppose A38: b1 <> b2;
        now per cases by A38,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st ((x in [.a1,b1.] &
         not x in ].a2,b2.]) or (not x in [.a1,b1.] &
         x in ].a2,b2.])) by A35,Th41;
         hence thesis by A35;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in ].a2,b2.] &
         not x in [.a1,b1.]) or (not x in ].a2,b2.] &
         x in [.a1,b1.])) by A35,Th43;
         hence thesis by A35;
      end;
      hence thesis;
end;
A39:
   (A = [.a1,b1.[ & A = [.a2,b2.[) implies a1 = a2 & b1 = b2
proof
   assume
A40: A = [.a1,b1.[ & A = [.a2,b2.[;
   assume
A41:a1 <> a2 or b1 <> b2;
   per cases by A41;
   suppose
A42:   a1 <> a2;
        now per cases by A42,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in [.a1,b1.[ &
         not x in [.a2,b2.[) or (not x in [.a1,b1.[ &
         x in [.a2,b2.[)) by A1,Th44;
         hence thesis by A40;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in [.a2,b2.[ &
         not x in [.a1,b1.[) or (not x in [.a2,b2.[ &
         x in [.a1,b1.[)) by A1,Th44;
         hence thesis by A40;
      end;
      hence thesis;
   suppose A43: b1 <> b2;
        now per cases by A43,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st ((x in [.a1,b1.[ &
         not x in [.a2,b2.[) or (not x in [.a1,b1.[ &
         x in [.a2,b2.[)) by A1,Th45;
         hence thesis by A40;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in [.a2,b2.[ &
         not x in [.a1,b1.[) or (not x in [.a2,b2.[ &
         x in [.a1,b1.[)) by A1,Th45;
         hence thesis by A40;
      end;
      hence thesis;
end;
A44: for a1,a2,b1,b2 holds
   ((a1 <' b1 or a2 <' b2) & A = [.a1,b1.[ & A = ].a2,b2.]) implies
   a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
   assume
A45:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.[ & A = ].a2,b2.];
   assume
A46:a1 <> a2 or b1 <> b2;
   per cases by A46;
   suppose
A47:   a1 <> a2;
        now per cases by A47,SUPINF_1:22;
        suppose a1 <' a2;
         then ex x being R_eal st ((x in [.a1,b1.[ &
         not x in ].a2,b2.]) or (not x in [.a1,b1.[ &
         x in ].a2,b2.])) by A45,Th46;
         hence thesis by A45;
        suppose a2 <' a1;
         then ex x being R_eal st ((x in ].a2,b2.] &
         not x in [.a1,b1.[) or (not x in ].a2,b2.] &
         x in [.a1,b1.[)) by A45,Th48;
         hence thesis by A45;
      end;
      hence thesis;
   suppose A48: b1 <> b2;
        now per cases by A48,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st ((x in [.a1,b1.[ &
         not x in ].a2,b2.]) or (not x in [.a1,b1.[ &
         x in ].a2,b2.])) by A45,Th47;
         hence thesis by A45;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in ].a2,b2.] &
         not x in [.a1,b1.[) or (not x in ].a2,b2.] &
         x in [.a1,b1.[)) by A45,Th49;
         hence thesis by A45;
      end;
      hence thesis;
end;
     (A = ].a1,b1.] & A = ].a2,b2.]) implies a1 = a2 & b1 = b2
proof
   assume
A49: A = ].a1,b1.] & A = ].a2,b2.];
   assume
A50:a1 <> a2 or b1 <> b2;
   per cases by A50;
   suppose
A51:   a1 <> a2;
        now per cases by A51,SUPINF_1:22;
      suppose a1 <' a2;
         then ex x being R_eal st ((x in ].a1,b1.] &
         not x in ].a2,b2.]) or (not x in ].a1,b1.] &
         x in ].a2,b2.])) by A1,Th50;
         hence thesis by A49;
      suppose a2 <' a1;
         then ex x being R_eal st ((x in ].a2,b2.] &
         not x in ].a1,b1.]) or (not x in ].a2,b2.] &
         x in ].a1,b1.])) by A1,Th50;
         hence thesis by A49;
      end;
      hence thesis;
   suppose A52: b1 <> b2;
        now per cases by A52,SUPINF_1:22;
      suppose b1 <' b2;
         then ex x being R_eal st ((x in ].a1,b1.] &
         not x in ].a2,b2.]) or (not x in ].a1,b1.] &
         x in ].a2,b2.])) by A1,Th51;
         hence thesis by A49;
      suppose b2 <' b1;
         then ex x being R_eal st ((x in ].a2,b2.] & not x in ].a1,b1.]) or
         (not x in ].a2,b2.] & x in ].a1,b1.])) by A1,Th51;
         hence thesis by A49;
      end;
      hence thesis;
end;
 hence thesis by A1,A2,A3,A8,A9,A14,A19,A24,A29,A34,A39,A44;
end;

definition let A be Interval;
  func vol A -> R_eal means
:Def10:ex a,b being R_eal st
       ((A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]) &
       (a <' b implies it = b - a) &
       (b <=' a implies it = 0.));
existence
proof
        A is open_interval or A is closed_interval or
      A is right_open_interval or A is left_open_interval by Def9;
      then (ex a,b being R_eal st (a <=' b & A = ].a,b.[)) or
      (ex a,b being R_eal st (a <=' b & A = [.a,b.])) or
      (ex a,b being R_eal st (a <=' b & A = [.a,b.[)) or
      (ex a,b being R_eal st (a <=' b & A = ].a,b.]))
      by Def5,Def6,Def7,Def8;
      then consider a,b being R_eal such that
   A1:A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.];
        b <=' a implies ex x being R_eal st
      ((a <' b implies x = b - a) & (b <=' a implies x = 0.));
      then ex x being R_eal st
      ((a <' b implies x = b - a) & (b <=' a implies x = 0.));
  hence thesis by A1;
end;
uniqueness
proof
   let x1,x2 be R_eal;
 given a1,b1 being R_eal such that
A2: ((A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.]) &
   (a1 <' b1 implies x1 = b1 - a1) &
   (b1 <=' a1 implies x1 = 0.));
 given a2,b2 being R_eal such that
A3: ((A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.]) &
   (a2 <' b2 implies x2 = b2 - a2) &
   (b2 <=' a2 implies x2 = 0.));
   per cases;
      suppose
        a1 <' b1 & a2 <' b2;
      then a1 = a2 & b1 = b2 by A2,A3,Th52;
         hence thesis by A2,A3;
      suppose
      A4:a1 <' b1 & b2 <=' a2;
         then a1 = a2 & b1 = b2 by A2,A3,Th52;
         hence thesis by A4;
      suppose
      A5:b1 <=' a1 & a2 <' b2;
         then a1 = a2 & b1 = b2 by A2,A3,Th52;
         hence thesis by A5;
      suppose b1 <=' a1 & b2 <=' a2;hence thesis by A2,A3;
end;
end;

theorem
     for A being open_interval Subset of REAL holds
   for a,b being R_eal holds
   A = ].a,b.[ implies
   ((a <' b implies vol(A) = b - a) &
   (b <=' a implies vol(A) = 0.)) by Def10;

theorem
     for A being closed_interval Subset of REAL holds
   for a,b being R_eal holds
   A = [.a,b.] implies
   ((a <' b implies vol(A) = b - a) &
   (b <=' a implies vol(A) = 0.)) by Def10;

theorem
     for A being right_open_interval Subset of REAL holds
   for a,b being R_eal holds
   A = [.a,b.[ implies
   ((a <' b implies vol(A) = b - a) &
   (b <=' a implies vol(A) = 0.)) by Def10;

theorem
     for A being left_open_interval Subset of REAL holds
   for a,b being R_eal holds
   A = ].a,b.] implies
   ((a <' b implies vol(A) = b - a) &
   (b <=' a implies vol(A) = 0.)) by Def10;

theorem
     for a,b,c being R_eal holds
   (a = -infty & b in REAL & c = +infty &
   (A = ].a,b.[ or A = ].b,c.[ or A = [.a,b.] or A = [.b,c.] or
    A = [.a,b.[ or A = [.b,c.[ or A = ].a,b.] or A = ].b,c.]))
   implies vol(A) = +infty
proof
   let a,b,c be R_eal;
   assume
A1:a = -infty & b in REAL & c = +infty &
   (A = ].a,b.[ or A = ].b,c.[ or A = [.a,b.] or A = [.b,c.] or
    A = [.a,b.[ or A = [.b,c.[ or A = ].a,b.] or A = ].b,c.]);
   per cases by A1;
   suppose A = ].a,b.[;
   then A = ].a,b.[ & a <' b by A1,SUPINF_1:31;
   then vol(A) = b - a by Def10;
   hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
   suppose A = ].b,c.[;
   then A = ].b,c.[ & b <' c by A1,SUPINF_1:31;
then A2:vol(A) = c - b by Def10;
     not ((c = +infty & b = +infty) or (c = -infty & b = -infty
)) by A1,SUPINF_1:def 1;
   hence thesis by A1,A2,SUPINF_2:6;
   suppose A3:A = [.a,b.];
     a <' b by A1,SUPINF_1:31;
   then vol(A) = b - a by A3,Def10;
   hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
   suppose A4:A = [.b,c.];
     b <' c by A1,SUPINF_1:31;
then A5:vol(A) = c - b by A4,Def10;
     not ((c = +infty & b = +infty) or (c = -infty & b = -infty
)) by A1,SUPINF_1:def 1;
   hence thesis by A1,A5,SUPINF_2:6;
   suppose A6:A = [.a,b.[;
     a <' b by A1,SUPINF_1:31;
   then vol(A) = b - a by A6,Def10;
   hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
   suppose A = [.b,c.[;
   then A = [.b,c.[ & b <' c by A1,SUPINF_1:31;
then A7:vol(A) = c - b by Def10;
     not ((c = +infty & b = +infty) or (c = -infty & b = -infty))
   by A1,SUPINF_1:def 1;
   hence thesis by A1,A7,SUPINF_2:6;
   suppose A = ].a,b.];
   then A = ].a,b.] & a <' b by A1,SUPINF_1:31;
    then vol(A) = b - a by Def10;
   hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
   suppose A = ].b,c.];
   then A = ].b,c.] & b <' c by A1,SUPINF_1:31;
then A8:vol(A) = c - b by Def10;
     not ((c = +infty & b = +infty) or (c = -infty & b = -infty))
   by A1,SUPINF_1:def 1;
   hence thesis by A1,A8,SUPINF_2:6;
end;

theorem
     for a,b being R_eal holds
   (a = -infty & b = +infty &
   (A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]))
   implies vol(A) = +infty
proof
   let a,b be R_eal;
   assume
A1:a = -infty & b = +infty &
   (A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]);
then a <' b by SUPINF_1:29,SUPINF_2:19;
   then vol(A) = b - a by A1,Def10
         .= +infty by A1,SUPINF_1:14,SUPINF_2:6;
   hence thesis;
end;

definition
  cluster empty Interval;
  existence
 proof
     {} is open_interval Subset of REAL
   proof
         ex a,b being R_eal st a <=' b & {} = ].a,b.[
       proof
          consider c being R_eal;
          consider a,b being R_eal such that
       A1:a = c & b = c;
          take a,b;
          thus thesis by A1,Th13;
       end;
       hence thesis by Def5;
   end;
   hence thesis;
 end;
end;

definition
  redefine func {} -> empty Interval;
coherence
proof
     {} is open_interval Subset of REAL
   proof
       ex a,b being R_eal st (a <=' b & {} = ].a,b.[)
     proof
        consider c being R_eal;
        consider a,b being R_eal such that
     A1:a = c & b = c;
        take a,b;
        thus thesis by A1,Th13;
     end;
     hence thesis by Def5;
   end;
   hence thesis;
end;
end;

canceled;

theorem Th60:
   vol {} = 0.
proof
     {} = ].0.,0..[ by Th13;
   hence thesis by Def10;
end;

theorem Th61:
   (A c= B & B =[.a,b.] & b <=' a) implies
   (vol(A) = 0. & vol(B) = 0.)
proof
   assume
A1:A c= B & B =[.a,b.] & b <=' a;
     A is open_interval or A is closed_interval or
   A is right_open_interval or A is left_open_interval by Def9;
   then (ex c,d being R_eal st (c <=' d & A = ].c,d.[)) or
   (ex c,d being R_eal st (c <=' d & A = [.c,d.])) or
   (ex c,d being R_eal st (c <=' d & A = [.c,d.[)) or
   (ex c,d being R_eal st (c <=' d & A = ].c,d.]))
   by Def5,Def6,Def7,Def8;
   then consider c,d being R_eal such that
A2:c <=' d &
   (A = ].c,d.[ or A = [.c,d.] or A = [.c,d.[ or A = ].c,d.]);
     c <' d implies vol(A) = 0.
   proof
      assume
   A3:c <' d;
        B c= {a} by A1,Th15;
   then A4:A c= {a} by A1,XBOOLE_1:1;
      per cases by A2;
         suppose
         A5:A = ].c,d.[;
              A = {}
            proof
               assume
A6:        A <> {};
               consider x being Element of A;
                 A c= ExtREAL by XBOOLE_1:1;
               then reconsider x as R_eal by A6,TARSKI:def 3;
           A7:c <' x & x <' d & x in REAL by A5,A6,Def2;
                 x in {a} by A4,A6,TARSKI:def 3;
           then A8:x = a by TARSKI:def 1;
               consider y being R_eal such that
           A9:c <' y & y <' x & y in REAL by A7,Th17;
                 y <' d by A7,A9,SUPINF_1:29;
               then y in A by A5,A9,Def2; hence thesis by A4,A8,A9,TARSKI:def 1
;
            end;
            hence thesis by Th60;
            suppose
         A10:A = [.c,d.];
            consider x being R_eal such that
        A11:c <' x & x <' d & x in REAL by A3,Th17;
              x in A by A10,A11,Def1;
        then A12:x = a by A4,TARSKI:def 1;
            consider y being R_eal such that
        A13:c <' y & y <' x & y in REAL by A11,Th17;
              c <=' y & y <=' d & y in REAL by A11,A13,SUPINF_1:29;
        then y in A by A10,Def1; hence thesis by A4,A12,A13,TARSKI:def 1;
         suppose
        A14:A = [.c,d.[;
              A = {}
            proof
               assume
A15:       A <> {};
               consider x being Element of A;
                 A c= ExtREAL by XBOOLE_1:1;
               then reconsider x as R_eal by A15,TARSKI:def 3;
           A16:c <=' x & x <' d & x in REAL by A14,A15,Def4;
                 x in {a} by A4,A15,TARSKI:def 3;
           then A17:x = a by TARSKI:def 1;
               consider y being R_eal such that
           A18:x <' y & y <' d & y in REAL by A16,Th17;
                 c <=' y by A16,A18,SUPINF_1:29;
               then y in A by A14,A18,Def4; hence thesis by A4,A17,A18,TARSKI:
def 1;
            end;
            hence thesis by Th60;
         suppose
        A19:A = ].c,d.];
              A = {}
            proof
               assume
A20:           A <> {};
               consider x being Element of A;
                 A c= ExtREAL by XBOOLE_1:1;
               then reconsider x as R_eal by A20,TARSKI:def 3;
           A21:c <' x & x <=' d & x in REAL by A19,A20,Def3;
                 x in {a} by A4,A20,TARSKI:def 3;
           then A22:x = a by TARSKI:def 1;
               consider y being R_eal such that
           A23:c <' y & y <' x & y in REAL by A21,Th17;
                 y <=' d by A21,A23,SUPINF_1:29;
               then y in A by A19,A23,Def3; hence thesis by A4,A22,A23,TARSKI:
def 1;
            end;
            hence thesis by Th60;
   end;
   hence thesis by A1,A2,Def10;
end;

theorem Th62:
   A c= B implies vol A <=' vol B
proof
   assume
A1:A c= B;
     A is open_interval or A is closed_interval or
   A is right_open_interval or A is left_open_interval by Def9;
   then (ex a1,b1 being R_eal st (a1 <=' b1 & A =].a1,b1.[)) or
   (ex a1,b1 being R_eal st (a1 <=' b1 & A =[.a1,b1.])) or
   (ex a1,b1 being R_eal st (a1 <=' b1 & A =[.a1,b1.[)) or
   (ex a1,b1 being R_eal st (a1 <=' b1 & A =].a1,b1.]))
   by Def5,Def6,Def7,Def8;
   then consider a1,b1 being R_eal such that
A2:A =].a1,b1.[ or A =[.a1,b1.] or A =[.a1,b1.[ or A =].a1,b1.];
     B is open_interval or B is closed_interval or
   B is right_open_interval or B is left_open_interval by Def9;
   then (ex a2,b2 being R_eal st (a2 <=' b2 & B =].a2,b2.[)) or
   (ex a2,b2 being R_eal st (a2 <=' b2 & B =[.a2,b2.])) or
   (ex a2,b2 being R_eal st (a2 <=' b2 & B =[.a2,b2.[)) or
   (ex a2,b2 being R_eal st (a2 <=' b2 & B =].a2,b2.]))
   by Def5,Def6,Def7,Def8;
   then consider a2,b2 being R_eal such that
A3:B =].a2,b2.[ or B =[.a2,b2.] or B =[.a2,b2.[ or B =].a2,b2.];
   per cases by A2,A3;
   suppose
A4:  A = ].a1,b1.[ & B = ].a2,b2.[;
   thus vol(A) <=' vol(B)
proof
   per cases;
      suppose
   A5:a1 <' b1 & a2 <' b2;
   A6:b1 <=' b2 & a2 <=' a1
      proof
         assume
A7:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A7;
            suppose b2 <' b1;
               then consider x being R_eal such that
            A8:a1 <' x & b2 <' x & x <' b1 & x in REAL by A5,Th19;
                 x in ].a1,b1.[ & not x <=' b2 by A8,Def2;
               hence thesis by A1,A4,Def2;
            suppose a1 <' a2;
               then consider x being R_eal such that
            A9:a1 <' x & x <' a2 & x <' b1 & x in REAL by A5,Th18;
                 x in ].a1,b1.[ & not a2 <=' x by A9,Def2;
               hence thesis by A1,A4,Def2;
      end;
A10:      not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A5;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A4,A5,Def10;
      hence thesis by A6,A10,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A4,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A11:b1 <=' a1 & a2 <' b2;
   then A12:vol(A) = 0. by A4,Def10;
   A13:vol(B) = b2 - a2 by A4,A11,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty
      ) & a2 <=' b2 by A11;
      hence thesis by A12,A13,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A4,Def10;
      hence thesis;
end;
   suppose
A14:  A = ].a1,b1.[ & B = [.a2,b2.];
   thus vol A <=' vol B
proof
   per cases;
      suppose
   A15:a1 <' b1 & a2 <' b2;
   A16:b1 <=' b2 & a2 <=' a1
      proof
         assume
A17:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A17;
            suppose b2 <' b1;
               then consider x being R_eal such that
            A18:a1 <' x & b2 <' x & x <' b1 & x in REAL by A15,Th19;
                 x in ].a1,b1.[ & not x <=' b2 by A18,Def2;
               hence thesis by A1,A14,Def1;
            suppose a1 <' a2;
               then consider x being R_eal such that
            A19:a1 <' x & x <' a2 & x <' b1 & x in REAL by A15,Th18;
                 x in ].a1,b1.[ & not a2 <=' x by A19,Def2;
               hence thesis by A1,A14,Def1;
      end;
A20:      not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A15;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A14,A15,Def10;
      hence thesis by A16,A20,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A1,A14,Th61;
      hence thesis;
      suppose
   A21:b1 <=' a1 & a2 <' b2;
   then A22:vol(A) = 0. by A14,Def10;
   A23:vol(B) = b2 - a2 by A14,A21,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A21;
      hence thesis by A22,A23,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A14,Def10;
      hence thesis;
end;
   suppose
A24:  A = ].a1,b1.[ & B = [.a2,b2.[;
   thus vol(A) <=' vol(B)
proof
   per cases;
      suppose
   A25:a1 <' b1 & a2 <' b2;
   A26:b1 <=' b2 & a2 <=' a1
      proof
         assume
A27:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A27;
            suppose b2 <' b1;
               then consider x being R_eal such that
            A28:a1 <' x & b2 <' x & x <' b1 & x in REAL by A25,Th19;
                 x in ].a1,b1.[ & not x <=' b2 by A28,Def2;
               hence thesis by A1,A24,Def4;
            suppose a1 <' a2;
               then consider x being R_eal such that
            A29:a1 <' x & x <' a2 & x <' b1 & x in REAL by A25,Th18;
                 x in ].a1,b1.[ & not a2 <=' x by A29,Def2;
               hence thesis by A1,A24,Def4;
      end;
A30:      not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A25;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A24,A25,Def10;
      hence thesis by A26,A30,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A24,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A31:b1 <=' a1 & a2 <' b2;
   then A32:vol(A) = 0. by A24,Def10;
   A33:vol(B) = b2 - a2 by A24,A31,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A31;
      hence thesis by A32,A33,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A24,Def10;
      hence thesis;
end;
   suppose
A34:   A = ].a1,b1.[ & B = ].a2,b2.];
   thus vol(A) <=' vol(B)
proof
   per cases;
      suppose
   A35:a1 <' b1 & a2 <' b2;
   A36:b1 <=' b2 & a2 <=' a1
      proof
         assume
A37:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A37;
            suppose b2 <' b1;
               then consider x being R_eal such that
            A38:a1 <' x & b2 <' x & x <' b1 & x in REAL by A35,Th19;
                 x in ].a1,b1.[ & not x <=' b2 by A38,Def2;
               hence thesis by A1,A34,Def3;
            suppose a1 <' a2;
               then consider x being R_eal such that
            A39:a1 <' x & x <' a2 & x <' b1 & x in REAL by A35,Th18;
                 x in ].a1,b1.[ & not a2 <=' x by A39,Def2;
               hence thesis by A1,A34,Def3;
      end;
A40:   (not (b1 = +infty & a1 = +infty) & not (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A35;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A34,A35,Def10;
      hence thesis by A36,A40,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A34,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A41:b1 <=' a1 & a2 <' b2;
   then A42:vol(A) = 0. by A34,Def10;
   A43:vol(B) = b2 - a2 by A34,A41,Def10;
        (b2 <> -infty or a2 <> -infty) & (b2 <> +infty or a2 <> +infty) &
          a2 <=' b2 by A41;
      hence thesis by A42,A43,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A34,Def10;
      hence thesis;
end;
   suppose
A44:   A = [.a1,b1.] & B = ].a2,b2.[;
   thus vol(A) <=' vol(B)
proof
   per cases;
      suppose
   A45:a1 <' b1 & a2 <' b2;
   A46:b1 <=' b2 & a2 <=' a1
      proof
         assume
A47:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A47;
            suppose b2 <' b1;
               then consider x being R_eal such that
            A48:a1 <' x & b2 <' x & x <' b1 & x in REAL by A45,Th19;
                 x in [.a1,b1.] & not x <=' b2 by A48,Def1;
               hence thesis by A1,A44,Def2;
            suppose a1 <' a2;
               then consider x being R_eal such that
            A49:a1 <' x & x <' a2 & x <' b1 & x in REAL by A45,Th18;
                 x in [.a1,b1.] & not a2 <=' x by A49,Def1;
               hence thesis by A1,A44,Def2;
      end;
A50:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A45;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A44,A45,Def10;
      hence thesis by A46,A50,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A44,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A51:b1 <=' a1 & a2 <' b2;
   then A52:vol A = 0. by A44,Def10;
  A53:vol B = b2 - a2 by A44,A51,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A51;
      hence thesis by A52,A53,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol A = 0. & vol B = 0. by A44,Def10;
      hence thesis;
end;
   suppose
A54:   A = [.a1,b1.] & B = [.a2,b2.];
   thus vol A <=' vol B
proof
   per cases;
      suppose
   A55:a1 <' b1 & a2 <' b2;
   A56:b1 <=' b2 & a2 <=' a1
      proof
         assume
A57:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A57;
            suppose b2 <' b1;
               then consider x being R_eal such that
            A58:a1 <' x & b2 <' x & x <' b1 & x in REAL by A55,Th19;
                 x in [.a1,b1.] & not x <=' b2 by A58,Def1;
               hence thesis by A1,A54,Def1;
            suppose a1 <' a2;
               then consider x being R_eal such that
            A59:a1 <' x & x <' a2 & x <' b1 & x in REAL by A55,Th18;
                 x in [.a1,b1.] & not a2 <=' x by A59,Def1;
               hence thesis by A1,A54,Def1;
      end;
A60:      not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A55;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A54,A55,Def10;
      hence thesis by A56,A60,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then vol A = 0. & vol B = 0. by A1,A54,Th61;
      hence thesis;
      suppose
   A61:b1 <=' a1 & a2 <' b2;
   then A62:vol A = 0. by A54,Def10;
   A63:vol B = b2 - a2 by A54,A61,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A61;
      hence thesis by A62,A63,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol A = 0. & vol B = 0. by A54,Def10;
      hence thesis;
end;
   suppose
A64:   A = [.a1,b1.] & B = [.a2,b2.[;
   thus vol A <=' vol B
proof
   per cases;
      suppose
   A65:a1 <' b1 & a2 <' b2;
   A66:b1 <=' b2 & a2 <=' a1
      proof
         assume
A67:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A67;
            suppose b2 <' b1;
            then consider x being R_eal such that
         A68:a1 <' x & b2 <' x & x <' b1 & x in REAL by A65,Th19;
              x in [.a1,b1.] & not x <=' b2 by A68,Def1;
            hence thesis by A1,A64,Def4;
            suppose a1 <' a2;
            then consider x being R_eal such that
         A69:a1 <' x & x <' a2 & x <' b1 & x in REAL by A65,Th18;
              x in [.a1,b1.] & not a2 <=' x by A69,Def1;
            hence thesis by A1,A64,Def4;
      end;
A70:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A65;
        vol A = b1 - a1 & vol(B) = b2 - a2 by A64,A65,Def10;
      hence thesis by A66,A70,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A64,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A71:b1 <=' a1 & a2 <' b2;
   then A72:vol A = 0. by A64,Def10;
   A73:vol B = b2 - a2 by A64,A71,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A71;
      hence thesis by A72,A73,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol A = 0. & vol B = 0. by A64,Def10;
      hence thesis;
end;
   suppose
A74:   A = [.a1,b1.] & B = ].a2,b2.];
   thus vol A <=' vol B
proof
   per cases;
      suppose
   A75:a1 <' b1 & a2 <' b2;
   A76:b1 <=' b2 & a2 <=' a1
      proof
         assume
A77:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A77;
            suppose b2 <' b1;
            then consider x being R_eal such that
         A78:a1 <' x & b2 <' x & x <' b1 & x in REAL by A75,Th19;
              x in [.a1,b1.] & not x <=' b2 by A78,Def1;
            hence thesis by A1,A74,Def3;
            suppose a1 <' a2;
            then consider x being R_eal such that
         A79:a1 <' x & x <' a2 & x <' b1 & x in REAL by A75,Th18;
              x in [.a1,b1.] & not a2 <=' x by A79,Def1;
            hence thesis by A1,A74,Def3;
      end;
A80:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A75;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A74,A75,Def10;
      hence thesis by A76,A80,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A74,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A81:b1 <=' a1 & a2 <' b2;
   then A82:vol(A) = 0. by A74,Def10;
   A83:vol(B) = b2 - a2 by A74,A81,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A81;
      hence thesis by A82,A83,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A74,Def10;
      hence thesis;
end;
   suppose
A84:   A = ].a1,b1.] & B = ].a2,b2.[;
   thus vol A <=' vol B
proof
   per cases;
   suppose
A85:a1 <' b1 & a2 <' b2;
A86:b1 <=' b2 & a2 <=' a1
   proof
      assume
A87:      not b1 <=' b2 or not a2 <=' a1;
      per cases by A87;
         suppose b2 <' b1;
         then consider x being R_eal such that
      A88:a1 <' x & b2 <' x & x <' b1 & x in REAL by A85,Th19;
           x in ].a1,b1.] & not x <=' b2 by A88,Def3;
        hence thesis by A1,A84,Def2;
         suppose a1 <' a2;
         then consider x being R_eal such that
      A89:a1 <' x & x <' a2 & x <' b1 & x in REAL by A85,Th18;
           x in ].a1,b1.] & not a2 <=' x by A89,Def3;
        hence thesis by A1,A84,Def2;
      end;
A90:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A85;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A84,A85,Def10;
      hence thesis by A86,A90,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A84,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A91:b1 <=' a1 & a2 <' b2;
   then A92:vol(A) = 0. by A84,Def10;
   A93:vol(B) = b2 - a2 by A84,A91,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A91;
      hence thesis by A92,A93,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A84,Def10;
      hence thesis;
end;
   suppose
A94:   A = ].a1,b1.] & B = [.a2,b2.];
   thus vol A <=' vol B
proof
   per cases;
   suppose
A95:a1 <' b1 & a2 <' b2;
A96:b1 <=' b2 & a2 <=' a1
   proof
      assume
A97:      not b1 <=' b2 or not a2 <=' a1;
      per cases by A97;
         suppose b2 <' b1;
         then consider x being R_eal such that
      A98:a1 <' x & b2 <' x & x <' b1 & x in REAL by A95,Th19;
           x in ].a1,b1.] & not x <=' b2 by A98,Def3;
         hence thesis by A1,A94,Def1;
         suppose a1 <' a2;
         then consider x being R_eal such that
      A99:a1 <' x & x <' a2 & x <' b1 & x in REAL by A95,Th18;
           x in ].a1,b1.] & not a2 <=' x by A99,Def3; hence thesis by A1,A94,
Def1
;
      end;
A100:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A95;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A94,A95,Def10;
      hence thesis by A96,A100,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A1,A94,Th61;
      hence thesis;
      suppose
   A101:b1 <=' a1 & a2 <' b2;
   then A102:vol(A) = 0. by A94,Def10;
  A103:vol(B) = b2 - a2 by A94,A101,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A101;
      hence thesis by A102,A103,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A94,Def10;
      hence thesis;
end;
   suppose
A104:   A = ].a1,b1.] & B = [.a2,b2.[;
   thus vol A <=' vol B
proof
   per cases;
      suppose
   A105:a1 <' b1 & a2 <' b2;
   A106:b1 <=' b2 & a2 <=' a1
      proof
         assume
A107:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A107;
            suppose b2 <' b1;
            then consider x being R_eal such that
         A108:a1 <' x & b2 <' x & x <' b1 & x in REAL by A105,Th19;
              x in ].a1,b1.] & not x <=' b2 by A108,Def3;
            hence thesis by A1,A104,Def4;
            suppose a1 <' a2;
            then consider x being R_eal such that
         A109:a1 <' x & x <' a2 & x <' b1 & x in REAL by A105,Th18;
              x in ].a1,b1.] & not a2 <=' x by A109,Def3;
            hence thesis by A1,A104,Def4;
      end;
A110:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A105;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A104,A105,Def10;
      hence thesis by A106,A110,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A104,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A111:b1 <=' a1 & a2 <' b2;
   then A112:vol(A) = 0. by A104,Def10;
   A113:vol(B) = b2 - a2 by A104,A111,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A111;
      hence thesis by A112,A113,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A104,Def10;
      hence thesis;
end;
   suppose
A114:   A = ].a1,b1.] & B = ].a2,b2.];
   thus vol A <=' vol B
proof
   per cases;
      suppose
   A115:a1 <' b1 & a2 <' b2;
   A116:b1 <=' b2 & a2 <=' a1
      proof
         assume
A117:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A117;
            suppose b2 <' b1;
            then consider x being R_eal such that
         A118:a1 <' x & b2 <' x & x <' b1 & x in REAL by A115,Th19;
              x in ].a1,b1.] & not x <=' b2 by A118,Def3;
            hence thesis by A1,A114,Def3;
            suppose a1 <' a2;
            then consider x being R_eal such that
         A119:a1 <' x & x <' a2 & x <' b1 & x in REAL by A115,Th18;
              x in ].a1,b1.] & not a2 <=' x by A119,Def3;
            hence thesis by A1,A114,Def3;
      end;
A120:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A115;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A114,A115,Def10;
      hence thesis by A116,A120,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A114,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A121:b1 <=' a1 & a2 <' b2;
   then A122:vol(A) = 0. by A114,Def10;
  A123:vol(B) = b2 - a2 by A114,A121,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A121;
      hence thesis by A122,A123,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A114,Def10;
      hence thesis;
end;
   suppose
A124:   A = [.a1,b1.[ & B = ].a2,b2.[;
   thus vol A <=' vol B
proof
   per cases;
      suppose
   A125:a1 <' b1 & a2 <' b2;
   A126:b1 <=' b2 & a2 <=' a1
      proof
         assume
A127:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A127;
            suppose b2 <' b1;
            then consider x being R_eal such that
         A128:a1 <' x & b2 <' x & x <' b1 & x in REAL by A125,Th19;
              x in [.a1,b1.[ & not x <=' b2 by A128,Def4;
            hence thesis by A1,A124,Def2;
            suppose a1 <' a2;
               then consider x being R_eal such that
            A129:a1 <' x & x <' a2 & x <' b1 & x in REAL by A125,Th18;
                 x in [.a1,b1.[ & not a2 <=' x by A129,Def4;
               hence thesis by A1,A124,Def2;
      end;
A130:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A125;
        vol A = b1 - a1 & vol(B) = b2 - a2 by A124,A125,Def10;
      hence thesis by A126,A130,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A124,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A131:b1 <=' a1 & a2 <' b2;
   then A132:vol(A) = 0. by A124,Def10;
   A133:vol(B) = b2 - a2 by A124,A131,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A131;
      hence thesis by A132,A133,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A124,Def10;
      hence thesis;
end;
   suppose
A134:   A = [.a1,b1.[ & B = [.a2,b2.];
   thus vol A <=' vol B
proof
   per cases;
   suppose
A135:a1 <' b1 & a2 <' b2;
A136:b1 <=' b2 & a2 <=' a1
   proof
      assume
A137:   not b1 <=' b2 or not a2 <=' a1;
      per cases by A137;
      suppose b2 <' b1;
      then consider x being R_eal such that
   A138:a1 <' x & b2 <' x & x <' b1 & x in REAL by A135,Th19;
        x in [.a1,b1.[ & not x <=' b2 by A138,Def4; hence thesis by A1,A134,
Def1
;
      suppose a1 <' a2;
      then consider x being R_eal such that
   A139:a1 <' x & x <' a2 & x <' b1 & x in REAL by A135,Th18;
        x in [.a1,b1.[ & not a2 <=' x by A139,Def4; hence thesis by A1,A134,
Def1
;
      end;
A140:not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
   not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A135;
     vol(A) = b1 - a1 & vol(B) = b2 - a2 by A134,A135,Def10;
   hence thesis by A136,A140,SUPINF_2:15;
   suppose a1 <' b1 & b2 <=' a2;
   then vol A = 0. & vol B = 0. by A1,A134,Th61;
   hence thesis;
   suppose
A141:b1 <=' a1 & a2 <' b2;
then A142:vol(A) = 0. by A134,Def10;
A143:vol(B) = b2 - a2 by A134,A141,Def10;
     not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
   a2 <=' b2 by A141;
   hence thesis by A142,A143,Th2;
   suppose b1 <=' a1 & b2 <=' a2;
   then vol(A) = 0. & vol(B) = 0. by A134,Def10;
   hence thesis;
end;
   suppose
A144:   A = [.a1,b1.[ & B = [.a2,b2.[;
   thus vol A <=' vol B
proof
   per cases;
   suppose
A145:a1 <' b1 & a2 <' b2;
A146:b1 <=' b2 & a2 <=' a1
   proof
      assume
A147:   not b1 <=' b2 or not a2 <=' a1;
      per cases by A147;
      suppose b2 <' b1;
      then consider x being R_eal such that
   A148:a1 <' x & b2 <' x & x <' b1 & x in REAL by A145,Th19;
        x in [.a1,b1.[ & not x <=' b2 by A148,Def4;
      hence thesis by A1,A144,Def4;
      suppose a1 <' a2;
      then consider x being R_eal such that
   A149:a1 <' x & x <' a2 & x <' b1 & x in REAL by A145,Th18;
        x in [.a1,b1.[ & not a2 <=' x by A149,Def4; hence thesis by A1,A144,
Def4
;
   end;
A150:not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
   not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A145;
     vol A = b1 - a1 & vol B = b2 - a2 by A144,A145,Def10;
   hence thesis by A146,A150,SUPINF_2:15;
   suppose a1 <' b1 & b2 <=' a2;
   then B = {} by A144,Th15;
   hence thesis by A1,XBOOLE_1:3;
   suppose
A151:b1 <=' a1 & a2 <' b2;
then A152:vol(A) = 0. by A144,Def10;
A153:vol(B) = b2 - a2 by A144,A151,Def10;
     not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
   a2 <=' b2 by A151;
   hence thesis by A152,A153,Th2;
   suppose b1 <=' a1 & b2 <=' a2;
   then vol(A) = 0. & vol(B) = 0. by A144,Def10;
   hence thesis;
end;
   suppose
A154:   A = [.a1,b1.[ & B = ].a2,b2.];
   thus vol(A) <=' vol(B)
proof
   per cases;
      suppose
   A155:a1 <' b1 & a2 <' b2;
   A156:b1 <=' b2 & a2 <=' a1
      proof
         assume
A157:      not b1 <=' b2 or not a2 <=' a1;
         per cases by A157;
            suppose b2 <' b1;
            then consider x being R_eal such that
         A158:a1 <' x & b2 <' x & x <' b1 & x in REAL by A155,Th19;
              x in [.a1,b1.[ & not x <=' b2 by A158,Def4;
            hence thesis by A1,A154,Def3;
            suppose a1 <' a2;
            then consider x being R_eal such that
         A159:a1 <' x & x <' a2 & x <' b1 & x in REAL by A155,Th18;
              x in [.a1,b1.[ & not a2 <=' x by A159,Def4;
            hence thesis by A1,A154,Def3;
      end;
A160:   not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
      not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A155;
        vol(A) = b1 - a1 & vol(B) = b2 - a2 by A154,A155,Def10;
      hence thesis by A156,A160,SUPINF_2:15;
      suppose a1 <' b1 & b2 <=' a2;
      then B = {} by A154,Th15;
      hence thesis by A1,XBOOLE_1:3;
      suppose
   A161:b1 <=' a1 & a2 <' b2;
   then A162:vol(A) = 0. by A154,Def10;
   A163:vol(B) = b2 - a2 by A154,A161,Def10;
        not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
      a2 <=' b2 by A161;
      hence thesis by A162,A163,Th2;
      suppose b1 <=' a1 & b2 <=' a2;
      then vol(A) = 0. & vol(B) = 0. by A154,Def10;
      hence thesis;
end;
end;

theorem
     0. <=' vol(A)
proof
     {} c= A by XBOOLE_1:2;
   hence thesis by Th60,Th62;
end;


Back to top