pscomp_1.miz



    begin

    reserve r,s,t,g for Real,

r3,r1,r2,q3,p3 for Real;

    

     Lm1: for X be Subset of REAL st X is bounded_below holds ( -- X) is bounded_above

    proof

      let X be Subset of REAL ;

      given s such that

       A1: s is LowerBound of X;

      take ( - s);

      let t be ExtReal;

      assume t in ( -- X);

      then t in { ( - r2) where r2 be Complex : r2 in X } by MEMBER_1:def 2;

      then

      consider r2 be Complex such that

       A2: t = ( - r2) and

       A3: r2 in X;

      reconsider r3 = r2 as Real by A3;

      r3 >= s by A1, A3, XXREAL_2:def 2;

      hence thesis by A2, XREAL_1: 24;

    end;

    

     Lm2: for X be non empty set, f be Function of X, REAL st f is with_min holds ( - f) is with_max

    proof

      let X be non empty set, f be Function of X, REAL ;

      assume that

       A1: (f .: X) is bounded_below and

       A2: ( lower_bound (f .: X)) in (f .: X);

      

       A3: ( -- (f .: X)) = (( - f) .: X) by MEASURE6: 65;

      hence (( - f) .: X) is bounded_above by A1, Lm1;

      

      then

       A4: ( upper_bound (( - f) .: X)) = ( - ( lower_bound ( -- ( -- (f .: X))))) by A3, MEASURE6: 44

      .= ( - ( lower_bound (f .: X)));

      ( - ( lower_bound (f .: X))) in ( -- (f .: X)) by A2, MEMBER_1: 11;

      hence thesis by A4, MEASURE6: 65;

    end;

    begin

    definition

      let T be 1-sorted;

      mode RealMap of T is Function of the carrier of T, REAL ;

    end

    registration

      let T be non empty 1-sorted;

      cluster bounded for RealMap of T;

      existence

      proof

        set c = the carrier of T;

        reconsider f = (c --> ( In ( 0 , REAL ))) as RealMap of T;

        take f;

        ( dom f) = c & ( rng f) = { 0 qua Real} by FUNCOP_1: 8, FUNCT_2:def 1;

        hence (f .: c) is bounded_above by RELAT_1: 113;

        thus (f .: c) is bounded_below;

      end;

    end

    definition

      let T be 1-sorted, f be RealMap of T;

      :: PSCOMP_1:def1

      func lower_bound f -> Real equals ( lower_bound (f .: the carrier of T));

      coherence ;

      :: PSCOMP_1:def2

      func upper_bound f -> Real equals ( upper_bound (f .: the carrier of T));

      coherence ;

    end

    theorem :: PSCOMP_1:1

    

     Th1: for T be non empty TopSpace, f be bounded_below RealMap of T holds for p be Point of T holds (f . p) >= ( lower_bound f)

    proof

      let T be non empty TopSpace, f be bounded_below RealMap of T;

      set fc = (f .: the carrier of T);

      let p be Point of T;

      fc is bounded_below & (f . p) in fc by FUNCT_2: 35, MEASURE6:def 10;

      hence thesis by SEQ_4:def 2;

    end;

    theorem :: PSCOMP_1:2

    for T be non empty TopSpace, f be bounded_below RealMap of T holds for s be Real st for t be Point of T holds (f . t) >= s holds ( lower_bound f) >= s

    proof

      let T be non empty TopSpace, f be bounded_below RealMap of T;

      set c = the carrier of T;

      set fc = (f .: the carrier of T);

      let s be Real;

      assume

       A1: for t be Point of T holds (f . t) >= s;

      now

        let p1 be Real;

        assume p1 in fc;

        then ex x be object st x in c & x in c & p1 = (f . x) by FUNCT_2: 64;

        hence p1 >= s by A1;

      end;

      hence thesis by SEQ_4: 43;

    end;

    theorem :: PSCOMP_1:3

    for T be non empty TopSpace, f be RealMap of T st (for p be Point of T holds (f . p) >= r) & for t st for p be Point of T holds (f . p) >= t holds r >= t holds r = ( lower_bound f)

    proof

      let T be non empty TopSpace, f be RealMap of T;

      set c = the carrier of T;

      set fc = (f .: the carrier of T);

      assume that

       A1: for p be Point of T holds (f . p) >= r and

       A2: for t st for p be Point of T holds (f . p) >= t holds r >= t;

       A3:

      now

        let t;

        assume for s st s in fc holds s >= t;

        then for s be Point of T holds (f . s) >= t by FUNCT_2: 35;

        hence r >= t by A2;

      end;

      now

        let s;

        assume s in fc;

        then ex x be object st x in c & x in c & s = (f . x) by FUNCT_2: 64;

        hence s >= r by A1;

      end;

      hence thesis by A3, SEQ_4: 44;

    end;

    theorem :: PSCOMP_1:4

    

     Th4: for T be non empty TopSpace, f be bounded_above RealMap of T holds for p be Point of T holds (f . p) <= ( upper_bound f)

    proof

      let T be non empty TopSpace, f be bounded_above RealMap of T;

      set fc = (f .: the carrier of T);

      let p be Point of T;

      fc is bounded_above & (f . p) in fc by FUNCT_2: 35, MEASURE6:def 11;

      hence thesis by SEQ_4:def 1;

    end;

    theorem :: PSCOMP_1:5

    for T be non empty TopSpace, f be bounded_above RealMap of T holds for t st for p be Point of T holds (f . p) <= t holds ( upper_bound f) <= t

    proof

      let T be non empty TopSpace, f be bounded_above RealMap of T;

      set c = the carrier of T;

      set fc = (f .: the carrier of T);

      let t;

      assume

       A1: for p be Point of T holds (f . p) <= t;

      now

        let s;

        assume s in fc;

        then ex x be object st x in c & x in c & s = (f . x) by FUNCT_2: 64;

        hence s <= t by A1;

      end;

      hence thesis by SEQ_4: 45;

    end;

    theorem :: PSCOMP_1:6

    for T be non empty TopSpace, f be RealMap of T st (for p be Point of T holds (f . p) <= r) & (for t st for p be Point of T holds (f . p) <= t holds r <= t) holds r = ( upper_bound f)

    proof

      let T be non empty TopSpace, f be RealMap of T;

      set c = the carrier of T;

      set fc = (f .: the carrier of T);

      assume that

       A1: for p be Point of T holds (f . p) <= r and

       A2: for t st for p be Point of T holds (f . p) <= t holds r <= t;

       A3:

      now

        let t;

        assume for s st s in fc holds s <= t;

        then for s be Point of T holds (f . s) <= t by FUNCT_2: 35;

        hence r <= t by A2;

      end;

      now

        let s;

        assume s in fc;

        then ex x be object st x in c & x in c & s = (f . x) by FUNCT_2: 64;

        hence s <= r by A1;

      end;

      hence thesis by A3, SEQ_4: 46;

    end;

    theorem :: PSCOMP_1:7

    

     Th7: for T be non empty 1-sorted, f be bounded RealMap of T holds ( lower_bound f) <= ( upper_bound f)

    proof

      let T be non empty 1-sorted, f be bounded RealMap of T;

      (f .: the carrier of T) is bounded_below & (f .: the carrier of T) is bounded_above by MEASURE6:def 10, MEASURE6:def 11;

      hence thesis by SEQ_4: 11;

    end;

    definition

      let T be TopStruct, f be RealMap of T;

      :: PSCOMP_1:def3

      attr f is continuous means for Y be Subset of REAL st Y is closed holds (f " Y) is closed;

    end

    registration

      let T be non empty TopSpace;

      cluster continuous for RealMap of T;

      existence

      proof

        set c = the carrier of T;

        reconsider f = (c --> ( In ( 0 , REAL ))) as RealMap of T;

        take f;

        

         A1: ( dom f) = c by FUNCT_2:def 1;

        let Y be Subset of REAL ;

        

         A2: ( rng f) = { 0 qua Real} by FUNCOP_1: 8;

        assume Y is closed;

        per cases ;

          suppose 0 in Y;

          then

           A3: ( rng f) c= Y by A2, ZFMISC_1: 31;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " ( rng f)) by A3, XBOOLE_1: 28

          .= ( [#] T) by A1, RELAT_1: 134;

          hence thesis;

        end;

          suppose not 0 in Y;

          then

           A4: ( rng f) misses Y by A2, ZFMISC_1: 50;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " {} ) by A4, XBOOLE_0:def 7

          .= ( {} T);

          hence thesis;

        end;

      end;

    end

    registration

      let T be non empty TopSpace, S be non empty SubSpace of T;

      cluster continuous for RealMap of S;

      existence

      proof

        set c = the carrier of S;

        reconsider f = (c --> ( In ( 0 , REAL ))) as RealMap of S;

        take f;

        

         A1: ( dom f) = c by FUNCT_2:def 1;

        let Y be Subset of REAL ;

        

         A2: ( rng f) = { 0 qua Real} by FUNCOP_1: 8;

        assume Y is closed;

        per cases ;

          suppose 0 in Y;

          then

           A3: ( rng f) c= Y by A2, ZFMISC_1: 31;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " ( rng f)) by A3, XBOOLE_1: 28

          .= ( [#] S) by A1, RELAT_1: 134;

          hence thesis;

        end;

          suppose not 0 in Y;

          then

           A4: ( rng f) misses Y by A2, ZFMISC_1: 50;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " {} ) by A4, XBOOLE_0:def 7

          .= ( {} S);

          hence thesis;

        end;

      end;

    end

    reserve T for TopStruct,

f for RealMap of T;

    theorem :: PSCOMP_1:8

    

     Th8: f is continuous iff for Y be Subset of REAL st Y is open holds (f " Y) is open

    proof

      hereby

        assume

         A1: f is continuous;

        let Y be Subset of REAL ;

        assume Y is open;

        then (Y ` ) is closed;

        then

         A2: (f " (Y ` )) is closed by A1;

        (f " (Y ` )) = ((f " REAL ) \ (f " Y)) by FUNCT_1: 69

        .= (( [#] T) \ (f " Y)) by FUNCT_2: 40;

        then (( [#] T) \ (( [#] T) \ (f " Y))) is open by A2, PRE_TOPC:def 3;

        hence (f " Y) is open by PRE_TOPC: 3;

      end;

      assume

       A3: for Y be Subset of REAL st Y is open holds (f " Y) is open;

      let Y be Subset of REAL ;

      assume Y is closed;

      then (Y ` ) is open;

      then

       A4: (f " (Y ` )) is open by A3;

      (f " (Y ` )) = ((f " REAL ) \ (f " Y)) by FUNCT_1: 69

      .= (( [#] T) \ (f " Y)) by FUNCT_2: 40;

      hence thesis by A4, PRE_TOPC:def 3;

    end;

    theorem :: PSCOMP_1:9

    

     Th9: f is continuous implies ( - f) is continuous

    proof

      assume

       A1: f is continuous;

      let X be Subset of REAL ;

      assume X is closed;

      then

       A2: ( -- X) is closed by MEASURE6: 45;

      (( - f) " X) = (f " ( -- X)) by MEASURE6: 68;

      hence thesis by A1, A2;

    end;

    theorem :: PSCOMP_1:10

    

     Th10: f is continuous implies (r3 + f) is continuous

    proof

      assume

       A1: f is continuous;

      let X be Subset of REAL ;

      assume X is closed;

      then

       A2: (( - r3) ++ X) is closed by MEASURE6: 53;

      ((r3 + f) " X) = (f " (( - r3) ++ X)) by MEASURE6: 70;

      hence thesis by A1, A2;

    end;

    theorem :: PSCOMP_1:11

    

     Th11: f is continuous & not 0 in ( rng f) implies ( Inv f) is continuous

    proof

      assume that

       A1: f is continuous and

       A2: not 0 in ( rng f);

      let X0 be Subset of REAL ;

       0 in { 0 } by TARSKI:def 1;

      then not 0 in (X0 \ { 0 }) by XBOOLE_0:def 5;

      then

      reconsider X = (X0 \ { 0 }) as without_zero Subset of REAL by MEASURE6:def 2;

      set X9 = ( Inv X);

      

       A3: (X0 \ { 0 }) c= X0 by XBOOLE_1: 36;

      set X9r = (X9 /\ ( rng f));

      assume

       A4: X0 is closed;

      now

        let x be object;

        hereby

          

           A5: X9r c= ( Cl X9r) by MEASURE6: 58;

          assume

           A6: x in X9r;

          then x in ( rng f) by XBOOLE_0:def 4;

          hence x in (( Cl X9r) /\ ( rng f)) by A6, A5, XBOOLE_0:def 4;

        end;

        assume

         A7: x in (( Cl X9r) /\ ( rng f));

        then

        reconsider s = x as Real;

        x in ( Cl X9r) by A7, XBOOLE_0:def 4;

        then

        consider seq be Real_Sequence such that

         A8: ( rng seq) c= X9r and

         A9: seq is convergent and

         A10: ( lim seq) = s by MEASURE6: 64;

        assume

         A11: not x in X9r;

        

         A12: x in ( rng f) by A7, XBOOLE_0:def 4;

        now

          ( rng (seq " )) c= X

          proof

            let y be object;

            assume y in ( rng (seq " ));

            then

            consider n be object such that

             A13: n in ( dom (seq " )) and

             A14: y = ((seq " ) . n) by FUNCT_1:def 3;

            reconsider n as Element of NAT by A13;

            (seq . n) in ( rng seq) by FUNCT_2: 4;

            then

             A15: (1 / (1 / (seq . n))) in X9 by A8, XBOOLE_0:def 4;

            ((seq " ) . n) = ((seq . n) " ) by VALUED_1: 10

            .= (1 / (seq . n));

            hence thesis by A14, A15, MEASURE6: 54;

          end;

          then

           A16: ( rng (seq " )) c= X0 by A3;

          assume

           A17: ( lim seq) <> 0 ;

          now

            let n be Nat;

            

             A18: n in NAT by ORDINAL1:def 12;

            assume (seq . n) = 0 ;

            then 0 in ( rng seq) by FUNCT_2: 4, A18;

            hence contradiction by A2, A8, XBOOLE_0:def 4;

          end;

          then

           A19: seq is non-zero by SEQ_1: 5;

          then (seq " ) is convergent by A9, A17, SEQ_2: 21;

          then

           A20: ( lim (seq " )) in X0 by A4, A16;

          

           A21: ( lim (seq " )) = (( lim seq) " ) by A9, A17, A19, SEQ_2: 22;

          then ( lim (seq " )) <> 0 by A17;

          then not ( lim (seq " )) in { 0 } by TARSKI:def 1;

          then ( lim (seq " )) in X by A20, XBOOLE_0:def 5;

          then (1 / ( lim (seq " ))) in X9;

          hence contradiction by A12, A10, A11, A21, XBOOLE_0:def 4;

        end;

        hence contradiction by A2, A7, A10, XBOOLE_0:def 4;

      end;

      then

       A22: X9r = (( Cl X9r) /\ ( rng f)) by TARSKI: 2;

      (f " ( Cl X9r)) is closed by A1;

      then

       A23: (f " X9r) is closed by A22, RELAT_1: 133;

       A24:

      now

        let x be object;

        hereby

          assume

           A25: x in (( Inv f) " X0);

          then

           A26: (( Inv f) . x) in X0 by FUNCT_2: 38;

          reconsider xx = x as set by TARSKI: 1;

          now

            assume not (( Inv f) . x) in X;

            then (( Inv f) . x) in { 0 } by A26, XBOOLE_0:def 5;

            then (( Inv f) . x) = 0 by TARSKI:def 1;

            then 0 = ((f . xx) " ) by VALUED_1: 10;

            hence contradiction by A2, A25, FUNCT_2: 4, XCMPLX_1: 202;

          end;

          hence x in (( Inv f) " X) by A25, FUNCT_2: 38;

        end;

        (( Inv f) " X) c= (( Inv f) " X0) by RELAT_1: 143, XBOOLE_1: 36;

        hence x in (( Inv f) " X) implies x in (( Inv f) " X0);

      end;

      (f " X9) = (f " X9r) & (( Inv f) " X) = (f " ( Inv X)) by MEASURE6: 71, RELAT_1: 133;

      hence thesis by A23, A24, TARSKI: 2;

    end;

    theorem :: PSCOMP_1:12

    for R be Subset-Family of REAL st f is continuous & R is open holds (( " f) .: R) is open

    proof

      let R be Subset-Family of REAL ;

      assume

       A1: f is continuous;

      assume

       A2: R is open;

      let P be Subset of T;

      assume P in (( " f) .: R);

      then

      consider eR be object such that

       A3: eR in ( bool REAL ) and

       A4: eR in R and

       A5: P = (( " f) . eR) by FUNCT_2: 64;

      reconsider eR as set by TARSKI: 1;

      

       A6: P = (f " eR) by A3, A5, MEASURE6:def 3;

      reconsider eR as Subset of REAL by A3;

      eR is open by A2, A4;

      hence thesis by A1, A6, Th8;

    end;

    theorem :: PSCOMP_1:13

    

     Th13: for R be Subset-Family of REAL st f is continuous & R is closed holds (( " f) .: R) is closed

    proof

      let R be Subset-Family of REAL ;

      assume

       A1: f is continuous;

      assume

       A2: R is closed;

      let P be Subset of T;

      assume P in (( " f) .: R);

      then

      consider eR be object such that

       A3: eR in ( bool REAL ) and

       A4: eR in R and

       A5: P = (( " f) . eR) by FUNCT_2: 64;

      reconsider eR as set by TARSKI: 1;

      

       A6: P = (f " eR) by A3, A5, MEASURE6:def 3;

      reconsider eR as Subset of REAL by A3;

      eR is closed by A2, A4;

      hence thesis by A1, A6;

    end;

    definition

      let T be non empty TopStruct, f be RealMap of T, X be Subset of T;

      :: original: |

      redefine

      func f | X -> RealMap of (T | X) ;

      coherence

      proof

        the carrier of (T | X) = X by PRE_TOPC: 8;

        hence thesis by FUNCT_2: 32;

      end;

    end

    registration

      let T be non empty TopSpace, f be continuous RealMap of T, X be Subset of T;

      cluster (f | X) -> continuous;

      coherence

      proof

        now

          let Y be Subset of REAL ;

          assume Y is open;

          then

           A1: (f " Y) is open by Th8;

          the carrier of (T | X) = X & ((f | X) " Y) = (X /\ (f " Y)) by FUNCT_1: 70, PRE_TOPC: 8;

          hence ((f | X) " Y) is open by A1, TSP_1:def 1;

        end;

        hence thesis by Th8;

      end;

    end

    registration

      let T be non empty TopSpace, P be compact non empty Subset of T;

      cluster (T | P) -> compact;

      coherence by COMPTS_1: 3;

    end

    begin

    theorem :: PSCOMP_1:14

    

     Th14: for T be non empty TopSpace holds (for f be RealMap of T st f is continuous holds f is with_max) iff for f be RealMap of T st f is continuous holds f is with_min

    proof

      let T be non empty TopSpace;

      hereby

        assume

         A1: for f be RealMap of T st f is continuous holds f is with_max;

        let f be RealMap of T;

        assume f is continuous;

        then ( - f) is continuous by Th9;

        then ( - f) is with_max by A1;

        hence f is with_min by MEASURE6: 66;

      end;

      assume

       A2: for f be RealMap of T st f is continuous holds f is with_min;

      let f be RealMap of T;

      assume f is continuous;

      then ( - f) is continuous by Th9;

      then ( - ( - f)) is with_max by A2, Lm2;

      hence thesis;

    end;

    theorem :: PSCOMP_1:15

    

     Th15: for T be non empty TopSpace holds (for f be RealMap of T st f is continuous holds f is bounded) iff for f be RealMap of T st f is continuous holds f is with_max

    proof

      let T be non empty TopSpace;

      set cT = the carrier of T;

      hereby

        assume

         A1: for f be RealMap of T st f is continuous holds f is bounded;

        let f be RealMap of T such that

         A2: f is continuous;

        set fcT = (f .: cT);

        f is bounded by A1, A2;

        then

         A3: fcT is bounded_above by MEASURE6:def 11;

        set b = ( upper_bound fcT);

        set bf = (b + ( - f));

        ( - f) is continuous by A2, Th9;

        then

         A4: bf is continuous by Th10;

        reconsider bf9 = bf as Function of cT, REAL ;

        reconsider f9 = f as Function of cT, REAL ;

        set g = ( Inv bf);

        set gcT = (g .: cT);

        assume not f is with_max;

        then

         A5: not fcT is with_max;

        then

         A6: not ( upper_bound fcT) in fcT by A3;

        now

          assume 0 in ( rng bf);

          then

          consider x be object such that

           A7: x in ( dom bf) and

           A8: (bf . x) = 0 by FUNCT_1:def 3;

          reconsider x as Element of cT by A7;

          (bf9 . x) = (b + (( - f9) . x)) by VALUED_1: 2

          .= (b + ( - (f . x))) by VALUED_1: 8

          .= (b - (f . x));

          hence contradiction by A6, A8, FUNCT_2: 35;

        end;

        then

         A9: g is continuous by A4, Th11;

        now

          g is bounded by A1, A9;

          then gcT is bounded_above by MEASURE6:def 11;

          then

          consider p be Real such that

           A10: p is UpperBound of gcT;

          

           A11: for r be Real st r in gcT holds r <= p by A10, XXREAL_2:def 1;

          per cases ;

            suppose

             A12: p <= 0 ;

            reconsider a19 = 1 as Real;

            take a19;

            thus a19 > 0 ;

            let r be Real;

            assume r in gcT;

            hence r <= a19 by A11, A12;

          end;

            suppose

             A13: p > 0 ;

            take p;

            thus p > 0 by A13;

            thus for r be Real st r in gcT holds r <= p by A11;

          end;

        end;

        then

        consider p be Real such that

         A14: p > 0 and

         A15: for r be Real st r in gcT holds r <= p;

        consider r be Real such that

         A16: r in fcT and

         A17: (b - (1 / p)) < r by A3, A14, SEQ_4:def 1;

        consider x be object such that

         A18: x in the carrier of T and x in the carrier of T and

         A19: r = (f . x) by A16, FUNCT_2: 64;

        reconsider x as Element of T by A18;

        

         A20: (f . x) <= b by A3, A16, A19, SEQ_4:def 1;

        (f . x) <> b by A3, A5, A16, A19;

        then ((f . x) + 0 ) < b by A20, XXREAL_0: 1;

        then

         A21: (b - (f . x)) > 0 by XREAL_1: 20;

        (g . x) = ((bf9 . x) " ) by VALUED_1: 10

        .= ((b + (( - f9) . x)) " ) by VALUED_1: 2

        .= (1 / (b + (( - f9) . x)))

        .= (1 / (b + ( - (f . x)))) by VALUED_1: 8

        .= (1 / (b - (f . x)));

        then (1 / (b - (f . x))) <= p by A15, FUNCT_2: 35;

        then 1 <= (p * (b - (f . x))) by A21, XREAL_1: 81;

        then (1 / p) <= (b - (f . x)) by A14, XREAL_1: 79;

        then ((f . x) + (1 / p)) <= b by XREAL_1: 19;

        hence contradiction by A17, A19, XREAL_1: 19;

      end;

      assume

       A22: for f be RealMap of T st f is continuous holds f is with_max;

      let f be RealMap of T;

      assume

       A23: f is continuous;

      then f is with_max by A22;

      then (f .: the carrier of T) is with_max;

      then (f .: the carrier of T) is bounded_above;

      hence f is bounded_above;

      f is with_min by A22, A23, Th14;

      then (f .: the carrier of T) is with_min;

      then (f .: the carrier of T) is bounded_below;

      hence thesis;

    end;

    definition

      let T be TopStruct;

      :: PSCOMP_1:def4

      attr T is pseudocompact means

      : Def4: for f be RealMap of T st f is continuous holds f is bounded;

    end

    registration

      cluster compact -> pseudocompact for non empty TopSpace;

      coherence

      proof

        let T be non empty TopSpace;

        assume

         A1: T is compact;

        let f be RealMap of T such that

         A2: f is continuous;

        thus f is bounded_above

        proof

          set p = the Element of T;

          defpred P[ Real] means $1 >= (f . p);

          set R = { ( right_closed_halfline r3) where r3 be Element of REAL : P[r3] };

          

           A3: R is Subset-Family of REAL from DOMAIN_1:sch 8;

          

           A4: ( right_closed_halfline (f . p)) in R;

          then

          reconsider R as non empty Subset-Family of REAL by A3;

          reconsider F = (( " f) .: R) as Subset-Family of T;

          

           A5: F is c=-linear

          proof

            let X,Y be set;

            assume X in F;

            then

            consider A be object such that

             A6: A in ( bool REAL ) and

             A7: A in R and

             A8: X = (( " f) . A) by FUNCT_2: 64;

            reconsider A as set by TARSKI: 1;

            

             A9: X = (f " A) by A6, A8, MEASURE6:def 3;

            consider r1 be Element of REAL such that

             A10: A = ( right_closed_halfline r1) and r1 >= (f . p) by A7;

            assume Y in F;

            then

            consider B be object such that

             A11: B in ( bool REAL ) and

             A12: B in R and

             A13: Y = (( " f) . B) by FUNCT_2: 64;

            reconsider B as set by TARSKI: 1;

            

             A14: Y = (f " B) by A11, A13, MEASURE6:def 3;

            consider r2 be Element of REAL such that

             A15: B = ( right_closed_halfline r2) and r2 >= (f . p) by A12;

            r1 >= r2 or r2 >= r1;

            then X c= Y or Y c= X by A10, A15, A9, A14, RELAT_1: 143, XXREAL_1: 38;

            hence thesis by XBOOLE_0:def 9;

          end;

          assume

           A16: for s be Real holds not s is UpperBound of (f .: the carrier of T);

          now

            assume {} in F;

            then

            consider rchx be object such that

             A17: rchx in ( bool REAL ) and

             A18: rchx in R and

             A19: {} = (( " f) . rchx) by FUNCT_2: 64;

            consider r3 be Element of REAL such that

             A20: rchx = ( right_closed_halfline r3) and r3 >= (f . p) by A18;

             not r3 is UpperBound of (f .: the carrier of T) by A16;

            then

            consider r1 be ExtReal such that

             A21: r1 in (f .: the carrier of T) and

             A22: r1 > r3 by XXREAL_2:def 1;

            reconsider rchx as set by TARSKI: 1;

            rchx = { g where g be Real : g >= r3 } by A20, XXREAL_1: 232;

            then

             A23: r1 in rchx by A21, A22;

            

             A24: ex c be object st c in the carrier of T & c in the carrier of T & r1 = (f . c) by A21, FUNCT_2: 64;

             {} = (f " rchx) by A17, A19, MEASURE6:def 3;

            hence contradiction by A24, A23, FUNCT_2: 38;

          end;

          then

           A25: F is with_non-empty_elements by SETFAM_1:def 8;

          R is closed

          proof

            let X be Subset of REAL ;

            assume X in R;

            then ex r3 be Element of REAL st X = ( right_closed_halfline r3) & r3 >= (f . p);

            hence thesis;

          end;

          then

           A26: F is closed by A2, Th13;

          (( " f) . ( right_closed_halfline (f . p))) in F by A4, FUNCT_2: 35;

          then ( meet F) <> {} by A1, A25, A5, A26, COMPTS_1: 4;

          then

          consider x be object such that

           A27: x in ( meet F) by XBOOLE_0:def 1;

          set eR = the Element of R;

          eR in R;

          then

          consider er be Element of REAL such that

           A28: eR = ( right_closed_halfline er) and

           A29: er >= (f . p);

          reconsider x as Element of T by A27;

          

           A30: (f . x) in ( meet R) by A27, MEASURE6: 35;

          then

           A31: (f . x) in eR by SETFAM_1:def 1;

          consider fx9 be Real such that

           A32: fx9 > (f . x) by XREAL_1: 1;

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

          ( right_closed_halfline er) = { r3 : r3 >= er } by XXREAL_1: 232;

          then ex r1 be Real st (f . x) = r1 & r1 >= er by A31, A28;

          then (f . x) >= (f . p) by A29, XXREAL_0: 2;

          then fx9 >= (f . p) by A32, XXREAL_0: 2;

          then ( right_closed_halfline fx9) in R;

          then

           A33: (f . x) in ( right_closed_halfline fx9) by A30, SETFAM_1:def 1;

          ( right_closed_halfline fx9) = { r3 : r3 >= fx9 } by XXREAL_1: 232;

          then ex r3 st (f . x) = r3 & r3 >= fx9 by A33;

          hence contradiction by A32;

        end;

        set p = the Element of T;

        defpred P[ Real] means $1 <= (f . p);

        set R = { ( left_closed_halfline r3) where r3 be Element of REAL : P[r3] };

        

         A34: R is Subset-Family of REAL from DOMAIN_1:sch 8;

        

         A35: ( left_closed_halfline (f . p)) in R;

        then

        reconsider R as non empty Subset-Family of REAL by A34;

        reconsider F = (( " f) .: R) as Subset-Family of T;

        R is closed

        proof

          let X be Subset of REAL ;

          assume X in R;

          then ex r3 be Element of REAL st X = ( left_closed_halfline r3) & r3 <= (f . p);

          hence thesis;

        end;

        then

         A36: F is closed by A2, Th13;

        

         A37: F is c=-linear

        proof

          let X,Y be set;

          assume X in F;

          then

          consider A be object such that

           A38: A in ( bool REAL ) and

           A39: A in R and

           A40: X = (( " f) . A) by FUNCT_2: 64;

          reconsider A as set by TARSKI: 1;

          

           A41: X = (f " A) by A38, A40, MEASURE6:def 3;

          consider r1 be Element of REAL such that

           A42: A = ( left_closed_halfline r1) and r1 <= (f . p) by A39;

          assume Y in F;

          then

          consider B be object such that

           A43: B in ( bool REAL ) and

           A44: B in R and

           A45: Y = (( " f) . B) by FUNCT_2: 64;

          reconsider B as set by TARSKI: 1;

          

           A46: Y = (f " B) by A43, A45, MEASURE6:def 3;

          consider r2 be Element of REAL such that

           A47: B = ( left_closed_halfline r2) and r2 <= (f . p) by A44;

          r1 <= r2 or r2 <= r1;

          then X c= Y or Y c= X by A42, A47, A41, A46, RELAT_1: 143, XXREAL_1: 42;

          hence thesis by XBOOLE_0:def 9;

        end;

        assume

         A48: for s holds not s is LowerBound of (f .: the carrier of T);

        now

          assume {} in F;

          then

          consider rchx be object such that

           A49: rchx in ( bool REAL ) and

           A50: rchx in R and

           A51: {} = (( " f) . rchx) by FUNCT_2: 64;

          consider r3 be Element of REAL such that

           A52: rchx = ( left_closed_halfline r3) and r3 <= (f . p) by A50;

           not r3 is LowerBound of (f .: the carrier of T) by A48;

          then

          consider r1 be ExtReal such that

           A53: r1 in (f .: the carrier of T) and

           A54: r1 < r3 by XXREAL_2:def 2;

          reconsider rchx as set by TARSKI: 1;

          rchx = { g where g be Real : g <= r3 } by A52, XXREAL_1: 231;

          then

           A55: r1 in rchx by A53, A54;

          

           A56: ex c be object st c in the carrier of T & c in the carrier of T & r1 = (f . c) by A53, FUNCT_2: 64;

           {} = (f " rchx) by A49, A51, MEASURE6:def 3;

          hence contradiction by A56, A55, FUNCT_2: 38;

        end;

        then

         A57: F is with_non-empty_elements by SETFAM_1:def 8;

        (( " f) . ( left_closed_halfline (f . p))) in F by A35, FUNCT_2: 35;

        then ( meet F) <> {} by A1, A57, A37, A36, COMPTS_1: 4;

        then

        consider x be object such that

         A58: x in ( meet F) by XBOOLE_0:def 1;

        set eR = the Element of R;

        eR in R;

        then

        consider er be Element of REAL such that

         A59: eR = ( left_closed_halfline er) and

         A60: er <= (f . p);

        reconsider x as Element of T by A58;

        

         A61: (f . x) in ( meet R) by A58, MEASURE6: 35;

        then

         A62: (f . x) in eR by SETFAM_1:def 1;

        consider fx9 be Real such that

         A63: fx9 < (f . x) by XREAL_1: 2;

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

        ( left_closed_halfline er) = { r3 : r3 <= er } by XXREAL_1: 231;

        then ex r1 be Real st (f . x) = r1 & r1 <= er by A62, A59;

        then (f . x) <= (f . p) by A60, XXREAL_0: 2;

        then fx9 <= (f . p) by A63, XXREAL_0: 2;

        then ( left_closed_halfline fx9) in R;

        then

         A64: (f . x) in ( left_closed_halfline fx9) by A61, SETFAM_1:def 1;

        ( left_closed_halfline fx9) = { r3 : r3 <= fx9 } by XXREAL_1: 231;

        then ex r3 st (f . x) = r3 & r3 <= fx9 by A64;

        hence contradiction by A63;

      end;

    end

    registration

      cluster non empty compact for TopSpace;

      existence

      proof

        set T = the non empty compact TopSpace;

        take T;

        thus thesis;

      end;

    end

    registration

      let T be pseudocompact non empty TopSpace;

      cluster continuous -> bounded with_max with_min for RealMap of T;

      coherence

      proof

        let f be RealMap of T;

        assume

         A1: f is continuous;

        hence f is bounded by Def4;

        

         A2: for f be RealMap of T st f is continuous holds f is bounded by Def4;

        hence f is with_max by A1, Th15;

        for f be RealMap of T st f is continuous holds f is with_max by A2, Th15;

        hence thesis by A1, Th14;

      end;

    end

    theorem :: PSCOMP_1:16

    

     Th16: for T be non empty TopSpace, X be non empty Subset of T, Y be compact Subset of T, f be continuous RealMap of T st X c= Y holds ( lower_bound (f | Y)) <= ( lower_bound (f | X))

    proof

      let T be non empty TopSpace, X be non empty Subset of T, Y be compact Subset of T, f be continuous RealMap of T;

      

       A1: ((f | Y) .: the carrier of (T | Y)) = ((f | Y) .: Y) by PRE_TOPC: 8

      .= (f .: Y) by RELAT_1: 129;

      assume

       A2: X c= Y;

      then

      reconsider Y1 = Y as non empty compact Subset of T;

      

       A3: ((f | X) .: the carrier of (T | X)) = ((f | X) .: X) by PRE_TOPC: 8

      .= (f .: X) by RELAT_1: 129;

      ((f | Y1) .: the carrier of (T | Y1)) is bounded_below by MEASURE6:def 10;

      hence thesis by A2, A1, A3, RELAT_1: 123, SEQ_4: 47;

    end;

    theorem :: PSCOMP_1:17

    

     Th17: for T be non empty TopSpace, X be non empty Subset of T, Y be compact Subset of T, f be continuous RealMap of T st X c= Y holds ( upper_bound (f | X)) <= ( upper_bound (f | Y))

    proof

      let T be non empty TopSpace, X be non empty Subset of T, Y be compact Subset of T, f be continuous RealMap of T;

      

       A1: ((f | Y) .: the carrier of (T | Y)) = ((f | Y) .: Y) by PRE_TOPC: 8

      .= (f .: Y) by RELAT_1: 129;

      assume

       A2: X c= Y;

      then

      reconsider Y1 = Y as non empty compact Subset of T;

      

       A3: ((f | X) .: the carrier of (T | X)) = ((f | X) .: X) by PRE_TOPC: 8

      .= (f .: X) by RELAT_1: 129;

      ((f | Y1) .: the carrier of (T | Y1)) is bounded_above by MEASURE6:def 11;

      hence thesis by A2, A1, A3, RELAT_1: 123, SEQ_4: 48;

    end;

    begin

    registration

      let n be Element of NAT , X,Y be compact Subset of ( TOP-REAL n);

      cluster (X /\ Y) -> compact;

      coherence by COMPTS_1: 11;

    end

    reserve p for Point of ( TOP-REAL 2),

P for Subset of ( TOP-REAL 2),

Z for non empty Subset of ( TOP-REAL 2),

X for non empty compact Subset of ( TOP-REAL 2);

    definition

      :: PSCOMP_1:def5

      func proj1 -> RealMap of ( TOP-REAL 2) means

      : Def5: for p be Point of ( TOP-REAL 2) holds (it . p) = (p `1 );

      existence

      proof

        deffunc F( Point of ( TOP-REAL 2)) = ( In (($1 `1 ), REAL ));

        consider f be RealMap of ( TOP-REAL 2) such that

         A1: for p be Point of ( TOP-REAL 2) holds (f . p) = F(p) from FUNCT_2:sch 4;

        take f;

        let p be Point of ( TOP-REAL 2);

        (f . p) = F(p) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let it1,it2 be RealMap of ( TOP-REAL 2) such that

         A2: for p be Point of ( TOP-REAL 2) holds (it1 . p) = (p `1 ) and

         A3: for p be Point of ( TOP-REAL 2) holds (it2 . p) = (p `1 );

        now

          let p be Point of ( TOP-REAL 2);

          

          thus (it1 . p) = (p `1 ) by A2

          .= (it2 . p) by A3;

        end;

        hence it1 = it2 by FUNCT_2: 63;

      end;

      :: PSCOMP_1:def6

      func proj2 -> RealMap of ( TOP-REAL 2) means

      : Def6: for p be Point of ( TOP-REAL 2) holds (it . p) = (p `2 );

      existence

      proof

        deffunc F( Point of ( TOP-REAL 2)) = ( In (($1 `2 ), REAL ));

        consider f be RealMap of ( TOP-REAL 2) such that

         A4: for p be Point of ( TOP-REAL 2) holds (f . p) = F(p) from FUNCT_2:sch 4;

        take f;

        let p be Point of ( TOP-REAL 2);

        (f . p) = F(p) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let it1,it2 be RealMap of ( TOP-REAL 2) such that

         A5: for p be Point of ( TOP-REAL 2) holds (it1 . p) = (p `2 ) and

         A6: for p be Point of ( TOP-REAL 2) holds (it2 . p) = (p `2 );

        now

          let p be Point of ( TOP-REAL 2);

          

          thus (it1 . p) = (p `2 ) by A5

          .= (it2 . p) by A6;

        end;

        hence it1 = it2 by FUNCT_2: 63;

      end;

    end

    theorem :: PSCOMP_1:18

    

     Th18: ( proj1 " ].r, s.[) = { |[r1, r2]| : r < r1 & r1 < s }

    proof

      set Q = ( proj1 " ].r, s.[);

      set QQ = { |[r1, r2]| : r < r1 & r1 < s };

      now

        let z be object;

        hereby

          assume

           A1: z in Q;

          then

          reconsider p = z as Point of ( TOP-REAL 2);

          ( proj1 . p) in ].r, s.[ by A1, FUNCT_2: 38;

          then

           A2: ex t be Real st t = ( proj1 . p) & r < t & t < s;

          (p `1 ) = ( proj1 . p) & p = |[(p `1 ), (p `2 )]| by Def5, EUCLID: 53;

          hence z in QQ by A2;

        end;

        assume z in QQ;

        then

        consider r1,r2 be Real such that

         A3: z = |[r1, r2]| and

         A4: r < r1 & r1 < s;

        set p = |[r1, r2]|;

        

         A5: r1 in ].r, s.[ by A4;

        ( proj1 . p) = (p `1 ) by Def5

        .= r1 by EUCLID: 52;

        hence z in Q by A3, A5, FUNCT_2: 38;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: PSCOMP_1:19

    

     Th19: for r3, q3 st P = { |[r1, r2]| : r3 < r1 & r1 < q3 } holds P is open

    proof

      deffunc F( Real, Real) = |[$1, $2]|;

      let r3, q3;

      defpred P1[ Real, Real] means r3 < $1;

      defpred P2[ Real, Real] means $1 < q3;

      reconsider Q1 = { |[r1, r2]| : r3 < r1 }, Q2 = { |[r1, r2]| : r1 < q3 } as open Subset of ( TOP-REAL 2) by JORDAN1: 20, JORDAN1: 21;

      assume

       A1: P = { |[r1, r2]| : r3 < r1 & r1 < q3 };

      now

        let x be object;

        hereby

          assume x in P;

          then

          consider r1,r2 be Real such that

           A2: x = |[r1, r2]| & r3 < r1 & r1 < q3 by A1;

          x in Q1 & x in Q2 by A2;

          hence x in (Q1 /\ Q2) by XBOOLE_0:def 4;

        end;

        assume

         A3: x in (Q1 /\ Q2);

        then x in Q1 by XBOOLE_0:def 4;

        then

        consider r1,r2 be Real such that

         A4: x = |[r1, r2]| & r3 < r1;

        x in Q2 by A3, XBOOLE_0:def 4;

        then

        consider r19,r29 be Real such that

         A5: x = |[r19, r29]| & r19 < q3;

        ( |[r1, r2]| `1 ) = r1 & ( |[r19, r29]| `1 ) = r19 by EUCLID: 52;

        hence x in P by A1, A4, A5;

      end;

      then

       A6: P = (Q1 /\ Q2) by TARSKI: 2;

      thus thesis by A6, TOPS_1: 11;

    end;

    theorem :: PSCOMP_1:20

    

     Th20: ( proj2 " ].r, s.[) = { |[r1, r2]| : r < r2 & r2 < s }

    proof

      set Q = ( proj2 " ].r, s.[);

      set QQ = { |[r1, r2]| : r < r2 & r2 < s };

      now

        let z be object;

        hereby

          assume

           A1: z in Q;

          then

          reconsider p = z as Point of ( TOP-REAL 2);

          ( proj2 . p) in ].r, s.[ by A1, FUNCT_2: 38;

          then

           A2: ex t be Real st t = ( proj2 . p) & r < t & t < s;

          (p `2 ) = ( proj2 . p) & p = |[(p `1 ), (p `2 )]| by Def6, EUCLID: 53;

          hence z in QQ by A2;

        end;

        assume z in QQ;

        then

        consider r1,r2 be Real such that

         A3: z = |[r1, r2]| and

         A4: r < r2 & r2 < s;

        set p = |[r1, r2]|;

        

         A5: r2 in ].r, s.[ by A4;

        ( proj2 . p) = (p `2 ) by Def6

        .= r2 by EUCLID: 52;

        hence z in Q by A3, A5, FUNCT_2: 38;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: PSCOMP_1:21

    

     Th21: for r3, q3 st P = { |[r1, r2]| : r3 < r2 & r2 < q3 } holds P is open

    proof

      deffunc F( Real, Real) = |[$1, $2]|;

      let r3, q3;

      defpred P1[ Real, Real] means r3 < $2;

      defpred P2[ Real, Real] means $2 < q3;

      reconsider Q1 = { |[r1, r2]| : r3 < r2 }, Q2 = { |[r1, r2]| : r2 < q3 } as open Subset of ( TOP-REAL 2) by JORDAN1: 22, JORDAN1: 23;

      assume

       A1: P = { |[r1, r2]| : r3 < r2 & r2 < q3 };

      now

        let x be object;

        hereby

          assume x in P;

          then ex r1,r2 be Real st x = |[r1, r2]| & r3 < r2 & r2 < q3 by A1;

          then x in Q1 & x in Q2;

          hence x in (Q1 /\ Q2) by XBOOLE_0:def 4;

        end;

        assume

         A2: x in (Q1 /\ Q2);

        then x in Q1 by XBOOLE_0:def 4;

        then

        consider r1,r2 be Real such that

         A3: x = |[r1, r2]| & r3 < r2;

        x in Q2 by A2, XBOOLE_0:def 4;

        then

        consider r19,r29 be Real such that

         A4: x = |[r19, r29]| & r29 < q3;

        ( |[r1, r2]| `2 ) = r2 & ( |[r19, r29]| `2 ) = r29 by EUCLID: 52;

        hence x in P by A1, A3, A4;

      end;

      then

       A5: P = (Q1 /\ Q2) by TARSKI: 2;

      thus thesis by A5, TOPS_1: 11;

    end;

    registration

      cluster proj1 -> continuous;

      coherence

      proof

        now

          let Y be Subset of REAL ;

          set p1Y = ( proj1 " Y);

          assume

           A1: Y is open;

          now

            let x be set;

            hereby

              assume

               A2: x in p1Y;

              then

              reconsider p = x as Point of ( TOP-REAL 2);

              set p1 = ( proj1 . p);

              p1 in Y by A2, FUNCT_2: 38;

              then

              consider g such that

               A3: 0 < g and

               A4: ].(p1 - g), (p1 + g).[ c= Y by A1, RCOMP_1: 19;

              reconsider g as Real;

              reconsider Q = ( proj1 " ].(p1 - g), (p1 + g).[) as Subset of ( TOP-REAL 2);

              take Q;

              Q = { |[q3, p3]| : (p1 - g) < q3 & q3 < (p1 + g) } by Th18;

              hence Q is open by Th19;

              thus Q c= p1Y by A4, RELAT_1: 143;

              

               A5: p1 < (p1 + g) by A3, XREAL_1: 29;

              then (p1 - g) < p1 by XREAL_1: 19;

              then p1 in ].(p1 - g), (p1 + g).[ by A5;

              hence x in Q by FUNCT_2: 38;

            end;

            assume ex Q be Subset of ( TOP-REAL 2) st Q is open & Q c= p1Y & x in Q;

            hence x in p1Y;

          end;

          hence p1Y is open by TOPS_1: 25;

        end;

        hence thesis by Th8;

      end;

      cluster proj2 -> continuous;

      coherence

      proof

        now

          let Y be Subset of REAL ;

          set p1Y = ( proj2 " Y);

          assume

           A6: Y is open;

          now

            let x be set;

            hereby

              assume

               A7: x in p1Y;

              then

              reconsider p = x as Point of ( TOP-REAL 2);

              set p1 = ( proj2 . p);

              p1 in Y by A7, FUNCT_2: 38;

              then

              consider g such that

               A8: 0 < g and

               A9: ].(p1 - g), (p1 + g).[ c= Y by A6, RCOMP_1: 19;

              reconsider g as Real;

              reconsider Q = ( proj2 " ].(p1 - g), (p1 + g).[) as Subset of ( TOP-REAL 2);

              take Q;

              Q = { |[q3, p3]| : (p1 - g) < p3 & p3 < (p1 + g) } by Th20;

              hence Q is open by Th21;

              thus Q c= p1Y by A9, RELAT_1: 143;

              

               A10: p1 < (p1 + g) by A8, XREAL_1: 29;

              then (p1 - g) < p1 by XREAL_1: 19;

              then p1 in ].(p1 - g), (p1 + g).[ by A10;

              hence x in Q by FUNCT_2: 38;

            end;

            assume ex Q be Subset of ( TOP-REAL 2) st Q is open & Q c= p1Y & x in Q;

            hence x in p1Y;

          end;

          hence p1Y is open by TOPS_1: 25;

        end;

        hence thesis by Th8;

      end;

    end

    theorem :: PSCOMP_1:22

    

     Th22: for X be Subset of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in X holds (( proj1 | X) . p) = (p `1 )

    proof

      let X be Subset of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume p in X;

      

      hence (( proj1 | X) . p) = ( proj1 . p) by FUNCT_1: 49

      .= (p `1 ) by Def5;

    end;

    theorem :: PSCOMP_1:23

    

     Th23: for X be Subset of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in X holds (( proj2 | X) . p) = (p `2 )

    proof

      let X be Subset of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume p in X;

      

      hence (( proj2 | X) . p) = ( proj2 . p) by FUNCT_1: 49

      .= (p `2 ) by Def6;

    end;

    definition

      let X be Subset of ( TOP-REAL 2);

      :: PSCOMP_1:def7

      func W-bound X -> Real equals ( lower_bound ( proj1 | X));

      coherence ;

      :: PSCOMP_1:def8

      func N-bound X -> Real equals ( upper_bound ( proj2 | X));

      coherence ;

      :: PSCOMP_1:def9

      func E-bound X -> Real equals ( upper_bound ( proj1 | X));

      coherence ;

      :: PSCOMP_1:def10

      func S-bound X -> Real equals ( lower_bound ( proj2 | X));

      coherence ;

    end

    

     Lm3: p in X implies ( lower_bound ( proj1 | X)) <= (p `1 ) & (p `1 ) <= ( upper_bound ( proj1 | X)) & ( lower_bound ( proj2 | X)) <= (p `2 ) & (p `2 ) <= ( upper_bound ( proj2 | X))

    proof

      assume

       A1: p in X;

      then

      reconsider p9 = p as Point of (( TOP-REAL 2) | X) by PRE_TOPC: 8;

      

       A2: (( proj1 | X) . p9) = (p `1 ) by A1, Th22;

      hence ( lower_bound ( proj1 | X)) <= (p `1 ) by Th1;

      thus (p `1 ) <= ( upper_bound ( proj1 | X)) by A2, Th4;

      

       A3: (( proj2 | X) . p9) = (p `2 ) by A1, Th23;

      hence ( lower_bound ( proj2 | X)) <= (p `2 ) by Th1;

      thus thesis by A3, Th4;

    end;

    theorem :: PSCOMP_1:24

    p in X implies ( W-bound X) <= (p `1 ) & (p `1 ) <= ( E-bound X) & ( S-bound X) <= (p `2 ) & (p `2 ) <= ( N-bound X) by Lm3;

    definition

      let X be Subset of ( TOP-REAL 2);

      :: PSCOMP_1:def11

      func SW-corner X -> Point of ( TOP-REAL 2) equals |[( W-bound X), ( S-bound X)]|;

      coherence ;

      :: PSCOMP_1:def12

      func NW-corner X -> Point of ( TOP-REAL 2) equals |[( W-bound X), ( N-bound X)]|;

      coherence ;

      :: PSCOMP_1:def13

      func NE-corner X -> Point of ( TOP-REAL 2) equals |[( E-bound X), ( N-bound X)]|;

      coherence ;

      :: PSCOMP_1:def14

      func SE-corner X -> Point of ( TOP-REAL 2) equals |[( E-bound X), ( S-bound X)]|;

      coherence ;

    end

    theorem :: PSCOMP_1:25

    (( SW-corner P) `1 ) = (( NW-corner P) `1 )

    proof

      

      thus (( SW-corner P) `1 ) = ( W-bound P) by EUCLID: 52

      .= (( NW-corner P) `1 ) by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:26

    (( SE-corner P) `1 ) = (( NE-corner P) `1 )

    proof

      

      thus (( SE-corner P) `1 ) = ( E-bound P) by EUCLID: 52

      .= (( NE-corner P) `1 ) by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:27

    (( NW-corner P) `2 ) = (( NE-corner P) `2 )

    proof

      

      thus (( NW-corner P) `2 ) = ( N-bound P) by EUCLID: 52

      .= (( NE-corner P) `2 ) by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:28

    (( SW-corner P) `2 ) = (( SE-corner P) `2 )

    proof

      

      thus (( SW-corner P) `2 ) = ( S-bound P) by EUCLID: 52

      .= (( SE-corner P) `2 ) by EUCLID: 52;

    end;

    definition

      let X be Subset of ( TOP-REAL 2);

      :: PSCOMP_1:def15

      func W-most X -> Subset of ( TOP-REAL 2) equals (( LSeg (( SW-corner X),( NW-corner X))) /\ X);

      coherence ;

      :: PSCOMP_1:def16

      func N-most X -> Subset of ( TOP-REAL 2) equals (( LSeg (( NW-corner X),( NE-corner X))) /\ X);

      coherence ;

      :: PSCOMP_1:def17

      func E-most X -> Subset of ( TOP-REAL 2) equals (( LSeg (( SE-corner X),( NE-corner X))) /\ X);

      coherence ;

      :: PSCOMP_1:def18

      func S-most X -> Subset of ( TOP-REAL 2) equals (( LSeg (( SW-corner X),( SE-corner X))) /\ X);

      coherence ;

    end

    registration

      let X be non empty compact Subset of ( TOP-REAL 2);

      cluster ( W-most X) -> non empty compact;

      coherence

      proof

        set p1X = ( proj1 | X), c = the carrier of (( TOP-REAL 2) | X);

        

         A1: (( SW-corner X) `1 ) = ( W-bound X) & (( NW-corner X) `1 ) = ( W-bound X) by EUCLID: 52;

        (p1X .: c) is with_min by MEASURE6:def 13;

        then ( lower_bound (p1X .: c)) in (p1X .: c);

        then

        consider p be object such that

         A2: p in c and p in c and

         A3: ( lower_bound (p1X .: c)) = (p1X . p) by FUNCT_2: 64;

        

         A4: c = X by PRE_TOPC: 8;

        then

        reconsider p as Point of ( TOP-REAL 2) by A2;

        

         A5: (p `2 ) <= ( N-bound X) by A4, A2, Lm3;

        

         A6: (( SW-corner X) `2 ) = ( S-bound X) & (( NW-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

        (p1X . p) = (p `1 ) & ( S-bound X) <= (p `2 ) by A4, A2, Lm3, Th22;

        then p in ( LSeg (( SW-corner X),( NW-corner X))) by A1, A6, A3, A5, GOBOARD7: 7;

        hence thesis by A4, A2, XBOOLE_0:def 4;

      end;

      cluster ( N-most X) -> non empty compact;

      coherence

      proof

        set p2X = ( proj2 | X), c = the carrier of (( TOP-REAL 2) | X);

        

         A7: (( NW-corner X) `1 ) = ( W-bound X) & (( NE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

        (p2X .: c) is with_max by MEASURE6:def 12;

        then ( upper_bound (p2X .: c)) in (p2X .: c);

        then

        consider p be object such that

         A8: p in c and p in c and

         A9: ( upper_bound (p2X .: c)) = (p2X . p) by FUNCT_2: 64;

        

         A10: c = X by PRE_TOPC: 8;

        then

        reconsider p as Point of ( TOP-REAL 2) by A8;

        

         A11: (p `1 ) <= ( E-bound X) by A10, A8, Lm3;

        

         A12: (( NW-corner X) `2 ) = ( N-bound X) & (( NE-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

        (p2X . p) = (p `2 ) & ( W-bound X) <= (p `1 ) by A10, A8, Lm3, Th23;

        then p in ( LSeg (( NW-corner X),( NE-corner X))) by A7, A12, A9, A11, GOBOARD7: 8;

        hence thesis by A10, A8, XBOOLE_0:def 4;

      end;

      cluster ( E-most X) -> non empty compact;

      coherence

      proof

        set p1X = ( proj1 | X), c = the carrier of (( TOP-REAL 2) | X);

        

         A13: (( SE-corner X) `1 ) = ( E-bound X) & (( NE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

        (p1X .: c) is with_max by MEASURE6:def 12;

        then ( upper_bound (p1X .: c)) in (p1X .: c);

        then

        consider p be object such that

         A14: p in c and p in c and

         A15: ( upper_bound (p1X .: c)) = (p1X . p) by FUNCT_2: 64;

        

         A16: c = X by PRE_TOPC: 8;

        then

        reconsider p as Point of ( TOP-REAL 2) by A14;

        

         A17: (p `2 ) <= ( N-bound X) by A16, A14, Lm3;

        

         A18: (( SE-corner X) `2 ) = ( S-bound X) & (( NE-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

        (p1X . p) = (p `1 ) & ( S-bound X) <= (p `2 ) by A16, A14, Lm3, Th22;

        then p in ( LSeg (( SE-corner X),( NE-corner X))) by A13, A18, A15, A17, GOBOARD7: 7;

        hence thesis by A16, A14, XBOOLE_0:def 4;

      end;

      cluster ( S-most X) -> non empty compact;

      coherence

      proof

        set p2X = ( proj2 | X), c = the carrier of (( TOP-REAL 2) | X);

        

         A19: (( SW-corner X) `1 ) = ( W-bound X) & (( SE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

        (p2X .: c) is with_min by MEASURE6:def 13;

        then ( lower_bound (p2X .: c)) in (p2X .: c);

        then

        consider p be object such that

         A20: p in c and p in c and

         A21: ( lower_bound (p2X .: c)) = (p2X . p) by FUNCT_2: 64;

        

         A22: c = X by PRE_TOPC: 8;

        then

        reconsider p as Point of ( TOP-REAL 2) by A20;

        

         A23: (p `1 ) <= ( E-bound X) by A22, A20, Lm3;

        

         A24: (( SW-corner X) `2 ) = ( S-bound X) & (( SE-corner X) `2 ) = ( S-bound X) by EUCLID: 52;

        (p2X . p) = (p `2 ) & ( W-bound X) <= (p `1 ) by A22, A20, Lm3, Th23;

        then p in ( LSeg (( SW-corner X),( SE-corner X))) by A19, A24, A21, A23, GOBOARD7: 8;

        hence thesis by A22, A20, XBOOLE_0:def 4;

      end;

    end

    definition

      let X be Subset of ( TOP-REAL 2);

      :: PSCOMP_1:def19

      func W-min X -> Point of ( TOP-REAL 2) equals |[( W-bound X), ( lower_bound ( proj2 | ( W-most X)))]|;

      coherence ;

      :: PSCOMP_1:def20

      func W-max X -> Point of ( TOP-REAL 2) equals |[( W-bound X), ( upper_bound ( proj2 | ( W-most X)))]|;

      coherence ;

      :: PSCOMP_1:def21

      func N-min X -> Point of ( TOP-REAL 2) equals |[( lower_bound ( proj1 | ( N-most X))), ( N-bound X)]|;

      coherence ;

      :: PSCOMP_1:def22

      func N-max X -> Point of ( TOP-REAL 2) equals |[( upper_bound ( proj1 | ( N-most X))), ( N-bound X)]|;

      coherence ;

      :: PSCOMP_1:def23

      func E-max X -> Point of ( TOP-REAL 2) equals |[( E-bound X), ( upper_bound ( proj2 | ( E-most X)))]|;

      coherence ;

      :: PSCOMP_1:def24

      func E-min X -> Point of ( TOP-REAL 2) equals |[( E-bound X), ( lower_bound ( proj2 | ( E-most X)))]|;

      coherence ;

      :: PSCOMP_1:def25

      func S-max X -> Point of ( TOP-REAL 2) equals |[( upper_bound ( proj1 | ( S-most X))), ( S-bound X)]|;

      coherence ;

      :: PSCOMP_1:def26

      func S-min X -> Point of ( TOP-REAL 2) equals |[( lower_bound ( proj1 | ( S-most X))), ( S-bound X)]|;

      coherence ;

    end

    theorem :: PSCOMP_1:29

    

     Th29: (( SW-corner P) `1 ) = (( W-min P) `1 ) & (( SW-corner P) `1 ) = (( W-max P) `1 ) & (( W-min P) `1 ) = (( W-max P) `1 ) & (( W-min P) `1 ) = (( NW-corner P) `1 ) & (( W-max P) `1 ) = (( NW-corner P) `1 )

    proof

      (( W-min P) `1 ) = ( W-bound P) & (( W-max P) `1 ) = ( W-bound P) by EUCLID: 52;

      hence thesis by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:30

    

     Th30: (( SW-corner X) `2 ) <= (( W-min X) `2 ) & (( SW-corner X) `2 ) <= (( W-max X) `2 ) & (( SW-corner X) `2 ) <= (( NW-corner X) `2 ) & (( W-min X) `2 ) <= (( W-max X) `2 ) & (( W-min X) `2 ) <= (( NW-corner X) `2 ) & (( W-max X) `2 ) <= (( NW-corner X) `2 )

    proof

      set LX = ( W-most X);

      

       A1: (( W-min X) `2 ) = ( lower_bound ( proj2 | LX)) by EUCLID: 52;

      

       A2: (( SW-corner X) `2 ) = ( lower_bound ( proj2 | X)) by EUCLID: 52;

      hence (( SW-corner X) `2 ) <= (( W-min X) `2 ) by A1, Th16, XBOOLE_1: 17;

      

       A3: (( W-max X) `2 ) = ( upper_bound ( proj2 | LX)) by EUCLID: 52;

      then

       A4: (( W-min X) `2 ) <= (( W-max X) `2 ) by A1, Th7;

      (( SW-corner X) `2 ) <= (( W-min X) `2 ) by A2, A1, Th16, XBOOLE_1: 17;

      hence

       A5: (( SW-corner X) `2 ) <= (( W-max X) `2 ) by A4, XXREAL_0: 2;

      

       A6: (( NW-corner X) `2 ) = ( upper_bound ( proj2 | X)) by EUCLID: 52;

      then

       A7: (( W-max X) `2 ) <= (( NW-corner X) `2 ) by A3, Th17, XBOOLE_1: 17;

      hence (( SW-corner X) `2 ) <= (( NW-corner X) `2 ) by A5, XXREAL_0: 2;

      thus (( W-min X) `2 ) <= (( W-max X) `2 ) by A1, A3, Th7;

      thus (( W-min X) `2 ) <= (( NW-corner X) `2 ) by A4, A7, XXREAL_0: 2;

      thus thesis by A3, A6, Th17, XBOOLE_1: 17;

    end;

    theorem :: PSCOMP_1:31

    

     Th31: p in ( W-most Z) implies (p `1 ) = (( W-min Z) `1 ) & (Z is compact implies (( W-min Z) `2 ) <= (p `2 ) & (p `2 ) <= (( W-max Z) `2 ))

    proof

      

       A1: (( SW-corner Z) `1 ) = ( W-bound Z) & (( W-min Z) `1 ) = ( W-bound Z) by EUCLID: 52;

      

       A2: (( NW-corner Z) `1 ) = ( W-bound Z) by EUCLID: 52;

      assume

       A3: p in ( W-most Z);

      then p in ( LSeg (( SW-corner Z),( NW-corner Z))) by XBOOLE_0:def 4;

      hence (p `1 ) = (( W-min Z) `1 ) by A1, A2, GOBOARD7: 5;

      assume Z is compact;

      then

      reconsider Z as non empty compact Subset of ( TOP-REAL 2);

      (( W-min Z) `2 ) = ( lower_bound ( proj2 | ( W-most Z))) & (( W-max Z) `2 ) = ( upper_bound ( proj2 | ( W-most Z))) by EUCLID: 52;

      hence thesis by A3, Lm3;

    end;

    theorem :: PSCOMP_1:32

    

     Th32: ( W-most X) c= ( LSeg (( W-min X),( W-max X)))

    proof

      let x be object;

      assume

       A1: x in ( W-most X);

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A2: (p `2 ) <= (( W-max X) `2 ) by A1, Th31;

      

       A3: (( W-min X) `1 ) = (( W-max X) `1 ) by Th29;

      (p `1 ) = (( W-min X) `1 ) & (( W-min X) `2 ) <= (p `2 ) by A1, Th31;

      hence thesis by A3, A2, GOBOARD7: 7;

    end;

    theorem :: PSCOMP_1:33

    ( LSeg (( W-min X),( W-max X))) c= ( LSeg (( SW-corner X),( NW-corner X)))

    proof

      

       A1: (( SW-corner X) `1 ) = ( W-bound X) & (( NW-corner X) `1 ) = ( W-bound X) by EUCLID: 52;

      

       A2: (( W-max X) `2 ) <= (( NW-corner X) `2 ) by Th30;

      (( W-max X) `1 ) = ( W-bound X) & (( SW-corner X) `2 ) <= (( W-max X) `2 ) by Th30, EUCLID: 52;

      then

       A3: ( W-max X) in ( LSeg (( SW-corner X),( NW-corner X))) by A1, A2, GOBOARD7: 7;

      

       A4: (( W-min X) `2 ) <= (( NW-corner X) `2 ) by Th30;

      (( W-min X) `1 ) = ( W-bound X) & (( SW-corner X) `2 ) <= (( W-min X) `2 ) by Th30, EUCLID: 52;

      then ( W-min X) in ( LSeg (( SW-corner X),( NW-corner X))) by A1, A4, GOBOARD7: 7;

      hence thesis by A3, TOPREAL1: 6;

    end;

    theorem :: PSCOMP_1:34

    

     Th34: ( W-min X) in ( W-most X) & ( W-max X) in ( W-most X)

    proof

      set p2W = ( proj2 | ( W-most X)), c = the carrier of (( TOP-REAL 2) | ( W-most X));

      

       A1: (( SW-corner X) `1 ) = ( W-bound X) & (( NW-corner X) `1 ) = ( W-bound X) by EUCLID: 52;

      (p2W .: c) is with_min by MEASURE6:def 13;

      then ( lower_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A2: p in c and p in c and

       A3: ( lower_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      

       A4: c = ( W-most X) by PRE_TOPC: 8;

      then

      reconsider p as Point of ( TOP-REAL 2) by A2;

      p in ( LSeg (( SW-corner X),( NW-corner X))) by A4, A2, XBOOLE_0:def 4;

      then

       A5: (p `1 ) = ( W-bound X) by A1, GOBOARD7: 5;

      

       A6: (( SW-corner X) `1 ) = ( W-bound X) & (( NW-corner X) `1 ) = ( W-bound X) by EUCLID: 52;

      (p2W . p) = (p `2 ) by A4, A2, Th23;

      hence ( W-min X) in ( W-most X) by A4, A2, A3, A5, EUCLID: 53;

      (p2W .: c) is with_max by MEASURE6:def 12;

      then ( upper_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A7: p in c and p in c and

       A8: ( upper_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      reconsider p as Point of ( TOP-REAL 2) by A4, A7;

      p in ( LSeg (( SW-corner X),( NW-corner X))) by A4, A7, XBOOLE_0:def 4;

      then

       A9: (p `1 ) = ( W-bound X) by A6, GOBOARD7: 5;

      (p2W . p) = (p `2 ) by A4, A7, Th23;

      hence thesis by A4, A7, A8, A9, EUCLID: 53;

    end;

    theorem :: PSCOMP_1:35

    (( LSeg (( SW-corner X),( W-min X))) /\ X) = {( W-min X)} & (( LSeg (( W-max X),( NW-corner X))) /\ X) = {( W-max X)}

    proof

      now

        let x be object;

        

         A1: ( W-min X) in ( LSeg (( SW-corner X),( W-min X))) by RLTOPSP1: 68;

        hereby

          ( W-min X) in ( W-most X) by Th34;

          then ( SW-corner X) in ( LSeg (( SW-corner X),( NW-corner X))) & ( W-min X) in ( LSeg (( SW-corner X),( NW-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A2: ( LSeg (( SW-corner X),( W-min X))) c= ( LSeg (( SW-corner X),( NW-corner X))) by TOPREAL1: 6;

          assume

           A3: x in (( LSeg (( SW-corner X),( W-min X))) /\ X);

          then

           A4: x in ( LSeg (( SW-corner X),( W-min X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A3;

          x in X by A3, XBOOLE_0:def 4;

          then p in ( W-most X) by A4, A2, XBOOLE_0:def 4;

          then

           A5: (( W-min X) `2 ) <= (p `2 ) by Th31;

          (( SW-corner X) `2 ) <= (( W-min X) `2 ) by Th30;

          then (p `2 ) <= (( W-min X) `2 ) by A4, TOPREAL1: 4;

          then

           A6: (p `2 ) = (( W-min X) `2 ) by A5, XXREAL_0: 1;

          (( SW-corner X) `1 ) = (( W-min X) `1 ) by Th29;

          then

           A7: (p `1 ) = (( W-min X) `1 ) by A4, GOBOARD7: 5;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( W-min X) by A7, A6, EUCLID: 53;

        end;

        ( W-min X) in ( W-most X) by Th34;

        then

         A8: ( W-min X) in X by XBOOLE_0:def 4;

        assume x = ( W-min X);

        hence x in (( LSeg (( SW-corner X),( W-min X))) /\ X) by A8, A1, XBOOLE_0:def 4;

      end;

      hence (( LSeg (( SW-corner X),( W-min X))) /\ X) = {( W-min X)} by TARSKI:def 1;

      now

        let x be object;

        

         A9: ( W-max X) in ( LSeg (( W-max X),( NW-corner X))) by RLTOPSP1: 68;

        hereby

          ( W-max X) in ( W-most X) by Th34;

          then ( NW-corner X) in ( LSeg (( SW-corner X),( NW-corner X))) & ( W-max X) in ( LSeg (( SW-corner X),( NW-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A10: ( LSeg (( W-max X),( NW-corner X))) c= ( LSeg (( SW-corner X),( NW-corner X))) by TOPREAL1: 6;

          assume

           A11: x in (( LSeg (( W-max X),( NW-corner X))) /\ X);

          then

           A12: x in ( LSeg (( W-max X),( NW-corner X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A11;

          x in X by A11, XBOOLE_0:def 4;

          then p in ( W-most X) by A12, A10, XBOOLE_0:def 4;

          then

           A13: (p `2 ) <= (( W-max X) `2 ) by Th31;

          (( W-max X) `2 ) <= (( NW-corner X) `2 ) by Th30;

          then (( W-max X) `2 ) <= (p `2 ) by A12, TOPREAL1: 4;

          then

           A14: (p `2 ) = (( W-max X) `2 ) by A13, XXREAL_0: 1;

          (( NW-corner X) `1 ) = (( W-max X) `1 ) by Th29;

          then

           A15: (p `1 ) = (( W-max X) `1 ) by A12, GOBOARD7: 5;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( W-max X) by A15, A14, EUCLID: 53;

        end;

        ( W-max X) in ( W-most X) by Th34;

        then

         A16: ( W-max X) in X by XBOOLE_0:def 4;

        assume x = ( W-max X);

        hence x in (( LSeg (( W-max X),( NW-corner X))) /\ X) by A16, A9, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PSCOMP_1:36

    ( W-min X) = ( W-max X) implies ( W-most X) = {( W-min X)}

    proof

      assume ( W-min X) = ( W-max X);

      then ( W-most X) c= ( LSeg (( W-min X),( W-min X))) by Th32;

      then ( W-most X) c= {( W-min X)} by RLTOPSP1: 70;

      hence thesis by ZFMISC_1: 33;

    end;

    theorem :: PSCOMP_1:37

    

     Th37: (( NW-corner P) `2 ) = (( N-min P) `2 ) & (( NW-corner P) `2 ) = (( N-max P) `2 ) & (( N-min P) `2 ) = (( N-max P) `2 ) & (( N-min P) `2 ) = (( NE-corner P) `2 ) & (( N-max P) `2 ) = (( NE-corner P) `2 )

    proof

      (( N-min P) `2 ) = ( N-bound P) & (( N-max P) `2 ) = ( N-bound P) by EUCLID: 52;

      hence thesis by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:38

    

     Th38: (( NW-corner X) `1 ) <= (( N-min X) `1 ) & (( NW-corner X) `1 ) <= (( N-max X) `1 ) & (( NW-corner X) `1 ) <= (( NE-corner X) `1 ) & (( N-min X) `1 ) <= (( N-max X) `1 ) & (( N-min X) `1 ) <= (( NE-corner X) `1 ) & (( N-max X) `1 ) <= (( NE-corner X) `1 )

    proof

      set LX = ( N-most X);

      

       A1: (( N-min X) `1 ) = ( lower_bound ( proj1 | LX)) by EUCLID: 52;

      

       A2: (( NW-corner X) `1 ) = ( lower_bound ( proj1 | X)) by EUCLID: 52;

      hence (( NW-corner X) `1 ) <= (( N-min X) `1 ) by A1, Th16, XBOOLE_1: 17;

      

       A3: (( N-max X) `1 ) = ( upper_bound ( proj1 | LX)) by EUCLID: 52;

      then

       A4: (( N-min X) `1 ) <= (( N-max X) `1 ) by A1, Th7;

      (( NW-corner X) `1 ) <= (( N-min X) `1 ) by A2, A1, Th16, XBOOLE_1: 17;

      hence

       A5: (( NW-corner X) `1 ) <= (( N-max X) `1 ) by A4, XXREAL_0: 2;

      

       A6: (( NE-corner X) `1 ) = ( upper_bound ( proj1 | X)) by EUCLID: 52;

      then

       A7: (( N-max X) `1 ) <= (( NE-corner X) `1 ) by A3, Th17, XBOOLE_1: 17;

      hence (( NW-corner X) `1 ) <= (( NE-corner X) `1 ) by A5, XXREAL_0: 2;

      thus (( N-min X) `1 ) <= (( N-max X) `1 ) by A1, A3, Th7;

      thus (( N-min X) `1 ) <= (( NE-corner X) `1 ) by A4, A7, XXREAL_0: 2;

      thus thesis by A3, A6, Th17, XBOOLE_1: 17;

    end;

    theorem :: PSCOMP_1:39

    

     Th39: p in ( N-most Z) implies (p `2 ) = (( N-min Z) `2 ) & (Z is compact implies (( N-min Z) `1 ) <= (p `1 ) & (p `1 ) <= (( N-max Z) `1 ))

    proof

      

       A1: (( NW-corner Z) `2 ) = ( N-bound Z) & (( N-min Z) `2 ) = ( N-bound Z) by EUCLID: 52;

      

       A2: (( NE-corner Z) `2 ) = ( N-bound Z) by EUCLID: 52;

      assume

       A3: p in ( N-most Z);

      then p in ( LSeg (( NW-corner Z),( NE-corner Z))) by XBOOLE_0:def 4;

      hence (p `2 ) = (( N-min Z) `2 ) by A1, A2, GOBOARD7: 6;

      assume Z is compact;

      then

      reconsider Z as non empty compact Subset of ( TOP-REAL 2);

      (( N-min Z) `1 ) = ( lower_bound ( proj1 | ( N-most Z))) & (( N-max Z) `1 ) = ( upper_bound ( proj1 | ( N-most Z))) by EUCLID: 52;

      hence thesis by A3, Lm3;

    end;

    theorem :: PSCOMP_1:40

    

     Th40: ( N-most X) c= ( LSeg (( N-min X),( N-max X)))

    proof

      let x be object;

      assume

       A1: x in ( N-most X);

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A2: (p `1 ) <= (( N-max X) `1 ) by A1, Th39;

      

       A3: (( N-min X) `2 ) = (( N-max X) `2 ) by Th37;

      (p `2 ) = (( N-min X) `2 ) & (( N-min X) `1 ) <= (p `1 ) by A1, Th39;

      hence thesis by A3, A2, GOBOARD7: 8;

    end;

    theorem :: PSCOMP_1:41

    ( LSeg (( N-min X),( N-max X))) c= ( LSeg (( NW-corner X),( NE-corner X)))

    proof

      

       A1: (( NW-corner X) `2 ) = ( N-bound X) & (( NE-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

      

       A2: (( N-max X) `1 ) <= (( NE-corner X) `1 ) by Th38;

      (( N-max X) `2 ) = ( N-bound X) & (( NW-corner X) `1 ) <= (( N-max X) `1 ) by Th38, EUCLID: 52;

      then

       A3: ( N-max X) in ( LSeg (( NW-corner X),( NE-corner X))) by A1, A2, GOBOARD7: 8;

      

       A4: (( N-min X) `1 ) <= (( NE-corner X) `1 ) by Th38;

      (( N-min X) `2 ) = ( N-bound X) & (( NW-corner X) `1 ) <= (( N-min X) `1 ) by Th38, EUCLID: 52;

      then ( N-min X) in ( LSeg (( NW-corner X),( NE-corner X))) by A1, A4, GOBOARD7: 8;

      hence thesis by A3, TOPREAL1: 6;

    end;

    theorem :: PSCOMP_1:42

    

     Th42: ( N-min X) in ( N-most X) & ( N-max X) in ( N-most X)

    proof

      set p2W = ( proj1 | ( N-most X)), c = the carrier of (( TOP-REAL 2) | ( N-most X));

      

       A1: (( NW-corner X) `2 ) = ( N-bound X) & (( NE-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

      (p2W .: c) is with_min by MEASURE6:def 13;

      then ( lower_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A2: p in c and p in c and

       A3: ( lower_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      

       A4: c = ( N-most X) by PRE_TOPC: 8;

      then

      reconsider p as Point of ( TOP-REAL 2) by A2;

      p in ( LSeg (( NW-corner X),( NE-corner X))) by A4, A2, XBOOLE_0:def 4;

      then

       A5: (p `2 ) = ( N-bound X) by A1, GOBOARD7: 6;

      

       A6: (( NW-corner X) `2 ) = ( N-bound X) & (( NE-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

      (p2W . p) = (p `1 ) by A4, A2, Th22;

      hence ( N-min X) in ( N-most X) by A4, A2, A3, A5, EUCLID: 53;

      (p2W .: c) is with_max by MEASURE6:def 12;

      then ( upper_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A7: p in c and p in c and

       A8: ( upper_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      reconsider p as Point of ( TOP-REAL 2) by A4, A7;

      p in ( LSeg (( NW-corner X),( NE-corner X))) by A4, A7, XBOOLE_0:def 4;

      then

       A9: (p `2 ) = ( N-bound X) by A6, GOBOARD7: 6;

      (p2W . p) = (p `1 ) by A4, A7, Th22;

      hence thesis by A4, A7, A8, A9, EUCLID: 53;

    end;

    theorem :: PSCOMP_1:43

    (( LSeg (( NW-corner X),( N-min X))) /\ X) = {( N-min X)} & (( LSeg (( N-max X),( NE-corner X))) /\ X) = {( N-max X)}

    proof

      now

        let x be object;

        

         A1: ( N-min X) in ( LSeg (( NW-corner X),( N-min X))) by RLTOPSP1: 68;

        hereby

          ( N-min X) in ( N-most X) by Th42;

          then ( NW-corner X) in ( LSeg (( NW-corner X),( NE-corner X))) & ( N-min X) in ( LSeg (( NW-corner X),( NE-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A2: ( LSeg (( NW-corner X),( N-min X))) c= ( LSeg (( NW-corner X),( NE-corner X))) by TOPREAL1: 6;

          assume

           A3: x in (( LSeg (( NW-corner X),( N-min X))) /\ X);

          then

           A4: x in ( LSeg (( NW-corner X),( N-min X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A3;

          x in X by A3, XBOOLE_0:def 4;

          then p in ( N-most X) by A4, A2, XBOOLE_0:def 4;

          then

           A5: (( N-min X) `1 ) <= (p `1 ) by Th39;

          (( NW-corner X) `1 ) <= (( N-min X) `1 ) by Th38;

          then (p `1 ) <= (( N-min X) `1 ) by A4, TOPREAL1: 3;

          then

           A6: (p `1 ) = (( N-min X) `1 ) by A5, XXREAL_0: 1;

          (( NW-corner X) `2 ) = (( N-min X) `2 ) by Th37;

          then

           A7: (p `2 ) = (( N-min X) `2 ) by A4, GOBOARD7: 6;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( N-min X) by A7, A6, EUCLID: 53;

        end;

        ( N-min X) in ( N-most X) by Th42;

        then

         A8: ( N-min X) in X by XBOOLE_0:def 4;

        assume x = ( N-min X);

        hence x in (( LSeg (( NW-corner X),( N-min X))) /\ X) by A8, A1, XBOOLE_0:def 4;

      end;

      hence (( LSeg (( NW-corner X),( N-min X))) /\ X) = {( N-min X)} by TARSKI:def 1;

      now

        let x be object;

        

         A9: ( N-max X) in ( LSeg (( N-max X),( NE-corner X))) by RLTOPSP1: 68;

        hereby

          ( N-max X) in ( N-most X) by Th42;

          then ( NE-corner X) in ( LSeg (( NW-corner X),( NE-corner X))) & ( N-max X) in ( LSeg (( NW-corner X),( NE-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A10: ( LSeg (( N-max X),( NE-corner X))) c= ( LSeg (( NW-corner X),( NE-corner X))) by TOPREAL1: 6;

          assume

           A11: x in (( LSeg (( N-max X),( NE-corner X))) /\ X);

          then

           A12: x in ( LSeg (( N-max X),( NE-corner X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A11;

          x in X by A11, XBOOLE_0:def 4;

          then p in ( N-most X) by A12, A10, XBOOLE_0:def 4;

          then

           A13: (p `1 ) <= (( N-max X) `1 ) by Th39;

          (( N-max X) `1 ) <= (( NE-corner X) `1 ) by Th38;

          then (( N-max X) `1 ) <= (p `1 ) by A12, TOPREAL1: 3;

          then

           A14: (p `1 ) = (( N-max X) `1 ) by A13, XXREAL_0: 1;

          (( NE-corner X) `2 ) = (( N-max X) `2 ) by Th37;

          then

           A15: (p `2 ) = (( N-max X) `2 ) by A12, GOBOARD7: 6;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( N-max X) by A15, A14, EUCLID: 53;

        end;

        ( N-max X) in ( N-most X) by Th42;

        then

         A16: ( N-max X) in X by XBOOLE_0:def 4;

        assume x = ( N-max X);

        hence x in (( LSeg (( N-max X),( NE-corner X))) /\ X) by A16, A9, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PSCOMP_1:44

    ( N-min X) = ( N-max X) implies ( N-most X) = {( N-min X)}

    proof

      assume ( N-min X) = ( N-max X);

      then ( N-most X) c= ( LSeg (( N-min X),( N-min X))) by Th40;

      then ( N-most X) c= {( N-min X)} by RLTOPSP1: 70;

      hence thesis by ZFMISC_1: 33;

    end;

    theorem :: PSCOMP_1:45

    

     Th45: (( SE-corner P) `1 ) = (( E-min P) `1 ) & (( SE-corner P) `1 ) = (( E-max P) `1 ) & (( E-min P) `1 ) = (( E-max P) `1 ) & (( E-min P) `1 ) = (( NE-corner P) `1 ) & (( E-max P) `1 ) = (( NE-corner P) `1 )

    proof

      (( E-min P) `1 ) = ( E-bound P) & (( E-max P) `1 ) = ( E-bound P) by EUCLID: 52;

      hence thesis by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:46

    

     Th46: (( SE-corner X) `2 ) <= (( E-min X) `2 ) & (( SE-corner X) `2 ) <= (( E-max X) `2 ) & (( SE-corner X) `2 ) <= (( NE-corner X) `2 ) & (( E-min X) `2 ) <= (( E-max X) `2 ) & (( E-min X) `2 ) <= (( NE-corner X) `2 ) & (( E-max X) `2 ) <= (( NE-corner X) `2 )

    proof

      set LX = ( E-most X);

      

       A1: (( E-min X) `2 ) = ( lower_bound ( proj2 | LX)) by EUCLID: 52;

      

       A2: (( SE-corner X) `2 ) = ( lower_bound ( proj2 | X)) by EUCLID: 52;

      hence (( SE-corner X) `2 ) <= (( E-min X) `2 ) by A1, Th16, XBOOLE_1: 17;

      

       A3: (( E-max X) `2 ) = ( upper_bound ( proj2 | LX)) by EUCLID: 52;

      then

       A4: (( E-min X) `2 ) <= (( E-max X) `2 ) by A1, Th7;

      (( SE-corner X) `2 ) <= (( E-min X) `2 ) by A2, A1, Th16, XBOOLE_1: 17;

      hence

       A5: (( SE-corner X) `2 ) <= (( E-max X) `2 ) by A4, XXREAL_0: 2;

      

       A6: (( NE-corner X) `2 ) = ( upper_bound ( proj2 | X)) by EUCLID: 52;

      then

       A7: (( E-max X) `2 ) <= (( NE-corner X) `2 ) by A3, Th17, XBOOLE_1: 17;

      hence (( SE-corner X) `2 ) <= (( NE-corner X) `2 ) by A5, XXREAL_0: 2;

      thus (( E-min X) `2 ) <= (( E-max X) `2 ) by A1, A3, Th7;

      thus (( E-min X) `2 ) <= (( NE-corner X) `2 ) by A4, A7, XXREAL_0: 2;

      thus thesis by A3, A6, Th17, XBOOLE_1: 17;

    end;

    theorem :: PSCOMP_1:47

    

     Th47: p in ( E-most Z) implies (p `1 ) = (( E-min Z) `1 ) & (Z is compact implies (( E-min Z) `2 ) <= (p `2 ) & (p `2 ) <= (( E-max Z) `2 ))

    proof

      

       A1: (( SE-corner Z) `1 ) = ( E-bound Z) & (( E-min Z) `1 ) = ( E-bound Z) by EUCLID: 52;

      

       A2: (( NE-corner Z) `1 ) = ( E-bound Z) by EUCLID: 52;

      assume

       A3: p in ( E-most Z);

      then p in ( LSeg (( SE-corner Z),( NE-corner Z))) by XBOOLE_0:def 4;

      hence (p `1 ) = (( E-min Z) `1 ) by A1, A2, GOBOARD7: 5;

      assume Z is compact;

      then

      reconsider Z as non empty compact Subset of ( TOP-REAL 2);

      (( E-min Z) `2 ) = ( lower_bound ( proj2 | ( E-most Z))) & (( E-max Z) `2 ) = ( upper_bound ( proj2 | ( E-most Z))) by EUCLID: 52;

      hence thesis by A3, Lm3;

    end;

    theorem :: PSCOMP_1:48

    

     Th48: ( E-most X) c= ( LSeg (( E-min X),( E-max X)))

    proof

      let x be object;

      assume

       A1: x in ( E-most X);

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A2: (p `2 ) <= (( E-max X) `2 ) by A1, Th47;

      

       A3: (( E-min X) `1 ) = (( E-max X) `1 ) by Th45;

      (p `1 ) = (( E-min X) `1 ) & (( E-min X) `2 ) <= (p `2 ) by A1, Th47;

      hence thesis by A3, A2, GOBOARD7: 7;

    end;

    theorem :: PSCOMP_1:49

    ( LSeg (( E-min X),( E-max X))) c= ( LSeg (( SE-corner X),( NE-corner X)))

    proof

      

       A1: (( SE-corner X) `1 ) = ( E-bound X) & (( NE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

      

       A2: (( E-max X) `2 ) <= (( NE-corner X) `2 ) by Th46;

      (( E-max X) `1 ) = ( E-bound X) & (( SE-corner X) `2 ) <= (( E-max X) `2 ) by Th46, EUCLID: 52;

      then

       A3: ( E-max X) in ( LSeg (( SE-corner X),( NE-corner X))) by A1, A2, GOBOARD7: 7;

      

       A4: (( E-min X) `2 ) <= (( NE-corner X) `2 ) by Th46;

      (( E-min X) `1 ) = ( E-bound X) & (( SE-corner X) `2 ) <= (( E-min X) `2 ) by Th46, EUCLID: 52;

      then ( E-min X) in ( LSeg (( SE-corner X),( NE-corner X))) by A1, A4, GOBOARD7: 7;

      hence thesis by A3, TOPREAL1: 6;

    end;

    theorem :: PSCOMP_1:50

    

     Th50: ( E-min X) in ( E-most X) & ( E-max X) in ( E-most X)

    proof

      set p2W = ( proj2 | ( E-most X)), c = the carrier of (( TOP-REAL 2) | ( E-most X));

      

       A1: (( SE-corner X) `1 ) = ( E-bound X) & (( NE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

      (p2W .: c) is with_min by MEASURE6:def 13;

      then ( lower_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A2: p in c and p in c and

       A3: ( lower_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      

       A4: c = ( E-most X) by PRE_TOPC: 8;

      then

      reconsider p as Point of ( TOP-REAL 2) by A2;

      p in ( LSeg (( SE-corner X),( NE-corner X))) by A4, A2, XBOOLE_0:def 4;

      then

       A5: (p `1 ) = ( E-bound X) by A1, GOBOARD7: 5;

      

       A6: (( SE-corner X) `1 ) = ( E-bound X) & (( NE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

      (p2W . p) = (p `2 ) by A4, A2, Th23;

      hence ( E-min X) in ( E-most X) by A4, A2, A3, A5, EUCLID: 53;

      (p2W .: c) is with_max by MEASURE6:def 12;

      then ( upper_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A7: p in c and p in c and

       A8: ( upper_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      reconsider p as Point of ( TOP-REAL 2) by A4, A7;

      p in ( LSeg (( SE-corner X),( NE-corner X))) by A4, A7, XBOOLE_0:def 4;

      then

       A9: (p `1 ) = ( E-bound X) by A6, GOBOARD7: 5;

      (p2W . p) = (p `2 ) by A4, A7, Th23;

      hence thesis by A4, A7, A8, A9, EUCLID: 53;

    end;

    theorem :: PSCOMP_1:51

    (( LSeg (( SE-corner X),( E-min X))) /\ X) = {( E-min X)} & (( LSeg (( E-max X),( NE-corner X))) /\ X) = {( E-max X)}

    proof

      now

        let x be object;

        

         A1: ( E-min X) in ( LSeg (( SE-corner X),( E-min X))) by RLTOPSP1: 68;

        hereby

          ( E-min X) in ( E-most X) by Th50;

          then ( SE-corner X) in ( LSeg (( SE-corner X),( NE-corner X))) & ( E-min X) in ( LSeg (( SE-corner X),( NE-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A2: ( LSeg (( SE-corner X),( E-min X))) c= ( LSeg (( SE-corner X),( NE-corner X))) by TOPREAL1: 6;

          assume

           A3: x in (( LSeg (( SE-corner X),( E-min X))) /\ X);

          then

           A4: x in ( LSeg (( SE-corner X),( E-min X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A3;

          x in X by A3, XBOOLE_0:def 4;

          then p in ( E-most X) by A4, A2, XBOOLE_0:def 4;

          then

           A5: (( E-min X) `2 ) <= (p `2 ) by Th47;

          (( SE-corner X) `2 ) <= (( E-min X) `2 ) by Th46;

          then (p `2 ) <= (( E-min X) `2 ) by A4, TOPREAL1: 4;

          then

           A6: (p `2 ) = (( E-min X) `2 ) by A5, XXREAL_0: 1;

          (( SE-corner X) `1 ) = (( E-min X) `1 ) by Th45;

          then

           A7: (p `1 ) = (( E-min X) `1 ) by A4, GOBOARD7: 5;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( E-min X) by A7, A6, EUCLID: 53;

        end;

        ( E-min X) in ( E-most X) by Th50;

        then

         A8: ( E-min X) in X by XBOOLE_0:def 4;

        assume x = ( E-min X);

        hence x in (( LSeg (( SE-corner X),( E-min X))) /\ X) by A8, A1, XBOOLE_0:def 4;

      end;

      hence (( LSeg (( SE-corner X),( E-min X))) /\ X) = {( E-min X)} by TARSKI:def 1;

      now

        let x be object;

        

         A9: ( E-max X) in ( LSeg (( E-max X),( NE-corner X))) by RLTOPSP1: 68;

        hereby

          ( E-max X) in ( E-most X) by Th50;

          then ( NE-corner X) in ( LSeg (( SE-corner X),( NE-corner X))) & ( E-max X) in ( LSeg (( SE-corner X),( NE-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A10: ( LSeg (( E-max X),( NE-corner X))) c= ( LSeg (( SE-corner X),( NE-corner X))) by TOPREAL1: 6;

          assume

           A11: x in (( LSeg (( E-max X),( NE-corner X))) /\ X);

          then

           A12: x in ( LSeg (( E-max X),( NE-corner X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A11;

          x in X by A11, XBOOLE_0:def 4;

          then p in ( E-most X) by A12, A10, XBOOLE_0:def 4;

          then

           A13: (p `2 ) <= (( E-max X) `2 ) by Th47;

          (( E-max X) `2 ) <= (( NE-corner X) `2 ) by Th46;

          then (( E-max X) `2 ) <= (p `2 ) by A12, TOPREAL1: 4;

          then

           A14: (p `2 ) = (( E-max X) `2 ) by A13, XXREAL_0: 1;

          (( NE-corner X) `1 ) = (( E-max X) `1 ) by Th45;

          then

           A15: (p `1 ) = (( E-max X) `1 ) by A12, GOBOARD7: 5;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( E-max X) by A15, A14, EUCLID: 53;

        end;

        ( E-max X) in ( E-most X) by Th50;

        then

         A16: ( E-max X) in X by XBOOLE_0:def 4;

        assume x = ( E-max X);

        hence x in (( LSeg (( E-max X),( NE-corner X))) /\ X) by A16, A9, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PSCOMP_1:52

    ( E-min X) = ( E-max X) implies ( E-most X) = {( E-min X)}

    proof

      assume ( E-min X) = ( E-max X);

      then ( E-most X) c= ( LSeg (( E-min X),( E-min X))) by Th48;

      then ( E-most X) c= {( E-min X)} by RLTOPSP1: 70;

      hence thesis by ZFMISC_1: 33;

    end;

    theorem :: PSCOMP_1:53

    

     Th53: (( SW-corner P) `2 ) = (( S-min P) `2 ) & (( SW-corner P) `2 ) = (( S-max P) `2 ) & (( S-min P) `2 ) = (( S-max P) `2 ) & (( S-min P) `2 ) = (( SE-corner P) `2 ) & (( S-max P) `2 ) = (( SE-corner P) `2 )

    proof

      (( S-min P) `2 ) = ( S-bound P) & (( S-max P) `2 ) = ( S-bound P) by EUCLID: 52;

      hence thesis by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:54

    

     Th54: (( SW-corner X) `1 ) <= (( S-min X) `1 ) & (( SW-corner X) `1 ) <= (( S-max X) `1 ) & (( SW-corner X) `1 ) <= (( SE-corner X) `1 ) & (( S-min X) `1 ) <= (( S-max X) `1 ) & (( S-min X) `1 ) <= (( SE-corner X) `1 ) & (( S-max X) `1 ) <= (( SE-corner X) `1 )

    proof

      set LX = ( S-most X);

      

       A1: (( S-min X) `1 ) = ( lower_bound ( proj1 | LX)) by EUCLID: 52;

      

       A2: (( SW-corner X) `1 ) = ( lower_bound ( proj1 | X)) by EUCLID: 52;

      hence (( SW-corner X) `1 ) <= (( S-min X) `1 ) by A1, Th16, XBOOLE_1: 17;

      

       A3: (( S-max X) `1 ) = ( upper_bound ( proj1 | LX)) by EUCLID: 52;

      then

       A4: (( S-min X) `1 ) <= (( S-max X) `1 ) by A1, Th7;

      (( SW-corner X) `1 ) <= (( S-min X) `1 ) by A2, A1, Th16, XBOOLE_1: 17;

      hence

       A5: (( SW-corner X) `1 ) <= (( S-max X) `1 ) by A4, XXREAL_0: 2;

      

       A6: (( SE-corner X) `1 ) = ( upper_bound ( proj1 | X)) by EUCLID: 52;

      then

       A7: (( S-max X) `1 ) <= (( SE-corner X) `1 ) by A3, Th17, XBOOLE_1: 17;

      hence (( SW-corner X) `1 ) <= (( SE-corner X) `1 ) by A5, XXREAL_0: 2;

      thus (( S-min X) `1 ) <= (( S-max X) `1 ) by A1, A3, Th7;

      thus (( S-min X) `1 ) <= (( SE-corner X) `1 ) by A4, A7, XXREAL_0: 2;

      thus thesis by A3, A6, Th17, XBOOLE_1: 17;

    end;

    theorem :: PSCOMP_1:55

    

     Th55: p in ( S-most Z) implies (p `2 ) = (( S-min Z) `2 ) & (Z is compact implies (( S-min Z) `1 ) <= (p `1 ) & (p `1 ) <= (( S-max Z) `1 ))

    proof

      

       A1: (( SW-corner Z) `2 ) = ( S-bound Z) & (( S-min Z) `2 ) = ( S-bound Z) by EUCLID: 52;

      

       A2: (( SE-corner Z) `2 ) = ( S-bound Z) by EUCLID: 52;

      assume

       A3: p in ( S-most Z);

      then p in ( LSeg (( SW-corner Z),( SE-corner Z))) by XBOOLE_0:def 4;

      hence (p `2 ) = (( S-min Z) `2 ) by A1, A2, GOBOARD7: 6;

      assume Z is compact;

      then

      reconsider Z as non empty compact Subset of ( TOP-REAL 2);

      (( S-min Z) `1 ) = ( lower_bound ( proj1 | ( S-most Z))) & (( S-max Z) `1 ) = ( upper_bound ( proj1 | ( S-most Z))) by EUCLID: 52;

      hence thesis by A3, Lm3;

    end;

    theorem :: PSCOMP_1:56

    

     Th56: ( S-most X) c= ( LSeg (( S-min X),( S-max X)))

    proof

      let x be object;

      assume

       A1: x in ( S-most X);

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A2: (p `1 ) <= (( S-max X) `1 ) by A1, Th55;

      

       A3: (( S-min X) `2 ) = (( S-max X) `2 ) by Th53;

      (p `2 ) = (( S-min X) `2 ) & (( S-min X) `1 ) <= (p `1 ) by A1, Th55;

      hence thesis by A3, A2, GOBOARD7: 8;

    end;

    theorem :: PSCOMP_1:57

    ( LSeg (( S-min X),( S-max X))) c= ( LSeg (( SW-corner X),( SE-corner X)))

    proof

      

       A1: (( SW-corner X) `2 ) = ( S-bound X) & (( SE-corner X) `2 ) = ( S-bound X) by EUCLID: 52;

      

       A2: (( S-max X) `1 ) <= (( SE-corner X) `1 ) by Th54;

      (( S-max X) `2 ) = ( S-bound X) & (( SW-corner X) `1 ) <= (( S-max X) `1 ) by Th54, EUCLID: 52;

      then

       A3: ( S-max X) in ( LSeg (( SW-corner X),( SE-corner X))) by A1, A2, GOBOARD7: 8;

      

       A4: (( S-min X) `1 ) <= (( SE-corner X) `1 ) by Th54;

      (( S-min X) `2 ) = ( S-bound X) & (( SW-corner X) `1 ) <= (( S-min X) `1 ) by Th54, EUCLID: 52;

      then ( S-min X) in ( LSeg (( SW-corner X),( SE-corner X))) by A1, A4, GOBOARD7: 8;

      hence thesis by A3, TOPREAL1: 6;

    end;

    theorem :: PSCOMP_1:58

    

     Th58: ( S-min X) in ( S-most X) & ( S-max X) in ( S-most X)

    proof

      set p2W = ( proj1 | ( S-most X)), c = the carrier of (( TOP-REAL 2) | ( S-most X));

      

       A1: (( SW-corner X) `2 ) = ( S-bound X) & (( SE-corner X) `2 ) = ( S-bound X) by EUCLID: 52;

      (p2W .: c) is with_min by MEASURE6:def 13;

      then ( lower_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A2: p in c and p in c and

       A3: ( lower_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      

       A4: c = ( S-most X) by PRE_TOPC: 8;

      then

      reconsider p as Point of ( TOP-REAL 2) by A2;

      p in ( LSeg (( SW-corner X),( SE-corner X))) by A4, A2, XBOOLE_0:def 4;

      then

       A5: (p `2 ) = ( S-bound X) by A1, GOBOARD7: 6;

      

       A6: (( SW-corner X) `2 ) = ( S-bound X) & (( SE-corner X) `2 ) = ( S-bound X) by EUCLID: 52;

      (p2W . p) = (p `1 ) by A4, A2, Th22;

      hence ( S-min X) in ( S-most X) by A4, A2, A3, A5, EUCLID: 53;

      (p2W .: c) is with_max by MEASURE6:def 12;

      then ( upper_bound (p2W .: c)) in (p2W .: c);

      then

      consider p be object such that

       A7: p in c and p in c and

       A8: ( upper_bound (p2W .: c)) = (p2W . p) by FUNCT_2: 64;

      reconsider p as Point of ( TOP-REAL 2) by A4, A7;

      p in ( LSeg (( SW-corner X),( SE-corner X))) by A4, A7, XBOOLE_0:def 4;

      then

       A9: (p `2 ) = ( S-bound X) by A6, GOBOARD7: 6;

      (p2W . p) = (p `1 ) by A4, A7, Th22;

      hence thesis by A4, A7, A8, A9, EUCLID: 53;

    end;

    theorem :: PSCOMP_1:59

    (( LSeg (( SW-corner X),( S-min X))) /\ X) = {( S-min X)} & (( LSeg (( S-max X),( SE-corner X))) /\ X) = {( S-max X)}

    proof

      now

        let x be object;

        

         A1: ( S-min X) in ( LSeg (( SW-corner X),( S-min X))) by RLTOPSP1: 68;

        hereby

          ( S-min X) in ( S-most X) by Th58;

          then ( SW-corner X) in ( LSeg (( SW-corner X),( SE-corner X))) & ( S-min X) in ( LSeg (( SW-corner X),( SE-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A2: ( LSeg (( SW-corner X),( S-min X))) c= ( LSeg (( SW-corner X),( SE-corner X))) by TOPREAL1: 6;

          assume

           A3: x in (( LSeg (( SW-corner X),( S-min X))) /\ X);

          then

           A4: x in ( LSeg (( SW-corner X),( S-min X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A3;

          x in X by A3, XBOOLE_0:def 4;

          then p in ( S-most X) by A4, A2, XBOOLE_0:def 4;

          then

           A5: (( S-min X) `1 ) <= (p `1 ) by Th55;

          (( SW-corner X) `1 ) <= (( S-min X) `1 ) by Th54;

          then (p `1 ) <= (( S-min X) `1 ) by A4, TOPREAL1: 3;

          then

           A6: (p `1 ) = (( S-min X) `1 ) by A5, XXREAL_0: 1;

          (( SW-corner X) `2 ) = (( S-min X) `2 ) by Th53;

          then

           A7: (p `2 ) = (( S-min X) `2 ) by A4, GOBOARD7: 6;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( S-min X) by A7, A6, EUCLID: 53;

        end;

        ( S-min X) in ( S-most X) by Th58;

        then

         A8: ( S-min X) in X by XBOOLE_0:def 4;

        assume x = ( S-min X);

        hence x in (( LSeg (( SW-corner X),( S-min X))) /\ X) by A8, A1, XBOOLE_0:def 4;

      end;

      hence (( LSeg (( SW-corner X),( S-min X))) /\ X) = {( S-min X)} by TARSKI:def 1;

      now

        let x be object;

        

         A9: ( S-max X) in ( LSeg (( S-max X),( SE-corner X))) by RLTOPSP1: 68;

        hereby

          ( S-max X) in ( S-most X) by Th58;

          then ( SE-corner X) in ( LSeg (( SW-corner X),( SE-corner X))) & ( S-max X) in ( LSeg (( SW-corner X),( SE-corner X))) by RLTOPSP1: 68, XBOOLE_0:def 4;

          then

           A10: ( LSeg (( S-max X),( SE-corner X))) c= ( LSeg (( SW-corner X),( SE-corner X))) by TOPREAL1: 6;

          assume

           A11: x in (( LSeg (( S-max X),( SE-corner X))) /\ X);

          then

           A12: x in ( LSeg (( S-max X),( SE-corner X))) by XBOOLE_0:def 4;

          reconsider p = x as Point of ( TOP-REAL 2) by A11;

          x in X by A11, XBOOLE_0:def 4;

          then p in ( S-most X) by A12, A10, XBOOLE_0:def 4;

          then

           A13: (p `1 ) <= (( S-max X) `1 ) by Th55;

          (( S-max X) `1 ) <= (( SE-corner X) `1 ) by Th54;

          then (( S-max X) `1 ) <= (p `1 ) by A12, TOPREAL1: 3;

          then

           A14: (p `1 ) = (( S-max X) `1 ) by A13, XXREAL_0: 1;

          (( SE-corner X) `2 ) = (( S-max X) `2 ) by Th53;

          then

           A15: (p `2 ) = (( S-max X) `2 ) by A12, GOBOARD7: 6;

          p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          hence x = ( S-max X) by A15, A14, EUCLID: 53;

        end;

        ( S-max X) in ( S-most X) by Th58;

        then

         A16: ( S-max X) in X by XBOOLE_0:def 4;

        assume x = ( S-max X);

        hence x in (( LSeg (( S-max X),( SE-corner X))) /\ X) by A16, A9, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PSCOMP_1:60

    ( S-min X) = ( S-max X) implies ( S-most X) = {( S-min X)}

    proof

      assume ( S-min X) = ( S-max X);

      then ( S-most X) c= ( LSeg (( S-min X),( S-min X))) by Th56;

      then ( S-most X) c= {( S-min X)} by RLTOPSP1: 70;

      hence thesis by ZFMISC_1: 33;

    end;

    theorem :: PSCOMP_1:61

    ( W-max P) = ( N-min P) implies ( W-max P) = ( NW-corner P)

    proof

      

       A1: (( W-max P) `1 ) = ( W-bound P) by EUCLID: 52;

      assume ( W-max P) = ( N-min P);

      hence thesis by A1, EUCLID: 52;

    end;

    theorem :: PSCOMP_1:62

    ( N-max P) = ( E-max P) implies ( N-max P) = ( NE-corner P)

    proof

      

       A1: (( N-max P) `2 ) = ( N-bound P) by EUCLID: 52;

      assume ( N-max P) = ( E-max P);

      hence thesis by A1, EUCLID: 52;

    end;

    theorem :: PSCOMP_1:63

    ( E-min P) = ( S-max P) implies ( E-min P) = ( SE-corner P)

    proof

      

       A1: (( E-min P) `1 ) = ( E-bound P) by EUCLID: 52;

      assume ( E-min P) = ( S-max P);

      hence thesis by A1, EUCLID: 52;

    end;

    theorem :: PSCOMP_1:64

    ( S-min P) = ( W-min P) implies ( S-min P) = ( SW-corner P)

    proof

      

       A1: (( S-min P) `2 ) = ( S-bound P) by EUCLID: 52;

      assume ( S-min P) = ( W-min P);

      hence thesis by A1, EUCLID: 52;

    end;

    theorem :: PSCOMP_1:65

    ( proj2 . |[r, s]|) = s & ( proj1 . |[r, s]|) = r

    proof

      

      thus ( proj2 . |[r, s]|) = ( |[r, s]| `2 ) by Def6

      .= s by EUCLID: 52;

      

      thus ( proj1 . |[r, s]|) = ( |[r, s]| `1 ) by Def5

      .= r by EUCLID: 52;

    end;

    theorem :: PSCOMP_1:66

    for X be non empty Subset of ( TOP-REAL 2) holds for Y be compact Subset of ( TOP-REAL 2) st X c= Y holds ( N-bound X) <= ( N-bound Y) by Th17;

    theorem :: PSCOMP_1:67

    for X be non empty Subset of ( TOP-REAL 2) holds for Y be compact Subset of ( TOP-REAL 2) st X c= Y holds ( E-bound X) <= ( E-bound Y) by Th17;

    theorem :: PSCOMP_1:68

    for X be non empty Subset of ( TOP-REAL 2) holds for Y be compact Subset of ( TOP-REAL 2) st X c= Y holds ( S-bound X) >= ( S-bound Y) by Th16;

    theorem :: PSCOMP_1:69

    for X be non empty Subset of ( TOP-REAL 2) holds for Y be compact Subset of ( TOP-REAL 2) st X c= Y holds ( W-bound X) >= ( W-bound Y) by Th16;