rcomp_1.miz



    begin

    reserve n,n1,m,k for Nat;

    reserve x,y for set;

    reserve s,g,g1,g2,r,p,p2,q,t for Real;

    reserve s1,s2,s3 for Real_Sequence;

    reserve Nseq for increasing sequence of NAT ;

    reserve X for Subset of REAL ;

    definition

      let g,s be Real;

      :: original: [.

      redefine

      :: RCOMP_1:def1

      func [.g,s.] -> Subset of REAL equals { r : g <= r & r <= s };

      coherence

      proof

        now

          let x be object;

          assume x in [.g, s.];

          then

           A1: ex r be Element of ExtREAL st x = r & g <= r & r <= s;

          g in REAL & s in REAL by XREAL_0:def 1;

          hence x in REAL by A1, XXREAL_0: 45;

        end;

        hence thesis by TARSKI:def 3;

      end;

      compatibility

      proof

        set Y = { r : g <= r & r <= s };

        let X be Subset of REAL ;

        

         A2: [.g, s.] c= Y

        proof

          let x be object;

          assume x in [.g, s.];

          then

          consider r be Element of ExtREAL such that

           A3: x = r and

           A4: g <= r & r <= s;

          g in REAL & s in REAL by XREAL_0:def 1;

          then r in REAL by A4, XXREAL_0: 45;

          hence thesis by A3, A4;

        end;

        Y c= [.g, s.]

        proof

          let x be object;

          assume x in Y;

          then

          consider r such that

           A5: x = r & g <= r & r <= s;

          r in REAL by XREAL_0:def 1;

          hence thesis by A5, NUMBERS: 31;

        end;

        hence thesis by A2;

      end;

    end

    definition

      let g,s be ExtReal;

      :: original: ].

      redefine

      :: RCOMP_1:def2

      func ].g,s.[ -> Subset of REAL equals { r : g < r & r < s };

      coherence

      proof

        now

          let x be object;

          assume x in ].g, s.[;

          then ex r be Element of ExtREAL st x = r & g < r & r < s;

          hence x in REAL by XXREAL_0: 48;

        end;

        hence thesis by TARSKI:def 3;

      end;

      compatibility

      proof

        set Y = { r : g < r & r < s };

        let X be Subset of REAL ;

        

         A1: Y c= ].g, s.[

        proof

          let x be object;

          assume x in Y;

          then

          consider r such that

           A2: x = r & g < r & r < s;

          r in REAL by XREAL_0:def 1;

          hence thesis by A2, NUMBERS: 31;

        end;

         ].g, s.[ c= Y

        proof

          let x be object;

          assume x in ].g, s.[;

          then

          consider r be Element of ExtREAL such that

           A3: x = r and

           A4: g < r & r < s;

          r in REAL by A4, XXREAL_0: 48;

          hence thesis by A3, A4;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: RCOMP_1:1

    

     Th1: r in ].(p - g), (p + g).[ iff |.(r - p).| < g

    proof

      thus r in ].(p - g), (p + g).[ implies |.(r - p).| < g

      proof

        assume r in ].(p - g), (p + g).[;

        then

         A1: ex s st r = s & (p - g) < s & s < (p + g);

        then (p + ( - g)) < r;

        then

         A2: ( - g) < (r - p) by XREAL_1: 20;

        (r - p) < g by A1, XREAL_1: 19;

        hence thesis by A2, SEQ_2: 1;

      end;

      assume

       A3: |.(r - p).| < g;

      then (r - p) < g by SEQ_2: 1;

      then

       A4: r < (p + g) by XREAL_1: 19;

      ( - g) < (r - p) by A3, SEQ_2: 1;

      then r is Real & (p + ( - g)) < r by XREAL_1: 20;

      hence thesis by A4;

    end;

    theorem :: RCOMP_1:2

    r in [.p, g.] iff |.((p + g) - (2 * r)).| <= (g - p)

    proof

      thus r in [.p, g.] implies |.((p + g) - (2 * r)).| <= (g - p)

      proof

        assume r in [.p, g.];

        then

         A1: ex s st s = r & p <= s & s <= g;

        then (2 * r) <= (2 * g) by XREAL_1: 64;

        then ( - (2 * r)) >= ( - (2 * g)) by XREAL_1: 24;

        then ((p + g) + ( - (2 * r))) >= ((p + g) + ( - (2 * g))) by XREAL_1: 7;

        then

         A2: ((p + g) - (2 * r)) >= ( - (g - p));

        (2 * p) <= (2 * r) by A1, XREAL_1: 64;

        then ( - (2 * p)) >= ( - (2 * r)) by XREAL_1: 24;

        then ((p + g) + ( - (2 * p))) >= ((p + g) + ( - (2 * r))) by XREAL_1: 7;

        hence thesis by A2, ABSVALUE: 5;

      end;

      assume

       A3: |.((p + g) - (2 * r)).| <= (g - p);

      then ((p + g) - (2 * r)) >= ( - (g - p)) by ABSVALUE: 5;

      then (p + g) >= ((p - g) + (2 * r)) by XREAL_1: 19;

      then ((p + g) - (p - g)) >= (2 * r) by XREAL_1: 19;

      then

       A4: ((1 / 2) * (2 * g)) >= ((1 / 2) * (2 * r)) by XREAL_1: 64;

      (g - p) >= ((p + g) - (2 * r)) by A3, ABSVALUE: 5;

      then ((2 * r) + (g - p)) >= (p + g) by XREAL_1: 20;

      then (2 * r) >= ((p + g) - (g - p)) by XREAL_1: 20;

      then ((1 / 2) * (2 * r)) >= ((1 / 2) * (2 * p)) by XREAL_1: 64;

      hence r in [.p, g.] by A4;

    end;

    theorem :: RCOMP_1:3

    r in ].p, g.[ iff |.((p + g) - (2 * r)).| < (g - p)

    proof

      thus r in ].p, g.[ implies |.((p + g) - (2 * r)).| < (g - p)

      proof

        assume r in ].p, g.[;

        then

         A1: ex s st s = r & p < s & s < g;

        then (2 * r) < (2 * g) by XREAL_1: 68;

        then ( - (2 * r)) > ( - (2 * g)) by XREAL_1: 24;

        then ((p + g) + ( - (2 * r))) > ((p + g) + ( - (2 * g))) by XREAL_1: 6;

        then

         A2: ((p + g) - (2 * r)) > ( - (g - p));

        (2 * p) < (2 * r) by A1, XREAL_1: 68;

        then ( - (2 * p)) > ( - (2 * r)) by XREAL_1: 24;

        then ((p + g) + ( - (2 * p))) > ((p + g) + ( - (2 * r))) by XREAL_1: 6;

        hence thesis by A2, SEQ_2: 1;

      end;

      assume

       A3: |.((p + g) - (2 * r)).| < (g - p);

      then ((p + g) - (2 * r)) > ( - (g - p)) by SEQ_2: 1;

      then (p + g) > ((p - g) + (2 * r)) by XREAL_1: 20;

      then ((p + g) - (p - g)) > (2 * r) by XREAL_1: 20;

      then

       A4: ((1 / 2) * (2 * g)) > ((1 / 2) * (2 * r)) by XREAL_1: 68;

      (g - p) > ((p + g) - (2 * r)) by A3, SEQ_2: 1;

      then ((2 * r) + (g - p)) > (p + g) by XREAL_1: 19;

      then (2 * r) > ((p + g) - (g - p)) by XREAL_1: 19;

      then ((1 / 2) * (2 * r)) > ((1 / 2) * (2 * p)) by XREAL_1: 68;

      hence thesis by A4;

    end;

    definition

      let X;

      :: RCOMP_1:def3

      attr X is compact means for s1 st ( rng s1) c= X holds ex s2 st s2 is subsequence of s1 & s2 is convergent & ( lim s2) in X;

    end

    definition

      let X;

      :: RCOMP_1:def4

      attr X is closed means for s1 st ( rng s1) c= X & s1 is convergent holds ( lim s1) in X;

    end

    definition

      let X;

      :: RCOMP_1:def5

      attr X is open means

      : Def5: (X ` ) is closed;

    end

    theorem :: RCOMP_1:4

    

     Th4: for s1 st ( rng s1) c= [.s, g.] holds s1 is bounded

    proof

      let s1 such that

       A1: ( rng s1) c= [.s, g.];

      thus s1 is bounded_above

      proof

        take r = (g + 1);

        

         A2: for t st t in ( rng s1) holds t < r

        proof

          let t;

          assume t in ( rng s1);

          then t in [.s, g.] by A1;

          then

           A3: ex p st t = p & s <= p & p <= g;

          g < r by XREAL_1: 29;

          hence thesis by A3, XXREAL_0: 2;

        end;

        let n;

        n in NAT by ORDINAL1:def 12;

        then n in ( dom s1) by FUNCT_2:def 1;

        then (s1 . n) in ( rng s1) by FUNCT_1:def 3;

        hence thesis by A2;

      end;

      take r = (s - 1);

      

       A4: (r + 1) = (s - (1 - 1));

      

       A5: for t st t in ( rng s1) holds r < t

      proof

        let t;

        assume t in ( rng s1);

        then t in [.s, g.] by A1;

        then

         A6: ex p st t = p & s <= p & p <= g;

        r < s by A4, XREAL_1: 29;

        hence thesis by A6, XXREAL_0: 2;

      end;

      let n;

      n in NAT by ORDINAL1:def 12;

      then n in ( dom s1) by FUNCT_2:def 1;

      then (s1 . n) in ( rng s1) by FUNCT_1:def 3;

      hence thesis by A5;

    end;

    theorem :: RCOMP_1:5

    

     Th5: [.s, g.] is closed

    proof

      for s1 st ( rng s1) c= [.s, g.] & s1 is convergent holds ( lim s1) in [.s, g.]

      proof

        let s1;

        assume that

         A1: ( rng s1) c= [.s, g.] and

         A2: s1 is convergent;

        

         A3: s <= ( lim s1)

        proof

          set s2 = ( seq_const s);

           A4:

          now

            let n;

            n in NAT by ORDINAL1:def 12;

            then n in ( dom s1) by FUNCT_2:def 1;

            then (s1 . n) in ( rng s1) by FUNCT_1:def 3;

            then (s1 . n) in [.s, g.] by A1;

            then ex p st (s1 . n) = p & s <= p & p <= g;

            hence (s2 . n) <= (s1 . n) by SEQ_1: 57;

          end;

          (s2 . 0 ) = s by SEQ_1: 57;

          then ( lim s2) = s by SEQ_4: 25;

          hence thesis by A2, A4, SEQ_2: 18;

        end;

        ( lim s1) <= g

        proof

          set s2 = ( seq_const g);

           A5:

          now

            let n;

            n in NAT by ORDINAL1:def 12;

            then n in ( dom s1) by FUNCT_2:def 1;

            then (s1 . n) in ( rng s1) by FUNCT_1:def 3;

            then (s1 . n) in [.s, g.] by A1;

            then ex p st (s1 . n) = p & s <= p & p <= g;

            hence (s1 . n) <= (s2 . n) by SEQ_1: 57;

          end;

          (s2 . 0 ) = g by SEQ_1: 57;

          then ( lim s2) = g by SEQ_4: 25;

          hence thesis by A2, A5, SEQ_2: 18;

        end;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: RCOMP_1:6

     [.s, g.] is compact

    proof

      for s1 st ( rng s1) c= [.s, g.] holds ex s2 st s2 is subsequence of s1 & s2 is convergent & ( lim s2) in [.s, g.]

      proof

        let s1;

        

         A1: [.s, g.] is closed by Th5;

        assume

         A2: ( rng s1) c= [.s, g.];

        then

        consider s2 be Real_Sequence such that

         A3: s2 is subsequence of s1 and

         A4: s2 is convergent by Th4, SEQ_4: 40;

        take s2;

        ex Nseq st s2 = (s1 * Nseq) by A3, VALUED_0:def 17;

        then ( rng s2) c= ( rng s1) by RELAT_1: 26;

        then ( rng s2) c= [.s, g.] by A2;

        hence thesis by A3, A4, A1;

      end;

      hence thesis;

    end;

    theorem :: RCOMP_1:7

    

     Th7: ].p, q.[ is open

    proof

      defpred P[ Real] means $1 <= p or q <= $1;

      consider X such that

       A1: for r be Element of REAL holds r in X iff P[r] from SUBSET_1:sch 3;

      now

        let s1 such that

         A2: ( rng s1) c= X and

         A3: s1 is convergent;

        

         A4: ( lim s1) in REAL by XREAL_0:def 1;

        ( lim s1) <= p or q <= ( lim s1)

        proof

          assume

           A5: not thesis;

          then 0 < (( lim s1) - p) by XREAL_1: 50;

          then

          consider n1 such that

           A6: for m st n1 <= m holds |.((s1 . m) - ( lim s1)).| < (( lim s1) - p) by A3, SEQ_2:def 7;

           0 < (q - ( lim s1)) by A5, XREAL_1: 50;

          then

          consider n such that

           A7: for m st n <= m holds |.((s1 . m) - ( lim s1)).| < (q - ( lim s1)) by A3, SEQ_2:def 7;

          consider k such that

           A8: ( max (n,n1)) < k by SEQ_4: 3;

          n1 <= ( max (n,n1)) by XXREAL_0: 25;

          then n1 <= k by A8, XXREAL_0: 2;

          then

           A9: |.((s1 . k) - ( lim s1)).| < (( lim s1) - p) by A6;

          ( - |.((s1 . k) - ( lim s1)).|) <= ((s1 . k) - ( lim s1)) by ABSVALUE: 4;

          then ( - ((s1 . k) - ( lim s1))) <= ( - ( - |.((s1 . k) - ( lim s1)).|)) by XREAL_1: 24;

          then ( - ((s1 . k) - ( lim s1))) < (( lim s1) - p) by A9, XXREAL_0: 2;

          then ( - (( lim s1) - p)) < ( - ( - ((s1 . k) - ( lim s1)))) by XREAL_1: 24;

          then (p - ( lim s1)) < ((s1 . k) - ( lim s1));

          then

           A10: p < (s1 . k) by XREAL_1: 9;

          n <= ( max (n,n1)) by XXREAL_0: 25;

          then n <= k by A8, XXREAL_0: 2;

          then ((s1 . k) - ( lim s1)) <= |.((s1 . k) - ( lim s1)).| & |.((s1 . k) - ( lim s1)).| < (q - ( lim s1)) by A7, ABSVALUE: 4;

          then ((s1 . k) - ( lim s1)) < (q - ( lim s1)) by XXREAL_0: 2;

          then

           A11: (s1 . k) < q by XREAL_1: 9;

          

           A12: k in NAT by ORDINAL1:def 12;

          

           A13: (s1 . k) in REAL by XREAL_0:def 1;

          ( dom s1) = NAT by FUNCT_2:def 1;

          then (s1 . k) in ( rng s1) by FUNCT_1:def 3, A12;

          hence contradiction by A1, A2, A11, A10, A13;

        end;

        hence ( lim s1) in X by A1, A4;

      end;

      then

       A14: X is closed;

      now

        let r;

        

         A15: r in REAL by XREAL_0:def 1;

        assume r in ( ].p, q.[ ` );

        then not r in ].p, q.[ by XBOOLE_0:def 5;

        then r <= p or q <= r;

        hence r in X by A1, A15;

      end;

      then

       A16: ( ].p, q.[ ` ) c= X;

      now

        let r;

        assume r in X;

        then not ex s st s = r & p < s & s < q by A1;

        then r in REAL & not r in ].p, q.[ by XREAL_0:def 1;

        hence r in ( ].p, q.[ ` ) by XBOOLE_0:def 5;

      end;

      then X c= ( ].p, q.[ ` );

      then ( ].p, q.[ ` ) = X by A16;

      hence thesis by A14;

    end;

    registration

      let p,q be Real;

      cluster ].p, q.[ -> open;

      coherence by Th7;

      cluster [.p, q.] -> closed;

      coherence by Th5;

    end

    theorem :: RCOMP_1:8

    

     Th8: X is compact implies X is closed

    proof

      assume

       A1: X is compact;

      assume not X is closed;

      then

      consider s1 such that

       A2: ( rng s1) c= X and

       A3: s1 is convergent & not ( lim s1) in X;

      ex s2 st s2 is subsequence of s1 & s2 is convergent & ( lim s2) in X by A1, A2;

      hence contradiction by A3, SEQ_4: 17;

    end;

    registration

      cluster compact -> closed for Subset of REAL ;

      coherence by Th8;

    end

    theorem :: RCOMP_1:9

    

     Th9: (for p st p in X holds ex r, n st 0 < r & (for m st n < m holds r < |.((s1 . m) - p).|)) implies for s2 st s2 is subsequence of s1 holds not (s2 is convergent & ( lim s2) in X)

    proof

      assume that

       A1: for p st p in X holds ex r, n st 0 < r & for m st n < m holds r < |.((s1 . m) - p).| and

       A2: not for s2 st s2 is subsequence of s1 holds not (s2 is convergent & ( lim s2) in X);

      consider s2 such that

       A3: s2 is subsequence of s1 and

       A4: s2 is convergent and

       A5: ( lim s2) in X by A2;

      consider r, n such that

       A6: 0 < r and

       A7: for m st n < m holds r < |.((s1 . m) - ( lim s2)).| by A1, A5;

      consider n1 such that

       A8: for m st n1 <= m holds |.((s2 . m) - ( lim s2)).| < r by A4, A6, SEQ_2:def 7;

      consider NS be increasing sequence of NAT such that

       A9: s2 = (s1 * NS) by A3, VALUED_0:def 17;

      reconsider k = ((n + 1) + n1) as Element of NAT by ORDINAL1:def 12;

       |.(((s1 * NS) . k) - ( lim s2)).| < r by A8, A9, NAT_1: 11;

      then

       A10: |.((s1 . (NS . k)) - ( lim s2)).| < r by FUNCT_2: 15;

      (n + 1) <= k by NAT_1: 11;

      then

       A11: n < k by NAT_1: 13;

      k <= (NS . k) by SEQM_3: 14;

      then n < (NS . k) by A11, XXREAL_0: 2;

      hence contradiction by A7, A10;

    end;

    theorem :: RCOMP_1:10

    

     Th10: X is compact implies X is real-bounded

    proof

      assume

       A1: X is compact;

      assume

       A2: not X is real-bounded;

      per cases by A2;

        suppose

         A3: not X is bounded_above;

        defpred P[ Element of NAT , Element of REAL ] means ex q st q = $2 & q in X & $1 < q;

        

         A4: for n be Element of NAT holds ex p be Element of REAL st P[n, p]

        proof

          let n be Element of NAT ;

           not n is UpperBound of X by A3, XXREAL_2:def 10;

          then

          consider t be ExtReal such that

           A5: t in X & n < t by XXREAL_2:def 1;

          take t;

          thus thesis by A5;

        end;

        consider f be sequence of REAL such that

         A6: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A4);

         A7:

        now

          let n;

          n in NAT by ORDINAL1:def 12;

          then ex q st q = (f . n) & q in X & n < q by A6;

          hence (f . n) in X & n < (f . n);

        end;

        

         A8: for p st p in X holds ex r, n st 0 < r & for m st n < m holds r < |.((f . m) - p).|

        proof

          let p such that p in X;

          consider q such that

           A9: q = 1;

          take r = q;

          consider k such that

           A10: (p + 1) < k by SEQ_4: 3;

          take n = k;

          thus 0 < r by A9;

          let m;

          assume n < m;

          then (p + 1) < m by A10, XXREAL_0: 2;

          then (p + 1) < (f . m) by A7, XXREAL_0: 2;

          then 1 < ((f . m) - p) by XREAL_1: 20;

          hence thesis by A9, ABSVALUE:def 1;

        end;

        ( rng f) c= X

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A11: y in ( dom f) and

           A12: x = (f . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A11, FUNCT_2:def 1;

          (f . y) in X by A7;

          hence thesis by A12;

        end;

        then ex s2 st s2 is subsequence of f & s2 is convergent & ( lim s2) in X by A1;

        hence contradiction by A8, Th9;

      end;

        suppose

         A13: not X is bounded_below;

        defpred P[ Element of NAT , Element of REAL ] means ex q st q = $2 & q in X & q < ( - $1);

        

         A14: for n be Element of NAT holds ex p be Element of REAL st P[n, p]

        proof

          let n be Element of NAT ;

           not ( - n) is LowerBound of X by A13, XXREAL_2:def 9;

          then

          consider t be ExtReal such that

           A15: t in X & t < ( - n) by XXREAL_2:def 2;

          take t;

          thus thesis by A15;

        end;

        consider f be sequence of REAL such that

         A16: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A14);

         A17:

        now

          let n;

          n in NAT by ORDINAL1:def 12;

          then ex q st q = (f . n) & q in X & q < ( - n) by A16;

          hence (f . n) in X & (f . n) < ( - n);

        end;

        

         A18: for p st p in X holds ex r, n st 0 < r & for m st n < m holds r < |.((f . m) - p).|

        proof

          let p such that p in X;

          consider q such that

           A19: q = 1;

          take r = q;

          consider k such that

           A20: |.(p - 1).| < k by SEQ_4: 3;

          take n = k;

          thus 0 < r by A19;

          let m;

          assume n < m;

          then

           A21: ( - m) < ( - n) by XREAL_1: 24;

          ( - k) < (p - 1) by A20, SEQ_2: 1;

          then ( - m) < (p - 1) by A21, XXREAL_0: 2;

          then (f . m) < (p - 1) by A17, XXREAL_0: 2;

          then ((f . m) + 1) < p by XREAL_1: 20;

          then 1 < (p - (f . m)) by XREAL_1: 20;

          then r < |.( - ((f . m) - p)).| by A19, ABSVALUE:def 1;

          hence thesis by COMPLEX1: 52;

        end;

        ( rng f) c= X

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A22: y in ( dom f) and

           A23: x = (f . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A22, FUNCT_2:def 1;

          (f . y) in X by A17;

          hence thesis by A23;

        end;

        then ex s2 st s2 is subsequence of f & s2 is convergent & ( lim s2) in X by A1;

        hence contradiction by A18, Th9;

      end;

    end;

    theorem :: RCOMP_1:11

    X is real-bounded closed implies X is compact

    proof

      assume that

       A1: X is real-bounded and

       A2: X is closed;

      now

        let s1 such that

         A3: ( rng s1) c= X;

        

         A4: s1 is bounded_below

        proof

          consider p such that

           A5: p is LowerBound of X by A1, XXREAL_2:def 9;

          

           A6: for q st q in X holds p <= q by A5, XXREAL_2:def 2;

          take r = (p - 1);

          

           A7: (r + 1) = (p - (1 - 1));

          

           A8: for t st t in ( rng s1) holds r < t

          proof

            let t;

            assume t in ( rng s1);

            then

             A9: p <= t by A3, A6;

            r < p by A7, XREAL_1: 29;

            hence thesis by A9, XXREAL_0: 2;

          end;

          for n holds r < (s1 . n)

          proof

            let n;

            n in NAT by ORDINAL1:def 12;

            then n in ( dom s1) by FUNCT_2:def 1;

            then (s1 . n) in ( rng s1) by FUNCT_1:def 3;

            hence thesis by A8;

          end;

          hence thesis;

        end;

        s1 is bounded_above

        proof

          consider p such that

           A10: p is UpperBound of X by A1, XXREAL_2:def 10;

          

           A11: for q st q in X holds q <= p by A10, XXREAL_2:def 1;

          take r = (p + 1);

          

           A12: for t st t in ( rng s1) holds t < r

          proof

            let t;

            assume t in ( rng s1);

            then

             A13: t <= p by A3, A11;

            p < r by XREAL_1: 29;

            hence thesis by A13, XXREAL_0: 2;

          end;

          for n holds (s1 . n) < r

          proof

            let n;

            n in NAT by ORDINAL1:def 12;

            then n in ( dom s1) by FUNCT_2:def 1;

            then (s1 . n) in ( rng s1) by FUNCT_1:def 3;

            hence thesis by A12;

          end;

          hence thesis;

        end;

        then s1 is bounded by A4;

        then

        consider s2 be Real_Sequence such that

         A14: s2 is subsequence of s1 and

         A15: s2 is convergent by SEQ_4: 40;

        ex Nseq st s2 = (s1 * Nseq) by A14, VALUED_0:def 17;

        then ( rng s2) c= ( rng s1) by RELAT_1: 26;

        then ( rng s2) c= X by A3;

        then ( lim s2) in X by A2, A15;

        hence ex s2 st s2 is subsequence of s1 & s2 is convergent & ( lim s2) in X by A14, A15;

      end;

      hence thesis;

    end;

    theorem :: RCOMP_1:12

    

     Th12: for X st X <> {} & X is closed & X is bounded_above holds ( upper_bound X) in X

    proof

      let X such that

       A1: X <> {} and

       A2: X is closed and

       A3: X is bounded_above and

       A4: not ( upper_bound X) in X;

      set s1 = ( upper_bound X);

      defpred P[ Element of NAT , Element of REAL ] means ex q st q = $2 & q in X & (s1 - q) < (1 / ($1 + 1));

      

       A5: for n be Element of NAT holds ex p be Element of REAL st P[n, p]

      proof

        let n be Element of NAT ;

         0 < ((n + 1) " );

        then 0 < (1 / (n + 1)) by XCMPLX_1: 215;

        then

        consider t such that

         A6: t in X and

         A7: (s1 - (1 / (n + 1))) < t by A1, A3, SEQ_4:def 1;

        take t;

        s1 < (t + (1 / (n + 1))) by A7, XREAL_1: 19;

        then (s1 - t) < (1 / (n + 1)) by XREAL_1: 19;

        hence thesis by A6;

      end;

      consider f be sequence of REAL such that

       A8: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A5);

       A9:

      now

        let n;

        n in NAT by ORDINAL1:def 12;

        then ex q st q = (f . n) & q in X & (s1 - q) < (1 / (n + 1)) by A8;

        hence (f . n) in X & (s1 - (f . n)) < (1 / (n + 1));

      end;

      

       A10: ( rng f) c= X

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object such that

         A11: y in ( dom f) and

         A12: x = (f . y) by FUNCT_1:def 3;

        reconsider y as Element of NAT by A11, FUNCT_2:def 1;

        (f . y) in X by A9;

        hence thesis by A12;

      end;

       A13:

      now

        let s;

        assume

         A14: 0 < s;

        consider n such that

         A15: (s " ) < n by SEQ_4: 3;

        take k = n;

        let m;

        assume k <= m;

        then (k + 1) <= (m + 1) by XREAL_1: 6;

        then

         A16: (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

        (f . m) in X by A9;

        then (f . m) <= s1 by A3, SEQ_4:def 1;

        then

         A17: 0 <= (s1 - (f . m)) by XREAL_1: 48;

        ((s " ) + 0 ) < (n + 1) by A15, XREAL_1: 8;

        then (1 / (n + 1)) < (1 / (s " )) by A14, XREAL_1: 76;

        then (1 / (n + 1)) < s by XCMPLX_1: 216;

        then (1 / (m + 1)) < s by A16, XXREAL_0: 2;

        then (s1 - (f . m)) < s by A9, XXREAL_0: 2;

        then |.( - ((f . m) - s1)).| < s by A17, ABSVALUE:def 1;

        hence |.((f . m) - s1).| < s by COMPLEX1: 52;

      end;

      then

       A18: f is convergent;

      then ( lim f) = s1 by A13, SEQ_2:def 7;

      hence contradiction by A2, A4, A18, A10;

    end;

    theorem :: RCOMP_1:13

    

     Th13: for X st X <> {} & X is closed & X is bounded_below holds ( lower_bound X) in X

    proof

      let X such that

       A1: X <> {} and

       A2: X is closed and

       A3: X is bounded_below and

       A4: not ( lower_bound X) in X;

      set i1 = ( lower_bound X);

      defpred P[ Element of NAT , Element of REAL ] means ex q st q = $2 & q in X & (q - i1) < (1 / ($1 + 1));

      

       A5: for n be Element of NAT holds ex p be Element of REAL st P[n, p]

      proof

        let n be Element of NAT ;

         0 < ((n + 1) " );

        then 0 < (1 / (n + 1)) by XCMPLX_1: 215;

        then

        consider t such that

         A6: t in X and

         A7: t < (i1 + (1 / (n + 1))) by A1, A3, SEQ_4:def 2;

        take t;

        (t - i1) < (1 / (n + 1)) by A7, XREAL_1: 19;

        hence thesis by A6;

      end;

      consider f be sequence of REAL such that

       A8: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A5);

       A9:

      now

        let n;

        n in NAT by ORDINAL1:def 12;

        then ex q st q = (f . n) & q in X & (q - i1) < (1 / (n + 1)) by A8;

        hence (f . n) in X & ((f . n) - i1) < (1 / (n + 1));

      end;

      

       A10: ( rng f) c= X

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object such that

         A11: y in ( dom f) and

         A12: x = (f . y) by FUNCT_1:def 3;

        reconsider y as Element of NAT by A11, FUNCT_2:def 1;

        (f . y) in X by A9;

        hence thesis by A12;

      end;

       A13:

      now

        let s;

        assume

         A14: 0 < s;

        consider n such that

         A15: (s " ) < n by SEQ_4: 3;

        take k = n;

        let m;

        assume k <= m;

        then (k + 1) <= (m + 1) by XREAL_1: 6;

        then

         A16: (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

        (f . m) in X by A9;

        then i1 <= (f . m) by A3, SEQ_4:def 2;

        then

         A17: 0 <= ((f . m) - i1) by XREAL_1: 48;

        ((s " ) + 0 ) < (n + 1) by A15, XREAL_1: 8;

        then (1 / (n + 1)) < (1 / (s " )) by A14, XREAL_1: 76;

        then (1 / (n + 1)) < s by XCMPLX_1: 216;

        then (1 / (m + 1)) < s by A16, XXREAL_0: 2;

        then ((f . m) - i1) < s by A9, XXREAL_0: 2;

        hence |.((f . m) - i1).| < s by A17, ABSVALUE:def 1;

      end;

      then

       A18: f is convergent;

      then ( lim f) = i1 by A13, SEQ_2:def 7;

      hence contradiction by A2, A4, A18, A10;

    end;

    theorem :: RCOMP_1:14

    for X st X <> {} & X is compact holds ( upper_bound X) in X & ( lower_bound X) in X

    proof

      let X such that

       A1: X <> {} and

       A2: X is compact;

      X is real-bounded closed by A2, Th10;

      hence thesis by A1, Th12, Th13;

    end;

    theorem :: RCOMP_1:15

    X is compact & (for g1, g2 st g1 in X & g2 in X holds [.g1, g2.] c= X) implies ex p, g st X = [.p, g.]

    proof

      assume that

       A1: X is compact and

       A2: for g1, g2 st g1 in X & g2 in X holds [.g1, g2.] c= X;

      per cases ;

        suppose

         A3: X = {} ;

        take 1;

        take 0 ;

        thus thesis by A3, XXREAL_1: 29;

      end;

        suppose

         A4: X <> {} ;

        take p = ( lower_bound X), g = ( upper_bound X);

        

         A5: X is real-bounded closed by A1, Th10;

        now

          let r be Element of REAL ;

          assume r in X;

          then r <= g & p <= r by A5, SEQ_4:def 1, SEQ_4:def 2;

          hence r in [.p, g.];

        end;

        then

         A6: X c= [.p, g.];

        ( upper_bound X) in X & ( lower_bound X) in X by A4, A5, Th12, Th13;

        then [.p, g.] c= X by A2;

        hence thesis by A6;

      end;

    end;

    registration

      cluster open for Subset of REAL ;

      existence

      proof

        take ]. 0 , 1.[;

        thus thesis;

      end;

    end

    definition

      let r be Real;

      :: RCOMP_1:def6

      mode Neighbourhood of r -> Subset of REAL means

      : Def6: ex g st 0 < g & it = ].(r - g), (r + g).[;

      existence

      proof

        take ].(r - 1), (r + 1).[;

        thus thesis;

      end;

    end

    registration

      let r be Real;

      cluster -> open for Neighbourhood of r;

      coherence

      proof

        let A be Neighbourhood of r;

        ex g st 0 < g & A = ].(r - g), (r + g).[ by Def6;

        hence thesis;

      end;

    end

    theorem :: RCOMP_1:16

    for N be Neighbourhood of r holds r in N

    proof

      let N be Neighbourhood of r;

      (ex g st 0 < g & N = ].(r - g), (r + g).[) & |.(r - r).| = 0 by Def6, ABSVALUE: 2;

      hence thesis by Th1;

    end;

    theorem :: RCOMP_1:17

    for r holds for N1,N2 be Neighbourhood of r holds ex N be Neighbourhood of r st N c= N1 & N c= N2

    proof

      let r;

      let N1,N2 be Neighbourhood of r;

      consider g1 such that

       A1: 0 < g1 and

       A2: ].(r - g1), (r + g1).[ = N1 by Def6;

      consider g2 such that

       A3: 0 < g2 and

       A4: ].(r - g2), (r + g2).[ = N2 by Def6;

      set g = ( min (g1,g2));

       0 < g by A1, A3, XXREAL_0: 15;

      then

      reconsider N = ].(r - g), (r + g).[ as Neighbourhood of r by Def6;

      take N;

      

       A5: g <= g1 by XXREAL_0: 17;

      then

       A6: (r + g) <= (r + g1) by XREAL_1: 7;

      ( - g1) <= ( - g) by A5, XREAL_1: 24;

      then

       A7: (r + ( - g1)) <= (r + ( - g)) by XREAL_1: 7;

      

       A8: g <= g2 by XXREAL_0: 17;

      then ( - g2) <= ( - g) by XREAL_1: 24;

      then

       A9: (r + ( - g2)) <= (r + ( - g)) by XREAL_1: 7;

      

       A10: (r + g) <= (r + g2) by A8, XREAL_1: 7;

      now

        per cases ;

          suppose

           A11: g1 <= g2;

           A12:

          now

            let y be object;

            assume

             A13: y in ].(r - g), (r + g).[;

            then

            reconsider x1 = y as Real;

            ex p2 st y = p2 & (r - g) < p2 & p2 < (r + g) by A13;

            then x1 < (r + g2) & (r - g2) < x1 by A10, A9, XXREAL_0: 2;

            hence y in ].(r - g2), (r + g2).[;

          end;

          g1 = g by A11, XXREAL_0:def 9;

          hence ].(r - g), (r + g).[ c= N1 & ].(r - g), (r + g).[ c= N2 by A2, A4, A12;

        end;

          suppose

           A14: g2 <= g1;

           A15:

          now

            let y be object;

            assume

             A16: y in ].(r - g), (r + g).[;

            then

            reconsider x1 = y as Real;

            ex p2 st y = p2 & (r - g) < p2 & p2 < (r + g) by A16;

            then x1 < (r + g1) & (r - g1) < x1 by A6, A7, XXREAL_0: 2;

            hence y in ].(r - g1), (r + g1).[;

          end;

          g2 = g by A14, XXREAL_0:def 9;

          hence ].(r - g), (r + g).[ c= N1 & ].(r - g), (r + g).[ c= N2 by A2, A4, A15;

        end;

      end;

      hence thesis;

    end;

    theorem :: RCOMP_1:18

    

     Th18: for X be open Subset of REAL , r st r in X holds ex N be Neighbourhood of r st N c= X

    proof

      let X be open Subset of REAL , r;

      assume that

       A1: r in X and

       A2: for N be Neighbourhood of r holds not N c= X;

      defpred P[ Nat, Real] means $2 in ].(r - (1 / ($1 + 1))), (r + (1 / ($1 + 1))).[ & $2 in (X ` );

       A3:

      now

        let N be Neighbourhood of r;

        consider g such that 0 < g and

         A4: N = ].(r - g), (r + g).[ by Def6;

         not N c= X by A2;

        then

        consider x be object such that

         A5: x in N and

         A6: not x in X;

        consider s such that

         A7: x = s and (r - g) < s and s < (r + g) by A5, A4;

        reconsider s as Element of REAL by XREAL_0:def 1;

        take s;

        thus s in N by A5, A7;

        thus s in (X ` ) by A6, A7, XBOOLE_0:def 5;

      end;

      

       A8: for n be Element of NAT holds ex s be Element of REAL st P[n, s]

      proof

        let n be Element of NAT ;

         0 < (1 * ((n + 1) " ));

        then 0 < (1 / (n + 1)) by XCMPLX_0:def 9;

        then

        reconsider N = ].(r - (1 / (n + 1))), (r + (1 / (n + 1))).[ as Neighbourhood of r by Def6;

        ex s be Element of REAL st s in N & s in (X ` ) by A3;

        hence thesis;

      end;

      consider s3 such that

       A9: for n be Element of NAT holds P[n, (s3 . n)] from FUNCT_2:sch 3( A8);

      deffunc G( Nat) = (r + (1 / ($1 + 1)));

      deffunc F( Nat) = (r - (1 / ($1 + 1)));

      consider s1 be Real_Sequence such that

       A10: for n holds (s1 . n) = F(n) from SEQ_1:sch 1;

      consider s2 be Real_Sequence such that

       A11: for n holds (s2 . n) = G(n) from SEQ_1:sch 1;

      

       A12: for n holds (s1 . n) <= (s3 . n) & (s3 . n) <= (s2 . n)

      proof

        let n;

        n in NAT by ORDINAL1:def 12;

        then (s3 . n) in ].(r - (1 / (n + 1))), (r + (1 / (n + 1))).[ by A9;

        then

         A13: ex s st s = (s3 . n) & (r - (1 / (n + 1))) < s & s < (r + (1 / (n + 1)));

        hence (s1 . n) <= (s3 . n) by A10;

        thus thesis by A11, A13;

      end;

      

       A14: ( rng s3) c= (X ` )

      proof

        let x be object;

        assume x in ( rng s3);

        then

        consider y be object such that

         A15: y in ( dom s3) and

         A16: (s3 . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A15, FUNCT_2:def 1;

        (s3 . y) in (X ` ) by A9;

        hence thesis by A16;

      end;

      

       A17: (X ` ) is closed by Def5;

       A18:

      now

        let s;

        assume

         A19: 0 < s;

        consider n such that

         A20: (s " ) < n by SEQ_4: 3;

        take n;

        let m;

        assume n <= m;

        then (n + 1) <= (m + 1) by XREAL_1: 6;

        then

         A21: (1 / (m + 1)) <= (1 / (n + 1)) by XREAL_1: 118;

        ((s " ) + 0 ) < (n + 1) by A20, XREAL_1: 8;

        then (1 / (n + 1)) < (1 / (s " )) by A19, XREAL_1: 76;

        then

         A22: (1 / (n + 1)) < s by XCMPLX_1: 216;

         |.((s2 . m) - r).| = |.((r + (1 / (m + 1))) - r).| by A11

        .= (1 / (m + 1)) by ABSVALUE:def 1;

        hence |.((s2 . m) - r).| < s by A22, A21, XXREAL_0: 2;

      end;

      then

       A23: s2 is convergent;

      then

       A24: ( lim s2) = r by A18, SEQ_2:def 7;

       A25:

      now

        let s;

        assume

         A26: 0 < s;

        consider n such that

         A27: (s " ) < n by SEQ_4: 3;

        take n;

        let m;

        assume n <= m;

        then (n + 1) <= (m + 1) by XREAL_1: 6;

        then

         A28: (1 / (m + 1)) <= (1 / (n + 1)) by XREAL_1: 118;

        ((s " ) + 0 ) < (n + 1) by A27, XREAL_1: 8;

        then (1 / (n + 1)) < (1 / (s " )) by A26, XREAL_1: 76;

        then

         A29: (1 / (n + 1)) < s by XCMPLX_1: 216;

         |.((s1 . m) - r).| = |.((r - (1 / (m + 1))) - r).| by A10

        .= |.( - (1 / (m + 1))).|

        .= |.(1 / (m + 1)).| by COMPLEX1: 52

        .= (1 / (m + 1)) by ABSVALUE:def 1;

        hence |.((s1 . m) - r).| < s by A29, A28, XXREAL_0: 2;

      end;

      then

       A30: s1 is convergent;

      then ( lim s1) = r by A25, SEQ_2:def 7;

      then s3 is convergent & ( lim s3) = r by A30, A23, A24, A12, SEQ_2: 19, SEQ_2: 20;

      then r in (X ` ) by A14, A17;

      hence contradiction by A1, XBOOLE_0:def 5;

    end;

    theorem :: RCOMP_1:19

    for X be open Subset of REAL , r st r in X holds ex g st 0 < g & ].(r - g), (r + g).[ c= X

    proof

      let X be open Subset of REAL , r;

      assume r in X;

      then

      consider N be Neighbourhood of r such that

       A1: N c= X by Th18;

      consider g such that

       A2: 0 < g & N = ].(r - g), (r + g).[ by Def6;

      take g;

      thus thesis by A1, A2;

    end;

    theorem :: RCOMP_1:20

    (for r be Element of REAL st r in X holds ex N be Neighbourhood of r st N c= X) implies X is open

    proof

      assume that

       A1: for r be Element of REAL st r in X holds ex N be Neighbourhood of r st N c= X and

       A2: not X is open;

       not (X ` ) is closed by A2;

      then

      consider s1 such that

       A3: ( rng s1) c= (X ` ) and

       A4: s1 is convergent and

       A5: not ( lim s1) in (X ` );

      reconsider ls = ( lim s1) as Element of REAL by XREAL_0:def 1;

      consider N be Neighbourhood of ls such that

       A6: N c= X by A1, A5, SUBSET_1: 29;

      consider g such that

       A7: 0 < g and

       A8: ].(( lim s1) - g), (( lim s1) + g).[ = N by Def6;

      consider n such that

       A9: for m st n <= m holds |.((s1 . m) - ( lim s1)).| < g by A4, A7, SEQ_2:def 7;

      n in NAT by ORDINAL1:def 12;

      then n in ( dom s1) by FUNCT_2:def 1;

      then

       A10: (s1 . n) in ( rng s1) by FUNCT_1:def 3;

      

       A11: |.((s1 . n) - ( lim s1)).| < g by A9;

      then ((s1 . n) - ( lim s1)) < g by SEQ_2: 1;

      then

       A12: (s1 . n) < (( lim s1) + g) by XREAL_1: 19;

      ( - g) < ((s1 . n) - ( lim s1)) by A11, SEQ_2: 1;

      then (( lim s1) + ( - g)) < (( lim s1) + ((s1 . n) - ( lim s1))) by XREAL_1: 6;

      then (s1 . n) in { s : (( lim s1) - g) < s & s < (( lim s1) + g) } by A12;

      hence contradiction by A3, A6, A8, A10, XBOOLE_0:def 5;

    end;

    theorem :: RCOMP_1:21

    

     Th21: X is open bounded_above implies not ( upper_bound X) in X

    proof

      assume that

       A1: X is open and

       A2: X is bounded_above;

      assume ( upper_bound X) in X;

      then

      consider N be Neighbourhood of ( upper_bound X) such that

       A3: N c= X by A1, Th18;

      consider t such that

       A4: t > 0 and

       A5: N = ].(( upper_bound X) - t), (( upper_bound X) + t).[ by Def6;

      

       A6: (( upper_bound X) + (t / 2)) > ( upper_bound X) by A4, XREAL_1: 29, XREAL_1: 215;

      

       A7: ((( upper_bound X) + (t / 2)) + (t / 2)) > (( upper_bound X) + (t / 2)) by A4, XREAL_1: 29, XREAL_1: 215;

      (( upper_bound X) - t) < ( upper_bound X) by A4, XREAL_1: 44;

      then (( upper_bound X) - t) < (( upper_bound X) + (t / 2)) by A6, XXREAL_0: 2;

      then (( upper_bound X) + (t / 2)) in { s : (( upper_bound X) - t) < s & s < (( upper_bound X) + t) } by A7;

      hence contradiction by A2, A3, A5, A6, SEQ_4:def 1;

    end;

    theorem :: RCOMP_1:22

    

     Th22: X is open bounded_below implies not ( lower_bound X) in X

    proof

      assume that

       A1: X is open and

       A2: X is bounded_below;

      assume ( lower_bound X) in X;

      then

      consider N be Neighbourhood of ( lower_bound X) such that

       A3: N c= X by A1, Th18;

      consider t such that

       A4: t > 0 and

       A5: N = ].(( lower_bound X) - t), (( lower_bound X) + t).[ by Def6;

      

       A6: (( lower_bound X) - (t / 2)) < ( lower_bound X) by A4, XREAL_1: 44, XREAL_1: 215;

      

       A7: ((( lower_bound X) - (t / 2)) - (t / 2)) < (( lower_bound X) - (t / 2)) by A4, XREAL_1: 44, XREAL_1: 215;

      ( lower_bound X) < (( lower_bound X) + t) by A4, XREAL_1: 29;

      then (( lower_bound X) - (t / 2)) < (( lower_bound X) + t) by A6, XXREAL_0: 2;

      then (( lower_bound X) - (t / 2)) in { s : (( lower_bound X) - t) < s & s < (( lower_bound X) + t) } by A7;

      hence contradiction by A2, A3, A5, A6, SEQ_4:def 2;

    end;

    theorem :: RCOMP_1:23

    X is open real-bounded & (for g1, g2 st g1 in X & g2 in X holds [.g1, g2.] c= X) implies ex p, g st X = ].p, g.[

    proof

      assume that

       A1: X is open and

       A2: X is real-bounded and

       A3: for g1, g2 st g1 in X & g2 in X holds [.g1, g2.] c= X;

      per cases ;

        suppose

         A4: X = {} ;

        take 1;

        take 0 ;

        thus thesis by A4, XXREAL_1: 28;

      end;

        suppose

         A5: X <> {} ;

        take p = ( lower_bound X), g = ( upper_bound X);

        now

          let r be Element of REAL ;

          thus r in X implies r in ].p, g.[

          proof

            assume

             A6: r in X;

            then p <> r & p <= r by A1, A2, Th22, SEQ_4:def 2;

            then

             A7: p < r by XXREAL_0: 1;

            g <> r & r <= g by A1, A2, A6, Th21, SEQ_4:def 1;

            then r < g by XXREAL_0: 1;

            hence thesis by A7;

          end;

          assume r in ].p, g.[;

          then

           A8: ex s st s = r & p < s & s < g;

          then (g - r) > 0 by XREAL_1: 50;

          then

          consider g2 such that

           A9: g2 in X & (g - (g - r)) < g2 by A2, A5, SEQ_4:def 1;

          (r - p) > 0 by A8, XREAL_1: 50;

          then

          consider g1 such that

           A10: g1 in X & g1 < (p + (r - p)) by A2, A5, SEQ_4:def 2;

          reconsider g1, g2 as Real;

          r in { s : g1 <= s & s <= g2 } & [.g1, g2.] c= X by A3, A9, A10;

          hence r in X;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end;

    definition

      let g be Real, s be ExtReal;

      :: original: [.

      redefine

      :: RCOMP_1:def7

      func [.g,s.[ -> Subset of REAL equals { r : g <= r & r < s };

      coherence

      proof

        now

          let e be object;

          assume e in [.g, s.[;

          then

           A1: ex r be Element of ExtREAL st e = r & g <= r & r < s;

          g in REAL by XREAL_0:def 1;

          hence e in REAL by A1, XXREAL_0: 46;

        end;

        hence thesis by TARSKI:def 3;

      end;

      compatibility

      proof

        set Y = { r : g <= r & r < s };

        let X be Subset of REAL ;

        

         A2: [.g, s.[ c= Y

        proof

          let e be object;

          assume e in [.g, s.[;

          then

          consider r be Element of ExtREAL such that

           A3: e = r and

           A4: g <= r & r < s;

          g in REAL by XREAL_0:def 1;

          then r in REAL by A4, XXREAL_0: 46;

          hence thesis by A3, A4;

        end;

        Y c= [.g, s.[

        proof

          let e be object;

          assume e in Y;

          then

          consider r such that

           A5: e = r & g <= r & r < s;

          r in REAL by XREAL_0:def 1;

          hence thesis by A5, NUMBERS: 31;

        end;

        hence thesis by A2;

      end;

    end

    definition

      let g be ExtReal, s be Real;

      :: original: ].

      redefine

      :: RCOMP_1:def8

      func ].g,s.] -> Subset of REAL equals { r : g < r & r <= s };

      coherence

      proof

        now

          let e be object;

          assume e in ].g, s.];

          then

           A1: ex r be Element of ExtREAL st e = r & g < r & r <= s;

          s in REAL by XREAL_0:def 1;

          hence e in REAL by A1, XXREAL_0: 47;

        end;

        hence thesis by TARSKI:def 3;

      end;

      compatibility

      proof

        set Y = { r : g < r & r <= s };

        let X be Subset of REAL ;

        

         A2: ].g, s.] c= Y

        proof

          let e be object;

          assume e in ].g, s.];

          then

          consider r be Element of ExtREAL such that

           A3: e = r and

           A4: g < r & r <= s;

          s in REAL by XREAL_0:def 1;

          then r in REAL by A4, XXREAL_0: 47;

          hence thesis by A3, A4;

        end;

        Y c= ].g, s.]

        proof

          let e be object;

          assume e in Y;

          then

          consider r such that

           A5: e = r & g < r & r <= s;

          r in REAL by XREAL_0:def 1;

          hence thesis by A5, NUMBERS: 31;

        end;

        hence thesis by A2;

      end;

    end