The Mizar article:

Bounding Boxes for Compact Sets in $\calE^2$

by
Czeslaw Bylinski, and
Piotr Rudnicki

Received July 29, 1997

Copyright (c) 1997 Association of Mizar Users

MML identifier: PSCOMP_1
[ MML identifier index ]


environ

 vocabulary AMI_1, FREEALG, HAHNBAN, COMPTS_1, BOOLE, FINSET_1, ZFMISC_1,
      SETFAM_1, FUNCT_1, RELAT_1, ABSVALUE, ARYTM_1, SEQ_1, SEQ_2, ORDINAL2,
      LATTICES, ARYTM_3, SEQ_4, PRE_TOPC, RCOMP_1, FUNCOP_1, PRALG_1, SUBSET_1,
      NEWTON, INT_1, REALSET1, LIMFUNC1, PCOMPS_1, EUCLID, TOPREAL1, FUNCT_5,
      MCART_1, PSCOMP_1, ARYTM, MEMBERED;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      SETFAM_1, FINSET_1, STRUCT_0, FINSOP_1, ABSVALUE, REAL_1, NAT_1, INT_1,
      MEMBERED, RELAT_1, FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, AMI_1, SEQ_4, RCOMP_1,
      LIMFUNC1, PRE_TOPC, TOPS_2, COMPTS_1, PCOMPS_1, EUCLID, TOPREAL1;
 constructors REAL_1, TOPS_2, NAT_1, INT_1, FINSOP_1, ABSVALUE, SEQ_2, SEQ_4,
      AMI_1, RCOMP_1, COMPTS_1, LIMFUNC1, TOPREAL1, SEQM_3, TSP_1, PCOMPS_1,
      XCMPLX_0, XREAL_0, MEMBERED, RELSET_1, PARTFUN1, XBOOLE_0;
 clusters NUMBERS, SUBSET_1, STRUCT_0, PRE_TOPC, RCOMP_1, SEQM_3, EUCLID,
      PCOMPS_1, FUNCT_1, XREAL_0, RELSET_1, SEQ_1, REAL_1, SETFAM_1, INT_1,
      XBOOLE_0, SEQ_2, NAT_1, MEMBERED, RELAT_1, FUNCT_2, ZFMISC_1, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, SEQ_2, SEQ_4, TOPS_2, COMPTS_1, RCOMP_1, ORDINAL1,
      XBOOLE_0;
 theorems TARSKI, AXIOMS, REAL_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, SEQ_4,
      SUBSET_1, SQUARE_1, REAL_2, FCONT_3, RCOMP_1, FUNCOP_1, ABSVALUE, NAT_1,
      INT_1, EUCLID, RFUNCT_2, SEQ_1, SEQ_2, BORSUK_1, TOPS_1, TSP_1, COMPTS_1,
      LIMFUNC1, SETFAM_1, ZFMISC_1, AMI_1, PCOMPS_1, TOPREAL1, JORDAN1,
      GOBOARD7, SPPOL_1, RELSET_1, XREAL_0, ORDINAL1, XBOOLE_0, XBOOLE_1,
      PARTFUN1, XCMPLX_0, XCMPLX_1;
 schemes FINSET_1, FUNCT_2, COMPLSP1, COMPTS_1;

begin :: Preliminaries

definition let X be set;
 redefine attr X is with_non-empty_elements means
:Def1: not 0 in X;
 compatibility by AMI_1:def 1;
 synonym X is without_zero;
 antonym X is with_zero;
end;

definition
 cluster REAL -> with_zero;
 coherence by Def1;
 cluster NAT -> with_zero;
 coherence by Def1;
end;

definition
 cluster non empty without_zero set;
 existence proof set s = {1};
  take s;
  thus s is non empty; not 0 in s by TARSKI:def 1;
  hence s is without_zero by Def1;
 end;
 cluster non empty with_zero set;
 existence by Def1;
end;

definition
 cluster non empty without_zero Subset of REAL;
 existence proof set s = {1 qua Real};
  take s;
  thus s is non empty; not 0 in s by TARSKI:def 1;
  hence s is without_zero by Def1;
 end;
 cluster non empty with_zero Subset of REAL;
 existence by Def1;
end;

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

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

definition let A, B be set, f be Function of A, B;
 redefine func rng f -> Subset of B;
 coherence by RELSET_1:12;
end;

definition let X, Y be non empty set, f be Function of X, Y;
   :: see WAYBEL_2
 cluster f.:X -> non empty;
coherence proof
    consider x being Element of X;
A1: dom f = X by FUNCT_2:def 1;
    then f.x in rng f by FUNCT_1:def 5;
    hence thesis by A1,FUNCT_1:def 12;
  end;
end;

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

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

 reserve r, s, t, t' for real number;

theorem Th3:
 abs r + abs s = 0 implies r = 0
proof assume
A1: abs(r)+abs(s) = 0;
   set aa = abs(r), ab = abs(s);
A2: 0 <= aa & 0 <= ab by ABSVALUE:5;
     aa = -ab by A1,XCMPLX_0:def 6;
  then aa = 0 by A2,REAL_1:66;
 hence r = 0 by ABSVALUE:7;
end;

theorem Th4:
r < s & s < t implies abs s < abs r + abs t
proof assume
A1: r < s & s < t;
 per cases;
 suppose A2: s<0; then r<0 by A1,AXIOMS:22;
 then A3: -s = abs(s) & -r = abs(r) by A2,ABSVALUE:def 1;
 A4: -s < -r by A1,REAL_1:50;
      0 <= abs(t) by ABSVALUE:5;
    then -s+0 < -r+abs(t) by A4,REAL_1:67;
  hence abs(s) < abs(r)+abs(t) by A3;
 suppose A5: 0<=s; then 0<t by A1;
 then A6: s = abs(s) & t = abs(t) by A5,ABSVALUE:def 1;
      0 <= abs(r) by ABSVALUE:5;
    then s+0 < t+abs(r) by A1,REAL_1:67;
 hence abs(s) < abs(r)+abs(t) by A6;
end;

theorem Th5:
-s < r & r < s implies abs r < s
proof assume that
A1: -s < r & r < s and
A2: abs(r) >= s;
     abs(r) <= s by A1,ABSVALUE:12;
then A3: abs(r) = s by A2,AXIOMS:21;
      0 <= r or r < 0;
    then r = s or -r = s by A3,ABSVALUE:def 1;
 hence contradiction by A1;
end;

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

theorem Th6:
seq is convergent & seq is_not_0 & lim seq = 0 implies seq" is non bounded
proof assume that
A1: seq is convergent and
A2: seq is_not_0 and
A3: lim seq = 0;
   given a being real number such that
A4: for n being Nat holds (seq").n<a;
   given b being real number such that
A5: for n being Nat holds b<(seq").n;
   set aa = abs(a), ab = abs(b);
   set rab = 1/(aa+ab);
A6: b<(seq").1 & (seq").1<a by A4,A5;
      0 <= aa & 0 <= ab by ABSVALUE:5;
then A7: 0+0 <= aa+ab by REAL_1:55;
  now assume 0 >= aa+ab;
       then aa+ab = 0 by A7;
       then a = 0 & b = 0 by Th3;
     hence contradiction by A6;
    end;
   then 0 < (aa+ab)" by REAL_1:72;
then A8: 0 < rab by XCMPLX_1:217;
A9: now let n be Nat;
       set s = seq.n, t = (seq").n;
       set At = abs(t);
        b<t & t<a by A4,A5;
   then A10: At < aa+ab by Th4;
   A11: s <> 0 by A2,SEQ_1:7;
   A12: t = s" by SEQ_1:def 8
        .= 1/s by XCMPLX_1:217;
       then t <> 0 by A11,XCMPLX_1:62;
   then A13: 0 < At by ABSVALUE:6;
   A14: At = 1/(abs(s)) by A12,ABSVALUE:15;
         1/At > rab by A10,A13,REAL_2:151;
    hence abs(seq.n) > rab by A14,XCMPLX_1:56;
   end;
   consider n being Nat such that
A15: for m being Nat st n<=m holds abs(seq.m-0)<rab by A1,A3,A8,SEQ_2:def 7;
     abs(seq.n-0)<rab by A15;
 hence contradiction by A9;
end;

theorem Th7:
rng seq is bounded iff seq is bounded
proof
 thus rng seq is bounded implies seq is bounded proof
   given s such that
A1: for r st r in rng seq holds r>=s;
   given t such that
A2: for r st r in rng seq holds r<=t;
 thus seq is bounded_above proof
  take t+1;
  let n be Nat;
     seq.n in rng seq by FUNCT_2:6;
  then A3: seq.n <= t by A2;
     t < t+1 by REAL_1:69;
  hence seq.n < t+1 by A3,AXIOMS:22;
 end;
  take s-1;
  let n be Nat;
     seq.n in rng seq by FUNCT_2:6;
  then A4: seq.n >= s by A1;
     s < s+1 by REAL_1:69;
   then s-1 < s by REAL_1:84;
  hence s-1 < seq.n by A4,AXIOMS:22;
 end;
 given t such that
A5: for n being Nat holds seq.n<t;
 given s such that
A6: for n being Nat holds seq.n>s;
A7: dom seq = NAT by FUNCT_2:def 1;
 thus rng seq is bounded_below proof
  take s;
  let r; assume r in rng seq;
   then ex n being set st n in dom seq & seq.n = r by FUNCT_1:def 5;
  hence s<=r by A6,A7;
 end;
 take t;
 let r; assume
   r in rng seq;
   then ex n being set st n in dom seq & seq.n = r by FUNCT_1:def 5;
  hence r<=t by A5,A7;
end;

definition let X be real-membered set;
 redefine func upper_bound X; synonym sup X;
 redefine func lower_bound X; synonym inf X;
end;

definition let X be Subset of REAL;
 redefine func sup X -> Element of REAL;
coherence by XREAL_0:def 1;
 redefine func inf X -> Element of REAL;
coherence by XREAL_0:def 1;
end;

theorem Th8:
 for X being non empty real-membered set
 for t st for s st s in X holds s >= t holds inf X >= t
proof let X be non empty real-membered set;
 set r = inf X;
  let t; assume
 A1: for s st s in X holds s >= t;
 then A2: X is bounded_below by SEQ_4:def 2;
     set s = t-r;
  assume r < t;
   then s > 0 by SQUARE_1:11;
   then consider t' be real number such that
A3: t' in X & t' < r+s by A2,SEQ_4:def 5;
      r+s = t by XCMPLX_1:27;
  hence contradiction by A1,A3;
end;

theorem Th9:
for X being non empty real-membered set
 st (for s st s in X holds s >= r) &
    for t st for s st s in X holds s >= t holds r >= t
  holds r = inf X
proof let X be non empty real-membered set;
 assume that
A1: for s st s in X holds s >= r and
A2: for t st for s st s in X holds s >= t holds r >= t;
  A3: X is bounded_below by A1,SEQ_4:def 2;
    now let s be real number such that
  A4: 0 < s;
  assume for t be real number st t in X holds t >= r+s;
      then r >= r+s by A2;
   hence contradiction by A4,REAL_1:69;
  end;
 hence r = inf X by A1,A3,SEQ_4:def 5;
end;

theorem Th10:
for X being non empty real-membered set, r
 for t st for s st s in X holds s <= t holds sup X <= t
proof let X be non empty real-membered set, r;
 set r = sup X;
  let t; assume
 A1: for s st s in X holds s <= t;
 then A2: X is bounded_above by SEQ_4:def 1;
     set s = r-t;
  assume r > t;
   then s > 0 by SQUARE_1:11; then consider t' be real number such that
 A3: t' in X & r-s < t' by A2,SEQ_4:def 4;
      r-s = t by XCMPLX_1:18;
  hence contradiction by A1,A3;
end;

theorem Th11:
for X being non empty real-membered set, r
 st (for s st s in X holds s <= r) &
    for t st for s st s in X holds s <= t holds r <= t
  holds r = sup X
proof let X be non empty real-membered set, r;
 assume that
A1: for s st s in X holds s <= r and
A2: for t st for s st s in X holds s <= t holds r <= t;
   A3: X is bounded_above by A1,SEQ_4:def 1;
    now let s be real number such that
  A4: 0 < s;
   assume
        for t be real number st t in X holds r-s >= t;
      then r <= r-s by A2; then r+s <= r by REAL_1:84;
   hence contradiction by A4,REAL_1:69;
  end;
 hence r = sup X by A1,A3,SEQ_4:def 4;
end;

theorem Th12:
 for X being non empty real-membered set, Y being real-membered set
  st X c= Y & Y is bounded_below holds inf Y <= inf X
proof let X be non empty real-membered set, Y be real-membered set; assume that
A1: X c= Y and
A2: Y is bounded_below;
  t in X implies t >= inf Y by A1,A2,SEQ_4:def 5;
 hence inf Y <= inf X by Th8;
end;

theorem Th13:
 for X being non empty real-membered set, Y being real-membered set
  st X c= Y & Y is bounded_above holds sup X <= sup Y
proof let X be non empty real-membered set, Y be real-membered set; assume that
A1: X c= Y and
A2: Y is bounded_above;
  t in X implies t <= sup Y by A1,A2,SEQ_4:def 4;
 hence sup X <= sup Y by Th10;
end;

definition let X be real-membered set;
 attr X is with_max means
:Def3: X is bounded_above & sup X in X;
 attr X is with_min means
:Def4: X is bounded_below & inf X in X;
end;

definition
 cluster non empty closed bounded Subset of REAL;
 existence proof
   reconsider 0r = 0 as Real;
     [.0,0.]={0} & [.0,0.] is closed & {0r} is bounded by RCOMP_1:14,23,SEQ_4:
15
;
  hence thesis;
 end;
end;

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

 reserve p, q, r3, r1, r2, q3, p3 for Real;

definition let X be Subset of REAL;
 func -X -> Subset of REAL equals
:Def7: { -r3 : r3 in X};
 coherence
 proof
  defpred P[set] means $1 in X;
  deffunc F(Real) = -$1;
  thus { F(r3) : P[r3]} is Subset of REAL from SubsetFD;
 end;
 involutiveness
  proof
   let IT,X be Subset of REAL;
   assume
A1:  IT = { -r3 : r3 in X};
   thus X c= { -r3 : r3 in IT}
     proof let e be set;
      assume
A2:     e in X;
       then reconsider r0 = e as Element of REAL;
A3:     e = --r0;
         -r0 in IT by A1,A2;
      hence e in { -r3 : r3 in IT} by A3;
     end;
   let e be set;
   assume e in { -r3 : r3 in IT};
    then consider r0 being Element of REAL such that
A4:  -r0 = e and
A5:  r0 in IT;
      ex r1 being Element of REAL st -r1 = r0 & r1 in X by A1,A5;
   hence e in X by A4;
  end;
end;

theorem Th14:
r in X iff -r in -X
proof
A1: -X = { -p : p in X } by Def7;
 hence r in X implies -r in -X;
 assume -r in -X; then consider mr being Real such that
 A2: -r = -mr & mr in X by A1;
      --r = r & --mr = mr;
 hence r in X by A2;
end;

definition let X be non empty Subset of REAL;
 cluster -X -> non empty;
 coherence proof
     ex x being Real st x in X by SUBSET_1:10;
  hence thesis by Th14;
 end;
end;

Lm1:
for X being Subset of REAL
 st X is bounded_above holds -X is bounded_below
proof let X be Subset of REAL; given s such that
A1: for t st t in X holds t <= s;
  take -s;
  let t; assume t in -X; then t in { -r3 : r3 in X } by Def7;
   then consider r3 such that
A2: t = -r3 & r3 in X;
     r3 <= s by A1,A2;
 hence t >= -s by A2,REAL_1:50;
end;

Lm2:
for X being Subset of REAL
 st X is bounded_below holds -X is bounded_above
proof let X be Subset of REAL; given s such that
A1: for t st t in X holds t >= s;
  take -s;
  let t; assume t in -X; then t in { -r3 : r3 in X } by Def7;
   then consider r3 such that
A2: t = -r3 & r3 in X;
     r3 >= s by A1,A2;
 hence t <= -s by A2,REAL_1:50;
end;

theorem Th15:
X is bounded_above iff -X is bounded_below
proof X = --X;
 hence X is bounded_above iff -X is bounded_below by Lm1,Lm2;
end;

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

theorem Th17:
for X being non empty Subset of REAL
 st X is bounded_below holds inf X = - sup -X
proof let X be non empty Subset of REAL; assume
      X is bounded_below;
then A1: -X is bounded_above by Lm2;
   set r = - sup -X;
A2: now let s; assume s in X; then -s in -X by Th14;
      then -s <= -r by A1,SEQ_4:def 4;
     hence s >= r by REAL_1:50;
   end;
     now let t; assume
   A3:  for s st s in X holds s >= t;
       now let s; assume s in -X; then -s in --X by Th14;
       then -s >= t by A3; then --s <= -t by REAL_1:50;
      hence s <= -t;
     end;
     then -r <= -t by Th10;
    hence r >= t by REAL_1:50;
   end;
 hence inf X = - sup -X by A2,Th9;
end;

theorem Th18:
for X being non empty Subset of REAL
 st X is bounded_above holds sup X = - inf -X
proof let X be non empty Subset of REAL; assume
      X is bounded_above;
then A1: -X is bounded_below by Lm1;
   set r = - inf -X;
A2: now let t; assume t in X; then -t in -X by Th14;
      then -t >= -r by A1,SEQ_4:def 5;
     hence t <= r by REAL_1:50;
   end;
     now let s; assume
   A3:  for t st t in X holds t <= s;
       now let t; assume t in -X; then -t in --X by Th14;
       then -t <= s by A3; then --t >= -s by REAL_1:50;
      hence t >= -s;
     end;
     then -r >= -s by Th8;
    hence r <= s by REAL_1:50;
   end;
 hence sup X = - inf -X by A2,Th11;
end;

Lm3:
for X being Subset of REAL st X is closed holds -X is closed
proof let X be Subset of REAL; assume
A1: X is closed;
 let s1 be Real_Sequence; assume that
A2: (rng s1) c= -X and
A3: s1 is convergent;
A4: -s1 is convergent by A3,SEQ_2:23;
  rng -s1 c= X proof let x be set; assume
         x in rng -s1; then consider n being set such that
   A5: n in dom -s1 and
   A6: x = (-s1).n by FUNCT_1:def 5;
       reconsider n as Nat by A5,FUNCT_2:def 1;
   A7: x = -(s1.n) by A6,SEQ_1:14;
         s1.n in rng s1 by FUNCT_2:6;
       then x in --X by A2,A7,Th14;
    hence x in X;
   end;
then A8: lim -s1 in X by A1,A4,RCOMP_1:def 4;
     - lim s1 = lim -s1 by A3,SEQ_2:24;
   then --lim s1 in -X by A8,Th14;
  hence lim s1 in -X;
end;

theorem Th19:
X is closed iff -X is closed
proof --X = X; hence thesis by Lm3; end;

definition let X be Subset of REAL, p be Real;
 func p+X -> Subset of REAL equals
:Def8: { p+r3 : r3 in X};
 coherence
 proof
  defpred P[set] means $1 in X;
  deffunc F(Real) = p+$1;
  thus { F(r3) : P[r3]} is Subset of REAL from SubsetFD;
 end;
end;

theorem Th20:
r in X iff q3+r in q3+X
proof
A1: q3+X = { q3+p : p in X } by Def8;
 hence r in X implies q3+r in q3+X;
 assume q3+r in q3+X; then ex mr being Real st q3+r = q3+mr & mr in X by A1;
 hence r in X by XCMPLX_1:2;
end;

definition let X be non empty Subset of REAL, s be Real;
 cluster s+X -> non empty;
 coherence proof ex x being Real st x in X by SUBSET_1:10;
  hence thesis by Th20;
 end;
end;

theorem Th21:
X = 0+X
proof
A1: 0+X = {0+r3 : r3 in X} by Def8;
    now let x be set;
   hereby assume
   A2: x in X; then reconsider x' = x as Real;
        0+x' = x;
    hence x in 0+X by A1,A2;
   end; assume x in 0+X; then consider r3 such that
   A3: x = 0+r3 & r3 in X by A1;
   thus x in X by A3;
  end;
 hence X = 0+X by TARSKI:2;
end;

theorem Th22:
q3+(p3+X) = (q3+p3)+X
proof
A1: q3+(p3+X) = {q3+r3 : r3 in p3+X} by Def8;
A2: p3+X = {p3+r3 : r3 in X} by Def8;
A3: (q3+p3)+X = {(q3+p3)+r3 : r3 in X} by Def8;
    now let x be set;
   hereby assume x in q3+(p3+X); then consider r3 such that
   A4: x = q3+r3 & r3 in p3+X by A1;
      consider q such that
   A5: r3 = p3+q & q in X by A2,A4;
        x = (q3+p3)+q by A4,A5,XCMPLX_1:1;
    hence x in (q3+p3)+X by A3,A5;
   end; assume x in (q3+p3)+X; then consider r3 such that
   A6: x = (q3+p3)+r3 & r3 in X by A3;
        p3+r3 in p3+X by A2,A6;
      then q3+(p3+r3) in q3+(p3+X) by A1;
   hence x in q3+(p3+X) by A6,XCMPLX_1:1;
  end;
 hence q3+(p3+X) = (q3+p3)+X by TARSKI:2;
end;

Lm4:
for X being Subset of REAL, s being Real
 st X is bounded_above holds s+X is bounded_above
proof let X be Subset of REAL, p be Real; given s such that
A1: for t st t in X holds t <= s;
  take p+s;
  let t; assume t in p+X; then t in { p+r3 : r3 in X } by Def8;
   then consider r3 such that
A2: t = p+r3 & r3 in X;
     r3 <= s by A1,A2;
 hence t <= p+s by A2,AXIOMS:24;
end;

theorem
  X is bounded_above iff q3+X is bounded_above
proof -q3+(q3+X) = (-q3+q3)+X by Th22 .= 0+X by XCMPLX_0:def 6 .= X by Th21;
 hence thesis by Lm4;
end;

Lm5:
for X being Subset of REAL, p being Real
 st X is bounded_below holds p+X is bounded_below
proof let X be Subset of REAL, p be Real; given s such that
A1: for t st t in X holds t >= s;
  take p+s;
  let t; assume t in p+X; then t in { p+r3 : r3 in X } by Def8;
   then consider r3 such that
A2: t = p+r3 & r3 in X;
     r3 >= s by A1,A2;
 hence t >= p+s by A2,AXIOMS:24;
end;

theorem
  X is bounded_below iff q3+X is bounded_below
proof
    -q3+(q3+X) = (-q3+q3)+X by Th22 .= 0+X by XCMPLX_0:def 6 .= X by Th21;
 hence thesis by Lm5;
end;

theorem
  for X being non empty Subset of REAL
 st X is bounded_below holds inf (q3+X) = q3+inf X
proof let X be non empty Subset of REAL such that
A1: X is bounded_below;
   set i = q3+inf X;
A2: q3+X = {q3+r3 : r3 in X} by Def8;
A3: now let s; assume s in q3+X; then consider r3 such that
   A4: q3+r3 = s & r3 in X by A2;
         r3 >= inf X by A1,A4,SEQ_4:def 5;
     hence s >= i by A4,AXIOMS:24;
   end;
     now let t; assume
   A5:  for s st s in q3+X holds s >= t;
       now let s; assume s in X; then q3+s in q3+X by A2;
        then t <= q3+s by A5;
      hence t-q3 <= s by REAL_1:86;
     end; then inf X >= t-q3 by Th8;
    hence t <= i by REAL_1:86;
   end;
 hence inf (q3+X) = q3+ inf X by A3,Th9;
end;

theorem
  for X being non empty Subset of REAL
 st X is bounded_above holds sup (q3+X) = q3+sup X
proof let X be non empty Subset of REAL such that
A1: X is bounded_above;
   set i = q3+sup X;
A2: q3+X = {q3+r3 : r3 in X} by Def8;
A3: now let s; assume s in q3+X; then consider r3 such that
   A4: q3+r3 = s & r3 in X by A2;
         r3 <= sup X by A1,A4,SEQ_4:def 4;
     hence s <= i by A4,AXIOMS:24;
   end;
     now let t; assume
   A5:  for s st s in q3+X holds s <= t;
       now let s; assume s in X; then q3+s in q3+X by A2;
        then q3+s <= t by A5;
      hence s <= t-q3 by REAL_1:84;
     end; then sup X <= t-q3 by Th10;
    hence i <= t by REAL_1:84;
   end;
 hence sup (q3+X) = q3+ sup X by A3,Th11;
end;

Lm6:
for X being Subset of REAL st X is closed holds q3+X is closed
proof let X be Subset of REAL; assume
A1: X is closed;
 let s1 be Real_Sequence; assume that
A2: (rng s1) c= q3+X and
A3: s1 is convergent;
   reconsider s0 = (NAT --> q3) as Real_Sequence;
   s0 is convergent by SEQ_4:39;
then A4: s1-s0 is convergent by A3,SEQ_2:25;
  rng (s1-s0) c= X proof let x be set; assume
   A5: x in rng (s1-s0); then consider n being set such that
   A6: n in dom (s1-s0) and
   A7: x = (s1-s0).n by FUNCT_1:def 5;
       reconsider n as Nat by A6,FUNCT_2:def 1;
       reconsider x' = x as Real by A5;
   A8: x = (s1+-s0).n by A7,SEQ_1:15
        .= s1.n + (-s0).n by SEQ_1:11
        .= s1.n + -(s0.n) by SEQ_1:14
        .= s1.n + - q3 by FUNCOP_1:13
        .= s1.n - q3 by XCMPLX_0:def 8;
         s1.n in rng s1 by FUNCT_2:6;
       then s1.n in q3+X by A2;
       then x'+q3 in q3+X by A8,XCMPLX_1:27;
    hence x in X by Th20;
   end;
then A9: lim (s1-s0) in X by A1,A4,RCOMP_1:def 4;
     lim (s1-s0) = (lim s1) - s0.0 by A3,SEQ_4:59
              .= (lim s1) - q3 by FUNCOP_1:13;
   then q3+lim(s1-s0) = lim s1 by XCMPLX_1:27;
  hence lim s1 in q3+X by A9,Th20;
end;

theorem Th27:
X is closed iff q3+X is closed
proof -q3+(q3+X) = (-q3+q3)+X by Th22 .= 0+X by XCMPLX_0:def 6 .= X by Th21;
 hence thesis by Lm6;
end;

definition let X be Subset of REAL;
 func Inv X -> Subset of REAL equals
:Def9: { 1/r3 : r3 in X};
 coherence
 proof
  defpred P[set] means $1 in X;
  deffunc F(Real) = 1/$1;
  thus { F(r3) : P[r3]} is Subset of REAL from SubsetFD;
 end;
end;

theorem Th28:
for X being without_zero Subset of REAL holds r in X iff 1/r in Inv X
proof let X be without_zero Subset of REAL;
A1: Inv X = { 1/p : p in X } by Def9;
 hence r in X implies 1/r in Inv X;
 assume 1/r in Inv X; then consider mr being Real such that
 A2: 1/r = 1/mr & mr in X by A1;
 thus r in X by A2,XCMPLX_1:59;
end;

definition let X be non empty without_zero Subset of REAL;
 cluster Inv X -> non empty without_zero;
 coherence proof consider x being Real such that
 A1: x in X by SUBSET_1:10;
 A2: not 0 in X by Def1;
  thus Inv X is non empty by A1,Th28;
     now assume
 A3: 0 in Inv X;
      Inv X = {1/r3 : r3 in X} by Def9;
    then ex r3 st 0 = 1/r3 & r3 in X by A3;
    hence contradiction by A2,XCMPLX_1:62;
   end;
  hence thesis by Def1;
 end;
end;

definition let X be without_zero Subset of REAL;
 cluster Inv X -> without_zero;
 coherence proof
 A1: not 0 in X by Def1;
     now assume
 A2: 0 in Inv X;
      Inv X = {1/r3 : r3 in X} by Def9;
    then ex r3 st 0 = 1/r3 & r3 in X by A2;
    hence contradiction by A1,XCMPLX_1:62;
   end;
  hence thesis by Def1;
 end;
end;

theorem Th29:
for X being without_zero Subset of REAL holds Inv Inv X = X
proof let X be without_zero Subset of REAL;
    now let x be set;
   hereby assume x in Inv Inv X;
      then x in { 1/r3 : r3 in Inv X } by Def9;
      then consider rx being Real such that
   A1: x = 1/rx & rx in Inv X;
        rx in { 1/r3 : r3 in X } by A1,Def9;
      then consider rrx being Real such that
   A2: rx = 1/rrx & rrx in X;
    thus x in X by A1,A2,XCMPLX_1:56;
   end; assume
  A3: x in X;
     then reconsider rx = x as Real;
       1/rx in { 1/r3 : r3 in X } by A3;
     then 1/rx in Inv X by Def9;
     then 1/(1/rx) in { 1/r3 : r3 in Inv X };
     then 1/(1/rx) in Inv Inv X by Def9;
    hence x in Inv Inv X by XCMPLX_1:56;
  end;
 hence Inv Inv X = X by TARSKI:2;
end;

theorem
  for X being without_zero Subset of REAL
 st X is closed & X is bounded holds Inv X is closed
proof let X be without_zero Subset of REAL; assume that
A1: X is closed and
A2: X is bounded;
 let s1 be Real_Sequence; assume that
A3: (rng s1) c= Inv X and
A4: s1 is convergent;
A5: not 0 in rng s1 by A3,Def1;
A6: now assume not s1 is_not_0;
      then ex n being Nat st s1.n = 0 by SEQ_1:7;
     hence contradiction by A5,FUNCT_2:6;
    end;
A7: now assume
    A8: lim s1 = 0;
    A9: rng (s1") c= X proof let y be set; assume y in rng (s1");
            then consider x being set such that
        A10: x in dom (s1") & y = (s1").x by FUNCT_1:def 5;
            reconsider x as Nat by A10,FUNCT_2:def 1;
        A11: (s1").x = (s1.x)" by SEQ_1:def 8;
              s1.x in rng s1 by FUNCT_2:6;
            then 1/(s1.x) in Inv Inv X by A3,Th28;
            then 1/(s1.x) in X by Th29;
         hence y in X by A10,A11,XCMPLX_1:217;
        end;
          s1" is non bounded by A4,A6,A8,Th6;
        then rng (s1") is non bounded by Th7;
     hence contradiction by A2,A9,RCOMP_1:5;
    end;
then A12: s1" is convergent by A4,A6,SEQ_2:35;
  rng (s1") c= X proof let x be set; assume
         x in rng (s1"); then consider n being set such that
   A13: n in dom (s1") and
   A14: x = (s1").n by FUNCT_1:def 5;
       reconsider n as Nat by A13,FUNCT_2:def 1;
   A15: x = (s1.n)" by A14,SEQ_1:def 8;
         s1.n in rng s1 by FUNCT_2:6;
       then 1/(s1.n) in Inv Inv X by A3,Th28;
       then x in Inv Inv X by A15,XCMPLX_1:217;
    hence x in X by Th29;
   end;
then A16: lim s1" in X by A1,A12,RCOMP_1:def 4;
     (lim s1)" = lim s1" by A4,A6,A7,SEQ_2:36;
   then 1/lim s1 in X by A16,XCMPLX_1:217;
   then 1/(1/lim s1) in Inv X by Th28;
  hence lim s1 in Inv X by XCMPLX_1:56;
end;

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

definition let X be Subset of REAL;
 func Cl X -> Subset of REAL equals
:Def10: meet { A where A is Element of bool REAL : X c= A & A is closed };
 coherence proof
   defpred P[Element of bool REAL] means X c= $1 & $1 is closed;
   deffunc F(Element of bool REAL) = $1;
   reconsider Z = { F(A) where A is Element of bool REAL : P[A] }
    as Subset of bool REAL from SubsetFD;
   reconsider Z as Subset-Family of REAL by SETFAM_1:def 7;
     meet Z is Subset of REAL;
  hence thesis;
 end;
 projectivity
  proof let IT,X be Subset of REAL;
    set ClX = { A where A is Element of bool REAL : X c= A & A is closed },
        ClIT = { A where A is Element of bool REAL : IT c= A & A is closed };
   assume
A1:  IT= meet ClX;
    reconsider W = [#]REAL as Element of bool REAL;
      X c= REAL;
    then X c= W by SUBSET_1:def 4;
    then A2:  W in ClX by FCONT_3:1;
      IT c= REAL;
    then IT c= W by SUBSET_1:def 4;
    then A3:  W in ClIT by FCONT_3:1;
   thus
      IT c= meet { A where A is Element of bool REAL : IT c= A & A is closed }
    proof let e be set;
     assume
A4:   e in IT;
        for Y being set holds Y in ClIT implies e in Y
       proof let Y be set;
        assume Y in ClIT;
         then consider A being Element of bool REAL such that
A5:       A = Y and
A6:       IT c= A and
A7:       A is closed;
           for Z being set st Z in ClX holds X c= Z
          proof let Z be set;
           assume Z in ClX;
            then ex B being Element of bool REAL
                     st Z = B & X c= B & B is closed;
           hence X c= Z;
          end;
         then X c= IT by A1,A2,SETFAM_1:6;
         then X c= A by A6,XBOOLE_1:1;
         then A in ClX by A7;
        hence e in Y by A1,A4,A5,SETFAM_1:def 1;
       end;
     hence e in meet ClIT by A3,SETFAM_1:def 1;
    end;
   let e be set;
   assume
A8:  e in meet ClIT;

        for Y being set holds Y in ClX implies e in Y
       proof let Y be set;
        assume
A9:      Y in ClX;
         then consider A being Element of bool REAL such that
A10:       A = Y and
            X c= A and
A11:       A is closed;
           IT c= A by A1,A9,A10,SETFAM_1:4;
         then A in ClIT by A11;
        hence e in Y by A8,A10,SETFAM_1:def 1;
       end;
   hence e in IT by A1,A2,SETFAM_1:def 1;
  end;
end;

definition let X be Subset of REAL;
 cluster Cl X -> closed;
 coherence proof
   defpred P[Element of bool REAL] means X c= $1 & $1 is closed;
   deffunc F(Element of bool REAL) = $1;
   reconsider Z = { F(A) where A is Element of bool REAL : P[A] }
   as Subset of bool REAL from SubsetFD;
   reconsider Z as Subset-Family of REAL by SETFAM_1:def 7;
A1: Z is closed proof let Y be Subset of REAL; assume Y in Z;
     then ex A being Element of bool REAL st Y = A & X c= A & A is closed;
    hence Y is closed;
   end;
     Cl X = meet Z by Def10;
  hence thesis by A1,Th31;
 end;
end;

theorem Th32:
 for Y being closed Subset of REAL st X c= Y holds Cl X c= Y
proof let Y be closed Subset of REAL; assume
A1: X c= Y;
   set ClX = { A where A is Element of bool REAL : X c= A & A is closed };
A2: Cl X = meet ClX by Def10;
     Y in ClX by A1;
 hence Cl X c= Y by A2,SETFAM_1:4;
end;

theorem Th33:
X c= Cl X
proof let x be set; assume
A1: x in X;
   set ClX = { A where A is Element of bool REAL : X c= A & A is closed };
A2: Cl X = meet ClX by Def10;
     REAL = [#]REAL by SUBSET_1:def 4;
then A3: [#]REAL in ClX by FCONT_3:1;
     now let Y be set; assume Y in ClX;
       then consider YY being Subset of REAL such that
   A4: YY = Y & X c= YY & YY is closed;
    thus x in Y by A1,A4;
   end;
 hence x in Cl X by A2,A3,SETFAM_1:def 1;
end;

theorem Th34:
X is closed iff X = Cl X
proof
 hereby assume
 A1: X is closed;
 A2: X c= Cl X by Th33;
    set ClX = { A where A is Element of bool REAL : X c= A & A is closed };
 A3: Cl X = meet ClX by Def10;
      X in ClX by A1;
    then Cl X c= X by A3,SETFAM_1:4;
 hence X = Cl X by A2,XBOOLE_0:def 10;
 end;
 thus thesis;
end;

theorem
   Cl ({}REAL) = {} by Th34,FCONT_3:3;

theorem
   Cl ([#]REAL) = REAL
proof REAL = [#]REAL by SUBSET_1:def 4;
 hence thesis by Th34,FCONT_3:1;
end;

theorem
  X c= Y implies Cl X c= Cl Y
proof assume
A1: X c= Y;
   Y c= Cl Y by Th33;
then A2: X c= Cl Y by A1,XBOOLE_1:1;
   set ClX = { A where A is Element of bool REAL : X c= A & A is closed };
A3: Cl X = meet ClX by Def10;
     Cl Y in ClX by A2;
 hence Cl X c= Cl Y by A3,SETFAM_1:4;
end;

theorem Th38:
r3 in Cl X iff for O being open Subset of REAL st r3 in
 O holds O /\ X is non empty
proof
 hereby assume
 A1: r3 in Cl X;
  let O be open Subset of REAL such that
 A2: r3 in O and
 A3: O /\ X is empty;
      O misses X by A3,XBOOLE_0:def 7;
 then A4: X c= O` by SUBSET_1:43;
      O` is closed by RCOMP_1:def 5;
then A5: Cl X c= O` by A4,Th32;
      O misses O` by SUBSET_1:44;
  hence contradiction by A1,A2,A5,XBOOLE_0:3;
 end; assume
A6: for O being open Subset of REAL st r3 in O holds O /\ X is non empty;
     (Cl X)`` = Cl X;
then A7: (Cl X)` is open by RCOMP_1:def 5;
A8: X c= Cl X by Th33;
     (Cl X)` /\ X c= X by XBOOLE_1:17;
   then (Cl X)` /\ X c= Cl X & (Cl X)` /\ X c= (Cl X)` by A8,XBOOLE_1:1,17;
 then (Cl X)` /\ X is empty by SUBSET_1:40;
   then not r3 in (Cl X)` by A6,A7;
 hence r3 in Cl X by SUBSET_1:50;
end;

theorem Th39:
r3 in Cl X implies ex seq st rng seq c= X & seq is convergent & lim seq = r3
proof assume
A1: r3 in Cl X;
    defpred P[set,set] means ex n being Nat st $1 = n &
     $2 = choose(X/\].r3-1/(n+1),r3+1/(n+1).[);
A2: now let x be set; assume x in NAT;
        then reconsider n = x as Nat;
        set n1 = n+1;
        set oi = ].r3-1/n1,r3+1/n1.[;
        reconsider u = choose(X/\oi) as set;
     take u;
         n1 > 0 by NAT_1:19;
         then 1/n1 > 0 by REAL_2:127;
     then A3: r3 < r3+1/n1 by REAL_1:69;
         then r3-1/n1 < r3 by REAL_1:84;
         then r3 in {p : r3-1/n1 < p & p < r3+1/n1 } by A3;
      then r3 in oi by RCOMP_1:def 2;
        then X/\oi is non empty by A1,Th38;
        then u in X/\oi;
     hence u in REAL;
     thus P[x,u];
    end;
 consider seq being Function such that
A4: dom seq = NAT and
A5: rng seq c= REAL and
A6: for x being set st x in NAT holds P[x,seq.x] from NonUniqBoundFuncEx(A2);
 reconsider seq as Real_Sequence by A4,A5,FUNCT_2:def 1,RELSET_1:11;
 take seq;
 thus rng seq c= X proof let y be set; assume y in rng seq;
    then consider x being set such that
 A7: x in dom seq & seq.x = y by FUNCT_1:def 5;
     consider n being Nat such that
 A8: x = n & seq.x = choose(X/\].r3-1/(n+1),r3+1/(n+1).[) by A4,A6,A7;
        set n1 = n+1;
        set oi = ].r3-1/n1,r3+1/n1.[;
          n1 > 0 by NAT_1:19;
         then 1/n1 > 0 by REAL_2:127;
     then A9: r3 < r3+1/n1 by REAL_1:69;
         then r3-1/n1 < r3 by REAL_1:84;
         then r3 in {p : r3-1/n1 < p & p < r3+1/n1 } by A9;
      then r3 in oi by RCOMP_1:def 2;
         then X/\oi is non empty by A1,Th38;
  hence y in X by A7,A8,XBOOLE_0:def 3;
 end;
A10: now let p be real number; assume
   A11: 0<p;
       set cp = [/ 1/p \];
     A12: 0 < 1/p by A11,REAL_2:127;
     A13: 1/p <= cp by INT_1:def 5;
     A14: 0 < cp by A12,INT_1:def 5;
       then reconsider cp as Nat by INT_1:16;
    take n = cp;
    let m be Nat such that
    A15: n<=m;
        consider m' being Nat such that
    A16: m' = m & seq.m = choose(X/\].r3-1/(m'+1),r3+1/(m'+1).[) by A6;
        set m1 = m+1;
        set oi = ].r3-1/m1,r3+1/m1.[;
          m1 > 0 by NAT_1:19;
         then 1/m1 > 0 by REAL_2:127;
     then A17: r3 < r3+1/m1 by REAL_1:69;
         then r3-1/m1 < r3 by REAL_1:84;
         then r3 in {q3 : r3-1/m1 < q3 & q3 < r3+1/m1 } by A17;
      then r3 in oi by RCOMP_1:def 2;
         then X/\oi is non empty by A1,Th38;
         then seq.m in oi by A16,XBOOLE_0:def 3;
         then seq.m in {q3 : r3-1/m1 < q3 & q3 < r3+1/m1 } by RCOMP_1:def 2;
         then consider s being Real such that
     A18: seq.m = s & r3-1/m1 < s & s < r3+1/m1;
           r3-1/m1 = r3+-1/m1 by XCMPLX_0:def 8;
         then -1/m1 < s-r3 & s-r3 < 1/m1 by A18,REAL_1:84,86;
     then A19: abs(s-r3) < 1/m1 by Th5;
     A20: n+1 > 0 by NAT_1:18;
           n+1 <= m+1 by A15,AXIOMS:24;
     then A21: 1/m1 <= 1/(n+1) by A20,REAL_2:152;
           n < n+1 by NAT_1:38;
     then A22: 1/(n+1) < 1/n by A14,REAL_2:151;
            1/(1/p) >= 1/cp by A12,A13,REAL_2:152;
          then 1/n <= p by XCMPLX_1:56;
         then 1/(n+1) < p by A22,AXIOMS:22;
         then 1/m1 < p by A21,AXIOMS:22;
    hence abs(seq.m-r3)<p by A18,A19,AXIOMS:22;
   end;
 hence seq is convergent by SEQ_2:def 6;
 hence lim seq = r3 by A10,SEQ_2:def 7;
end;

begin :: Functions into Reals

definition let X be set, f be Function of X, REAL;
 redefine attr f is bounded_below means
:Def11: f.:X is bounded_below;
  compatibility
   proof
A1:   dom f = X by FUNCT_2:def 1;
    thus f is bounded_below implies f.:X is bounded_below
     proof
      given r being real number such that
A2:    for y being set st y in dom f holds r<f.y;
      take r;
      let s be real number;
      assume s in f.:X;
       then consider x being set such that
A3:     x in X and
          x in X and
A4:     s = f.x by FUNCT_2:115;
      thus r<=s by A1,A2,A3,A4;
     end;
    given p being real number such that
A5:  for r being real number st r in f.:X holds p<=r;
    take p - 1;
    let y be set;
    assume y in dom f;
     then f.y in rng f by FUNCT_1:12;
     then f.y in f.:X by PARTFUN1:51;
     then A6:    p <= f.y by A5;
       f.y < f.y + 1 by REAL_1:69;
     then p < f.y + 1 by A6,AXIOMS:22;
    hence p-1 < f.y by REAL_1:84;
   end;
 attr f is bounded_above means
:Def12:  f.:X is bounded_above;
  compatibility
   proof
A7:   dom f = X by FUNCT_2:def 1;
    thus f is bounded_above implies f.:X is bounded_above
     proof
      given r being real number such that
A8:    for y being set st y in dom f holds r>f.y;
      take r;
      let s be real number;
      assume s in f.:X;
       then consider x being set such that
A9:     x in X and
          x in X and
A10:     s = f.x by FUNCT_2:115;
      thus r>=s by A7,A8,A9,A10;
     end;
    given p being real number such that
A11:  for r being real number st r in f.:X holds p>=r;
    take p + 1;
    let y be set;
    assume y in dom f;
     then f.y in rng f by FUNCT_1:12;
     then f.y in f.:X by PARTFUN1:51;
     then p >= f.y by A11;
     then A12:    p+1 >= f.y+1 by AXIOMS:24;
       f.y < f.y + 1 by REAL_1:69;
    hence p+1 > f.y by A12,AXIOMS:22;
   end;
end;

definition let X be set, f be Function of X, REAL;
 canceled;

 attr f is with_max means
:Def14: f.:X is with_max;
 attr f is with_min means
:Def15: f.:X is with_min;
end;

definition let X be set, f be Function of X, REAL;
 func -f -> Function of X, REAL means
:Def16: for p being set st p in X holds it.p = -(f.p);
 existence proof
  deffunc F(set) = -(f.$1);
A1: for x being set st x in X holds F(x) in REAL;
  thus ex g be Function of X, REAL st for x be set st x in X holds g.x = F(x)
   from Lambda1(A1);
 end;
 uniqueness proof let g1, g2 be Function of X, REAL such that
A2:  for p being set st p in X holds g1.p = -(f.p) and
A3:  for p being set st p in X holds g2.p = -(f.p);
     now let p be set; assume
A4:   p in X;
    hence g1.p = -(f.p) by A2 .= g2.p by A3,A4;
   end;
   hence thesis by FUNCT_2:18;
  end;
 involutiveness
  proof let IT,f be Function of X, REAL;
   assume
A5:  for p being set st p in X holds IT.p = -(f.p);
   let p be set;
   assume
A6:  p in X;
   thus f.p = -(-(f.p))
      .= -(IT.p) by A5,A6;
  end;
end;

theorem Th40:
 for X, A being set, f being Function of X, REAL holds (-f).:A = -(f.:A)
proof let X, A be set, f be Function of X, REAL;
    now let x be set;
   hereby assume
        x in (-f).:A; then consider x1 being set such that
   A1: x1 in X & x1 in A & x = (-f).x1 by FUNCT_2:115;
   A2: x = -(f.x1) by A1,Def16;
        f.x1 in f.:A by A1,FUNCT_2:43;
      then -(f.x1) in { -r3 : r3 in f.:A };
     hence x in -(f.:A) by A2,Def7;
   end; assume x in -(f.:A);
     then x in { -r3 : r3 in f.:A } by Def7; then consider r3 such that
  A3: x = -r3 & r3 in f.:A;
     consider x1 being set such that
  A4: x1 in X & x1 in A & r3 = f.x1 by A3,FUNCT_2:115;
       x = (-f).x1 by A3,A4,Def16;
  hence x in (-f).:A by A4,FUNCT_2:43;
 end;
 hence (-f).:A = -(f.:A) by TARSKI:2;
end;

Lm7:
for X being non empty set, f being Function of X, REAL
 st f is with_max holds -f is with_min
proof let X be non empty set, f be Function of X, REAL; assume that
A1: f.:X is bounded_above and
A2: sup (f.:X) in f.:X;
A3: -(f.:X) = (-f).:X by Th40;
 hence A4: (-f).:X is bounded_below by A1,Lm1;
A5: - sup (f.:X) in -(f.:X) by A2,Th14;
     inf ((-f).:X) = - sup --(f.:X) by A3,A4,Th17
                  .= - sup (f.:X);
 hence inf ((-f).:X) in (-f).:X by A5,Th40;
end;

Lm8:
for X being non empty set, f being Function of X, REAL
 st f is with_min holds -f is with_max
proof let X be non empty set, f be Function of X, REAL; assume that
A1: f.:X is bounded_below and
A2: inf (f.:X) in f.:X;
A3: -(f.:X) = (-f).:X by Th40;
 hence A4: (-f).:X is bounded_above by A1,Lm2;
A5: - inf (f.:X) in -(f.:X) by A2,Th14;
     sup ((-f).:X) = - inf --(f.:X) by A3,A4,Th18
                  .= - inf (f.:X);
 hence sup ((-f).:X) in (-f).:X by A5,Th40;
end;

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

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

theorem Th43:
for X being set, A being Subset of REAL, f being Function of X, REAL
 holds (-f)"A = f"(-A)
proof let X be set, A be Subset of REAL, f be Function of X, REAL;
    now let x be set;
   hereby assume A1: x in (-f)"A;
  then A2: x in X & (-f).x in A by FUNCT_2:46;
    (-f).x = -(f.x) by A1,Def16;
     then --f.x in -A by A2,Th14;
    hence x in f"(-A) by A1,FUNCT_2:46;
   end; assume A3: x in f"(-A);
  then A4: x in X & f.x in -A by FUNCT_2:46;
    (-f).x = -(f.x) by A3,Def16;
     then (-f).x in --A by A4,Th14;
   hence x in (-f)"A by A3,FUNCT_2:46;
  end;
 hence (-f)"A = f"(-A) by TARSKI:2;
end;

definition let X be set, r be Real, f be Function of X, REAL;
 func r+f -> Function of X, REAL means
:Def17: for p being set st p in X holds it.p = r+f.p;
 existence proof
  deffunc F(set) = r+f.$1;
A1: for x being set st x in X holds F(x) in REAL;
  thus ex g be Function of X, REAL st for x be set st x in X holds g.x = F(x)
   from Lambda1(A1);
 end;
 uniqueness proof let g1, g2 be Function of X, REAL such that
A2:  for p being set st p in X holds g1.p = r+f.p and
A3:  for p being set st p in X holds g2.p = r+f.p;
     now let p be set; assume
A4:   p in X;
    hence g1.p = r+f.p by A2
              .= g2.p by A3,A4;
   end;
   hence thesis by FUNCT_2:18;
  end;
end;

theorem
   for X, A being set, f being Function of X, REAL, s being Real
  holds (s+f).:A = s+(f.:A)
proof let X, A be set, f be Function of X, REAL, s be Real;
    now let x be set;
   hereby assume
        x in (s+f).:A; then consider x1 being set such that
   A1: x1 in X & x1 in A & x = (s+f).x1 by FUNCT_2:115;
   A2: x = s+(f.x1) by A1,Def17;
        f.x1 in f.:A by A1,FUNCT_2:43;
      then s+(f.x1) in { s+r3 : r3 in f.:A };
     hence x in s+(f.:A) by A2,Def8;
   end; assume x in s+(f.:A);
     then x in { s+r3 : r3 in f.:A } by Def8; then consider r3 such that
  A3: x = s+r3 & r3 in f.:A;
     consider x1 being set such that
  A4: x1 in X & x1 in A & r3 = f.x1 by A3,FUNCT_2:115;
       x = (s+f).x1 by A3,A4,Def17;
  hence x in (s+f).:A by A4,FUNCT_2:43;
 end;
 hence (s+f).:A = s+(f.:A) by TARSKI:2;
end;

theorem Th45:
for X being set, A being Subset of REAL, f being Function of X, REAL, q3
 holds (q3+f)"A = f"(-q3+A)
proof let X be set, A be Subset of REAL, f be Function of X, REAL, q3 be Real;
    now let x be set;
   hereby assume A1: x in (q3+f)"A;
  then A2: x in X & (q3+f).x in A by FUNCT_2:46;
    (q3+f).x = q3+(f.x) by A1,Def17;
     then -q3+(q3+(f.x)) in -q3+A by A2,Th20;
     then f.x in -q3+A by XCMPLX_1:137;
    hence x in f"(-q3+A) by A1,FUNCT_2:46;
   end; assume A3: x in f"(-q3+A);
  then A4: x in X & f.x in -q3+A by FUNCT_2:46;
    (q3+f).x = q3+(f.x) by A3,Def17;
     then (q3+f).x in q3+(-q3+A) by A4,Th20;
     then (q3+f).x in (q3+-q3)+A by Th22;
     then (q3+f).x in 0+A by XCMPLX_0:def 6;
     then (q3+f).x in A by Th21;
   hence x in (q3+f)"A by A3,FUNCT_2:46;
  end;
 hence (q3+f)"A = f"(-q3+A) by TARSKI:2;
end;

definition let X be set, f be Function of X, REAL;
 func Inv f -> Function of X, REAL means
:Def18: for p being set st p in X holds it.p = 1/(f.p);
 existence proof
  deffunc F(set) = 1/(f.$1);
A1: for x being set st x in X holds F(x) in REAL;
  thus ex g be Function of X, REAL st for x be set st x in X holds g.x = F(x)
   from Lambda1(A1);
 end;
 uniqueness proof let g1, g2 be Function of X, REAL such that
A2:  for p being set st p in X holds g1.p = 1/f.p and
A3:  for p being set st p in X holds g2.p = 1/f.p;
     now let p be set; assume
A4:   p in X;
    hence g1.p = 1/f.p by A2
              .= g2.p by A3,A4;
   end;
   hence thesis by FUNCT_2:18;
  end;
 involutiveness
  proof let IT,f be Function of X, REAL;
   assume
A5:  for p being set st p in X holds IT.p = 1/(f.p);
   let p be set;
   assume
A6:  p in X;
   thus f.p = (f.p)""
         .= (1/(f.p))" by XCMPLX_1:217
         .= 1/(1/(f.p)) by XCMPLX_1:217
         .= 1/(IT.p) by A5,A6;
  end;
end;

theorem Th46:
for X being set, A being without_zero Subset of REAL,
    f being Function of X, REAL holds (Inv f)"A = f"(Inv A)
proof let X be set, A be without_zero Subset of REAL,
          f be Function of X, REAL;
    now let x be set;
   hereby assume A1: x in (Inv f)"A;
  then A2: x in X & (Inv f).x in A by FUNCT_2:46;
    (Inv f).x = 1/(f.x) by A1,Def18;
  then 1/(1/(f.x)) in Inv A by A2,Th28;
     then f.x in Inv A by XCMPLX_1:56;
    hence x in f"(Inv A) by A1,FUNCT_2:46;
   end; assume A3: x in f"(Inv A);
  then A4: x in X & f.x in Inv A by FUNCT_2:46;
    (Inv f).x = 1/(f.x) by A3,Def18;
     then (Inv f).x in Inv Inv A by A4,Th28;
     then (Inv f).x in A by Th29;
   hence x in (Inv f)"A by A3,FUNCT_2:46;
  end;
 hence (Inv f)"A = f"(Inv A) by TARSKI:2;
end;

begin :: Real maps

definition let T be 1-sorted;
 mode RealMap of T is Function of the carrier of T, REAL;
 canceled;
end;

definition let T be non empty 1-sorted;
 cluster bounded RealMap of T;
 existence proof set c = (the carrier of T);
  reconsider f = c --> (0 qua Real) as RealMap of T;
  take f;
A1: dom f = c by FUNCT_2:def 1;
    rng f = {0 qua Real} by FUNCOP_1:14;
  then f.:c = {0 qua Real} by A1,RELAT_1:146;
then A2: f.:c is bounded by SEQ_4:15;
  hence f.:c is bounded_above by SEQ_4:def 3;
  thus f.:c is bounded_below by A2,SEQ_4:def 3;
 end;
end;

scheme NonUniqExRF{X() -> non empty TopStruct, P[set,set]}:
  ex f being RealMap of X() st
    for x being Element of X() holds P[x, f.x]
provided
A1: for x being set st x in the carrier of X() ex r3 st P[x, r3]
proof
  defpred Q[set,set] means P[$1,$2];
A2: for x being set st x in the carrier of X()
     ex y being set st y in REAL & Q[x,y]
   proof let x be set;
    assume x in the carrier of X();
    then ex r3 st P[x, r3] by A1;
    hence thesis;
   end;
  consider f being Function of the carrier of X(),REAL such that
A3: for x being set st x in the carrier of X() holds Q[x,f.x]
   from FuncEx1(A2);
  reconsider f as RealMap of X();
  take f;
  thus thesis by A3;
 end;

scheme LambdaRF{X() -> non empty TopStruct, F(set) -> Real}:
ex f being RealMap of X() st
 for x being Element of X() holds f.x = F(x)
proof
  defpred P[set,set] means $2 = F($1);
A1: for x being set st x in the carrier of X() ex r3 st P[x,r3];
  thus ex f be RealMap of X() st for x be Element of X() holds
   P[x,f.x] from NonUniqExRF(A1);
 end;

definition let T be 1-sorted, f be RealMap of T, P be set;
 redefine func f"P -> Subset of T;
 coherence proof
   thus f"P is Subset of T;
 end;
end;

definition let T be 1-sorted, f be RealMap of T;
 func inf f -> Real equals
:Def20: inf (f.:the carrier of T);
 coherence;
 func sup f -> Real equals
:Def21: sup (f.:the carrier of T);
 coherence;
end;

theorem Th47:
for T being non empty TopSpace, f being bounded_below RealMap of T
 for p being Point of T holds f.p >= inf f
proof let T be non empty TopSpace, f be bounded_below RealMap of T;
  set fc = (f.:the carrier of T);
A1: inf f = inf fc by Def20;
A2: fc is bounded_below by Def11;
  set r = inf f;
  let p be Point of T;
      f.p in fc by FUNCT_2:43;
   hence f.p >= r by A1,A2,SEQ_4:def 5;
end;

theorem
  for T being non empty TopSpace, f being bounded_below RealMap of T
 for s being Real st for t being Point of T holds f.t >= s holds inf 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);
A1: inf f = inf fc by Def20;
  set r = inf f;
  let s be Real; assume
  A2: for t being Point of T holds f.t >= s;
       now let p1 be real number; assume p1 in fc;
        then consider x being set such that
     A3: x in c & x in c & p1 = f.x by FUNCT_2:115;
      thus p1 >= s by A2,A3;
     end;
  hence r >= s by A1,Th8;
end;

theorem
  for T being non empty TopSpace, f being RealMap of T
  st (for p being Point of T holds f.p >= r) &
   for t st for p being Point of T holds f.p >= t holds r >= t
 holds r = inf 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 being Point of T holds f.p >= r and
A2: for t st for p being Point of T holds f.p >= t
       holds r >= t;
A3: inf f = inf fc by Def20;
A4: now let s; assume s in fc;
        then consider x being set such that
     A5: x in c & x in c & s = f.x by FUNCT_2:115;
    thus s >= r by A1,A5;
   end;
     now let t; assume
   A6: for s st s in fc holds s >= t;
        now let s be Point of T;
          f.s in fc by FUNCT_2:43;
       hence f.s >= t by A6;
      end;
    hence r >= t by A2;
   end;
 hence r = inf f by A3,A4,Th9;
end;

theorem Th50:
for T being non empty TopSpace, f being bounded_above RealMap of T
 for p being Point of T holds f.p <= sup f
proof let T be non empty TopSpace, f be bounded_above RealMap of T;
   set fc = (f.:the carrier of T);
A1: sup f = sup fc by Def21;
A2: fc is bounded_above by Def12;
 set r = sup f;
 let p be Point of T;
      f.p in fc by FUNCT_2:43;
   hence f.p <= r by A1,A2,SEQ_4:def 4;
end;

theorem
  for T being non empty TopSpace, f being bounded_above RealMap of T
 for t st for p being Point of T holds f.p <= t holds sup 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);
A1: sup f = sup fc by Def21;
 set r = sup f;
  let t; assume
  A2: for p being Point of T holds f.p <= t;
       now let s; assume s in fc;
        then consider x being set such that
     A3: x in c & x in c & s = f.x by FUNCT_2:115;
      thus s <= t by A2,A3;
     end;
  hence r <= t by A1,Th10;
end;

theorem
  for T being non empty TopSpace, f being RealMap of T
   st (for p being Point of T holds f.p <= r) &
      (for t st for p being Point of T holds f.p <= t holds r <= t)
 holds r = sup 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);
A1: sup f = sup fc by Def21;
  assume that
A2: for p being Point of T holds f.p <= r and
A3: for t st for p being Point of T holds f.p <= t holds r <= t;
A4: now let s; assume s in fc;
        then consider x being set such that
     A5: x in c & x in c & s = f.x by FUNCT_2:115;
    thus s <= r by A2,A5;
   end;
     now let t; assume
   A6: for s st s in fc holds s <= t;
        now let s be Point of T;
          f.s in fc by FUNCT_2:43;
       hence f.s <= t by A6;
      end;
    hence r <= t by A3;
   end;
 hence r = sup f by A1,A4,Th11;
end;

theorem Th53:
 for T being non empty 1-sorted, f being bounded RealMap of T
  holds inf f <= sup 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 Def11,Def12;
   then f.:the carrier of T is bounded by SEQ_4:def 3;
   then inf (f.:the carrier of T) <= sup (f.:the carrier of T) by SEQ_4:24;
   then inf f <= sup (f.:the carrier of T) by Def20;
 hence inf f <= sup f by Def21;
end;

definition
 canceled 3;
end;

definition let T be TopStruct, f be RealMap of T;
 attr f is continuous means
:Def25: for Y being Subset of REAL st Y is closed holds f"Y is closed;
end;

definition let T be non empty TopSpace;
 cluster continuous RealMap of T;
 existence proof set c = (the carrier of T);
  reconsider f = c --> (0 qua Real) as RealMap of T;
  take f;
A1: dom f = c by FUNCT_2:def 1;
A2: rng f = {0 qua Real} by FUNCOP_1:14;
  let Y be Subset of REAL; assume Y is closed;
  per cases;
  suppose 0 in Y;
  then A3: rng f c= Y by A2,ZFMISC_1:37;
        f"Y = f"(rng f /\ Y) by RELAT_1:168
         .= f"rng f by A3,XBOOLE_1:28
         .= c by A1,RELAT_1:169
         .= [#]T by PRE_TOPC:12;
   hence f"Y is closed;
  suppose not 0 in Y;
then A4:    rng f misses Y by A2,ZFMISC_1:56;
        f"Y = f"(rng f /\ Y) by RELAT_1:168
         .= f"{} by A4,XBOOLE_0:def 7
         .= {}T by RELAT_1:171;
   hence f"Y is closed by TOPS_1:22;
 end;
end;

definition let T be non empty TopSpace, S be non empty SubSpace of T;
 cluster continuous RealMap of S;
 existence proof set c = (the carrier of S);
  reconsider f = c --> (0 qua Real) as RealMap of S;
  take f;
A1: dom f = c by FUNCT_2:def 1;
A2: rng f = {0 qua Real} by FUNCOP_1:14;
  let Y be Subset of REAL; assume Y is closed;
  per cases;
  suppose 0 in Y;
  then A3: rng f c= Y by A2,ZFMISC_1:37;
        f"Y = f"(rng f /\ Y) by RELAT_1:168
         .= f"rng f by A3,XBOOLE_1:28
         .= c by A1,RELAT_1:169
         .= [#]S by PRE_TOPC:12;
   hence f"Y is closed;
  suppose not 0 in Y;
then A4:    rng f misses Y by A2,ZFMISC_1:56;
        f"Y = f"(rng f /\ Y) by RELAT_1:168
         .= f"{} by A4,XBOOLE_0:def 7
         .= {}S by RELAT_1:171;
   hence f"Y is closed by TOPS_1:22;
 end;
end;

 reserve T for TopStruct,
         f for RealMap of T;

theorem Th54:
f is continuous iff for Y being 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 by RCOMP_1:def 5;
then A2: f"(Y`) is closed by A1,Def25;
      f"(Y`) = f"(REAL \ Y) by SUBSET_1:def 5
          .= (f"REAL) \ f"(Y) by FUNCT_1:138
          .= (the carrier of T) \ f"Y by FUNCT_2:48
          .= ([#]T) \ f"Y by PRE_TOPC:def 3;
    then ([#]T) \ (([#]T) \ f"(Y)) is open by A2,PRE_TOPC:def 6;
  hence f"Y is open by PRE_TOPC:22;
 end; assume
A3: for Y being Subset of REAL st Y is open holds f"Y is open;
 let Y be Subset of REAL; assume
A4: Y is closed;
      Y = Y``;
    then Y` is open by A4,RCOMP_1:def 5;
then A5: f"(Y`) is open by A3;
      f"(Y`) = f"(REAL \ Y) by SUBSET_1:def 5
          .= (f"REAL) \ f"(Y) by FUNCT_1:138
          .= (the carrier of T) \ f"Y by FUNCT_2:48
          .= ([#]T) \ f"Y by PRE_TOPC:def 3;
 hence f"Y is closed by A5,PRE_TOPC:def 6;
end;

theorem Th55:
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 Th19;
  (-f)"X = f"(-X) by Th43;
 hence (-f)"X is closed by A1,A2,Def25;
end;

theorem Th56:
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 Th27;
  (r3+f)"X = f"(-r3+X) by Th45;
 hence (r3+f)"X is closed by A1,A2,Def25;
end;

theorem Th57:
 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; assume
A3: X0 is closed;
     0 in {0} by TARSKI:def 1;
then A4: not 0 in X0\{0} by XBOOLE_0:def 4;
A5: X0\{0} c= X0 by XBOOLE_1:36;
   reconsider X = X0\{0} as without_zero Subset of REAL by A4,Def1;
   set X' = Inv X;
   set X'r = X'/\rng f;
     now let x be set;
    hereby assume
    A6: x in X'r;
          X'r c= Cl X'r by Th33;
        then x in Cl X'r & x in rng f by A6,XBOOLE_0:def 3;
     hence x in (Cl X'r) /\ rng f by XBOOLE_0:def 3;
    end; assume A7: x in (Cl X'r) /\ rng f;
    then A8: x in Cl (X'r) & x in rng f by XBOOLE_0:def 3;
      reconsider s = x as Real by A7;
      consider seq being Real_Sequence such that
    A9: rng seq c= X'r and
    A10: seq is convergent and
    A11: lim seq = s by A8,Th39;
        assume not x in X'r;
    then A12: not x in X' by A8,XBOOLE_0:def 3;
          now assume
        A13: lim seq <> 0;
              now let n be Nat; assume seq.n = 0;
              then 0 in rng seq by FUNCT_2:6;
             hence contradiction by A2,A9,XBOOLE_0:def 3;
            end;
        then A14: seq is_not_0 by SEQ_1:7;
        then A15: seq" is convergent by A10,A13,SEQ_2:35;
        A16: lim (seq") = (lim seq)" by A10,A13,A14,SEQ_2:36;
              rng (seq") c= X proof let y be set; assume
                  y in rng (seq");
              then consider n being set such that
            A17: n in dom (seq") & y = (seq").n by FUNCT_1:def 5;
                reconsider n as Nat by A17,FUNCT_2:def 1;
                  seq.n in rng seq by FUNCT_2:6;
                then seq.n in X' by A9,XBOOLE_0:def 3;
then A18:            1/(1/seq.n) in X' by XCMPLX_1:56;
                   (seq").n = (seq.n)" by SEQ_1:def 8
                        .= 1/(seq.n) by XCMPLX_1:217;
             hence y in X by A17,A18,Th28;
            end;
            then rng (seq") c= X0 by A5,XBOOLE_1:1;
        then A19: lim (seq") in X0 by A3,A15,RCOMP_1:def 4;
              (lim seq)" = 1/(lim seq) by XCMPLX_1:217;
            then lim (seq") <> 0 by A13,A16,XCMPLX_1:62;
            then not lim (seq") in {0} by TARSKI:def 1;
            then lim (seq") in X by A19,XBOOLE_0:def 4;
            then 1/(lim (seq")) in X' by Th28;
         hence contradiction by A11,A12,A16,XCMPLX_1:218;
        end;
    hence contradiction by A2,A7,A11,XBOOLE_0:def 3;
   end;
then A20: X'r = (Cl X'r) /\ rng f by TARSKI:2;
     f"(Cl X'r) is closed by A1,Def25;
then A21: f"X'r is closed by A20,RELAT_1:168;
A22: f"X' = f"X'r by RELAT_1:168;
A24: (Inv f)"X = f"(Inv X) by Th46;
      now let x be set;
     hereby assume
   A25: x in (Inv f)"X0;
then A26:     x in the carrier of T & (Inv f).x in X0 by FUNCT_2:46;
         now assume not (Inv f).x in X;
         then (Inv f).x in {0} by A26,XBOOLE_0:def 4;
         then (Inv f).x = 0 by TARSKI:def 1;
       then A27: 1/(f.x) = 0 by A25,Def18;
             f.x in rng f by A25,FUNCT_2:6;
        hence contradiction by A2,A27,XCMPLX_1:62;
       end;
      hence x in (Inv f)"X by A25,FUNCT_2:46;
     end;
       X c= X0 by XBOOLE_1:36;
     then (Inv f)"X c= (Inv f)"X0 by RELAT_1:178;
     hence x in (Inv f)"X implies x in (Inv f)"X0;
    end;
 hence (Inv f)"X0 is closed by A21,A22,A24,TARSKI:2;
end;

definition let X, Y be set, f be Function of bool X, bool Y;
           let R be Subset-Family of X;
  redefine func f.:R -> Subset-Family of Y;
  coherence
  proof
      f.:R c= bool Y;
    hence thesis by SETFAM_1:def 7;
  end;
end;

theorem
  for R being 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 being set such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = ("f).eR by FUNCT_2:115;
A6: P = f"eR by A3,A5,Def2;
   reconsider eR as Subset of REAL by A3;
     eR is open by A2,A4,Def5;
 hence P is open by A1,A6,Th54;
end;

theorem Th59:
for R being 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 being set such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = ("f).eR by FUNCT_2:115;
A6: P = f"eR by A3,A5,Def2;
   reconsider eR as Subset of REAL by A3;
     eR is closed by A2,A4,Def6;
 hence P is closed by A1,A6,Def25;
end;

definition let T be non empty TopStruct, X be Subset of T,
               f be RealMap of T;
 func f||X -> RealMap of T|X equals
:Def26: f|X;
 coherence proof
     the carrier of (T|X) = X by JORDAN1:1;
:::   then f|X is Function of the carrier of (T|X), REAL by FUNCT_2:38;
  hence thesis by FUNCT_2:38;
 end;
end;

definition let T be non empty TopSpace;
 cluster compact non empty Subset of T;
 existence proof
  consider x being Point of T;
  take {x};
  thus thesis by BORSUK_1:41;
 end;
end;

definition 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 Th54;
  A2: the carrier of (T|X) = X by JORDAN1:1;
       (f||X)"Y = (f|X)"Y by Def26 .= X/\(f"Y) by FUNCT_1:139;
   hence (f||X)"Y is open by A1,A2,TSP_1:def 1;
  end;
  hence thesis by Th54;
 end;
end;

definition let T be non empty TopSpace, P be compact non empty Subset of T;
 cluster T|P -> compact;
 coherence by COMPTS_1:12;
end;

begin :: Pseudocompact spaces

theorem Th60:
 for T being non empty TopSpace
  holds
   (for f being RealMap of T st f is continuous holds f is with_max)
 iff
   (for f being RealMap of T st f is continuous holds f is with_min)
proof let T be non empty TopSpace;
 hereby assume
A1: for f being 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 Th55;
then A2: -f is with_max by A1;
  thus f is with_min by Th41,A2;
 end;
 assume
A3: for f being 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 Th55;
then A4: -f is with_min by A3;
   reconsider Xf = f as Function of the carrier of T, REAL;
   --Xf is with_max by Lm8,A4;
  hence f is with_max;
end;

theorem Th61:
for T being non empty TopSpace
  holds
   (for f being RealMap of T st f is continuous holds f is bounded)
 iff
   (for f being 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 being 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 f is bounded_above by SEQ_2:def 5;
 then A3: fcT is bounded_above by Def12;
  assume
      not f is with_max; then A4: not fcT is with_max by Def14;
 then A5: not sup (fcT) in fcT by A3,Def3;
    set b = sup fcT;
    set bf = b+-f; set g = Inv bf;
    reconsider f' = f as Function of cT, REAL;
    reconsider bf' = bf as Function of cT, REAL;
A7: now assume 0 in rng bf; then consider x being set such that
    A8: x in dom bf and
    A9: bf.x = 0 by FUNCT_1:def 5;
           dom bf = cT & dom f = cT by FUNCT_2:def 1;
    then A10: f.x in fcT by A8,FUNCT_2:43;
        reconsider x as Element of cT by A8,FUNCT_2:def 1;
          bf'.x = b+(-f').x by Def17
             .= b+-(f.x) by Def16
             .= b-f.x by XCMPLX_0:def 8;
     hence contradiction by A5,A9,A10,XCMPLX_1:15;
    end;
    set gcT = g.:cT;
      -f is continuous by A2,Th55;
    then bf is continuous by Th56;
 then A11: g is continuous by A7,Th57;
      now
        g is bounded by A1,A11; then g is bounded_above by SEQ_2:def 5;
      then gcT is bounded_above by Def12;
      then consider p be real number such that
    A12: for r be real number st r in gcT holds r <= p by SEQ_4:def 1;
    per cases;
     suppose A13: p <= 0;
      reconsider 1' = 1 as real number;
      take 1';
      thus 1' > 0;
      let r be real number; assume r in gcT; then r <= p by A12;
      hence r <= 1' by A13,AXIOMS:22;
     suppose A14: p > 0;
      take p;
      thus p>0 by A14;
      thus for r be real number st r in gcT holds r <= p by A12;
    end;
    then consider p be real number such that
 A15: p > 0 and
 A16:  for r be real number st r in gcT holds r <= p;
   1/p > 0 by A15,REAL_2:127;
    then consider r be real number such that
A17: r in fcT and
A18: b-1/p < r by A3,SEQ_4:def 4;
    consider x being set such that
A19: x in the carrier of T & x in the carrier of T and
A20:  r = f.x by A17,FUNCT_2:115;
    reconsider x as Element of T by A19;
      f.x <= b & f.x <> b by A3,A4,A17,A20,Def3,SEQ_4:def 4;
    then f.x+0 < b by REAL_1:def 5;
then A21: b-f.x > 0 by REAL_1:86;
 A22: g.x = 1/(bf'.x) by Def18
       .= 1/(b+(-f').x) by Def17
       .= 1/(b+-(f.x)) by Def16
       .= 1/(b-f.x) by XCMPLX_0:def 8;
      g.x in gcT by FUNCT_2:43;
    then 1/(b-f.x) <= p by A16,A22;
    then 1 <= p*(b-f.x) by A21,REAL_2:178;
    then 1/p <= b-f.x by A15,REAL_2:177;
    then f.x+1/p <= b by REAL_1:84;
  hence contradiction by A18,A20,REAL_1:84;
 end; assume
A23: for f being RealMap of T st f is continuous holds f is with_max;
 let f be RealMap of T; assume
A24: f is continuous;
   then f is with_max by A23;
   then f.:(the carrier of T) is with_max by Def14;
   then f.:(the carrier of T) is bounded_above by Def3;
 hence f is bounded_above by Def12;
     f is with_min by A23,A24,Th60;
   then f.:(the carrier of T) is with_min by Def15;
   then f.:(the carrier of T) is bounded_below by Def4;
 hence f is bounded_below by Def11;
end;

definition let T be TopStruct;
 attr T is pseudocompact means
:Def27:
 for f being RealMap of T st f is continuous holds f is bounded;
end;

definition
 cluster compact -> pseudocompact (non empty TopSpace);
 coherence proof let T be non empty TopSpace;
  assume that
A1: T is compact;
  let f be RealMap of T such that
A2: f is continuous;
  thus f is bounded_above
  proof
  assume
A3: for s be real number ex r be real number
       st r in f.:(the carrier of T) & r > s;
    consider p being Element of T;
    defpred P[Real] means $1 >= f.p;
    deffunc F(Real) = right_closed_halfline($1);
    set R = {F(r3) : P[r3]};
A4: R is Subset of bool REAL from SubsetFD;
A5: right_closed_halfline(f.p) in R;
    then reconsider R as non empty Subset-Family of REAL by A4,SETFAM_1:def 7;
    reconsider F = ("f).:R as Subset-Family of T;
A6: ("f).right_closed_halfline(f.p) in F by A5,FUNCT_2:43;
      now assume {} in F; then consider rchx being set such that
    A7: rchx in bool REAL and
    A8: rchx in R and
    A9: {} = ("f).rchx by FUNCT_2:115;
        consider r3 being Real such that
    A10: rchx = right_closed_halfline(r3) & r3 >= f.p by A8;
    A11: {} = f"rchx by A7,A9,Def2;
        consider r1 being real number such that
    A12: r1 in f.:(the carrier of T) and
    A13: r1 > r3 by A3;
        consider c being set such that
    A14: c in the carrier of T & c in the carrier of T and
    A15: r1 = f.c by A12,FUNCT_2:115;
A16:  r1 is Real by XREAL_0:def 1;
          rchx = {g where g is Real : g >= r3} by A10,LIMFUNC1:def 2;
        then r1 in rchx by A13,A16;
     hence contradiction by A11,A14,A15,FUNCT_2:46;
    end;
then A17: F is with_non-empty_elements by AMI_1:def 1;
      F is c=-linear proof let X,Y be set;
     assume X in F;
        then consider A being set such that
    A18: A in bool REAL and
    A19: A in R and
    A20: X = ("f).A by FUNCT_2:115;
        consider r1 such that
    A21: A = right_closed_halfline(r1) and r1 >= f.p by A19;
     assume Y in F;
        then consider B being set such that
    A22: B in bool REAL and
    A23: B in R and
    A24: Y = ("f).B by FUNCT_2:115;
        consider r2 such that
    A25: B = right_closed_halfline(r2) and r2 >= f.p by A23;
          r1 >= r2 or r2 >= r1;
    then A26: A c= B or B c= A by A21,A25,LIMFUNC1:9;
          X = f"A & Y = f"B by A18,A20,A22,A24,Def2;
     then X c= Y or Y c= X by A26,RELAT_1:178;
     hence thesis by XBOOLE_0:def 9;
    end;
then A27: F is centered by A6,A17,Th1;
      R is closed proof let X be Subset of REAL;
     assume X in R;
        then ex r3 st X = right_closed_halfline(r3) & r3 >= f.p;
     hence X is closed by FCONT_3:5;
    end;
    then F is closed by A2,Th59;
    then meet F <> {} by A1,A27,COMPTS_1:13;
    then consider x being set such that
A28:  x in meet F by XBOOLE_0:def 1;
    reconsider x as Element of T by A28;
A29: f.x in meet R by A28,Th2;
    consider eR being Element of R;
A30: f.x in eR by A29,SETFAM_1:def 1;
      eR in R; then consider er being Real such that
A31: eR = right_closed_halfline(er) & er >= f.p;
      right_closed_halfline(er) = {r3:r3>=er} by LIMFUNC1:def 2;
    then consider r1 being Real such that
A32: f.x = r1 & r1 >= er by A30,A31;
A33: f.x >= f.p by A31,A32,AXIOMS:22;
    consider fx' being real number such that
A34:  fx' > f.x by REAL_1:76;
    reconsider fx' as Real by XREAL_0:def 1;
      fx' >= f.p by A33,A34,AXIOMS:22;
    then right_closed_halfline(fx') in R;
then A35:  f.x in right_closed_halfline(fx') by A29,SETFAM_1:def 1;
      right_closed_halfline(fx') = {r3:r3>=fx'} by LIMFUNC1:def 2;
    then ex r3 st f.x = r3 & r3 >= fx' by A35;
  hence contradiction by A34;
  end;
  assume
A36: for s be real number ex r3 be real number st
      r3 in f.:(the carrier of T) & r3 < s;
    consider p being Element of T;
    defpred P[Real] means $1 <= f.p;
    deffunc F(Real) = left_closed_halfline($1);
    set R = {F(r3): P[r3]};
A37: R is Subset of bool REAL from SubsetFD;
A38: left_closed_halfline(f.p) in R;
    then reconsider R as non empty Subset-Family of REAL by A37,SETFAM_1:def 7;
    reconsider F = ("f).:R as Subset-Family of T;
    A39: ("f).left_closed_halfline(f.p) in F by A38,FUNCT_2:43;
      now assume {} in F; then consider rchx being set such that
    A40: rchx in bool REAL and
    A41: rchx in R and
    A42: {} = ("f).rchx by FUNCT_2:115;
        consider r3 being Real such that
    A43: rchx = left_closed_halfline(r3) & r3 <= f.p by A41;
    A44: {} = f"rchx by A40,A42,Def2;
        consider r1 being real number such that
    A45: r1 in f.:(the carrier of T) and
    A46: r1 < r3 by A36;
        consider c being set such that
    A47: c in the carrier of T & c in the carrier of T and
    A48: r1 = f.c by A45,FUNCT_2:115;
A49:  r1 is Real by XREAL_0:def 1;
          rchx = {g where g is Real : g <= r3} by A43,LIMFUNC1:def 1;
        then r1 in rchx by A46,A49;
     hence contradiction by A44,A47,A48,FUNCT_2:46;
    end;
then A50: F is with_non-empty_elements by AMI_1:def 1;
      F is c=-linear proof let X,Y be set;
     assume X in F;
        then consider A being set such that
    A51: A in bool REAL and
    A52: A in R and
    A53: X = ("f).A by FUNCT_2:115;
        consider r1 such that
    A54: A = left_closed_halfline(r1) and r1 <= f.p by A52;
     assume Y in F;
        then consider B being set such that
    A55: B in bool REAL and
    A56: B in R and
    A57: Y = ("f).B by FUNCT_2:115;
        consider r2 such that
    A58: B = left_closed_halfline(r2) and r2 <= f.p by A56;
          r1 <= r2 or r2 <= r1;
    then A59: A c= B or B c= A by A54,A58,LIMFUNC1:14;
          X = f"A & Y = f"B by A51,A53,A55,A57,Def2;
     then X c= Y or Y c= X by A59,RELAT_1:178;
     hence thesis by XBOOLE_0:def 9;
    end;
then A60: F is centered by A39,A50,Th1;
      R is closed proof let X be Subset of REAL;
     assume X in R;
        then ex r3 st X = left_closed_halfline(r3) & r3 <= f.p;
     hence X is closed by FCONT_3:6;
    end;
    then F is closed by A2,Th59;
    then meet F <> {} by A1,A60,COMPTS_1:13;
    then consider x being set such that
A61:  x in meet F by XBOOLE_0:def 1;
    reconsider x as Element of T by A61;
A62: f.x in meet R by A61,Th2;
    consider eR being Element of R;
A63: f.x in eR by A62,SETFAM_1:def 1;
      eR in R; then consider er being Real such that
A64: eR = left_closed_halfline(er) & er <= f.p;
      left_closed_halfline(er) = {r3 : r3 <= er} by LIMFUNC1:def 1;
    then consider r1 being Real such that
A65: f.x = r1 & r1 <= er by A63,A64;
A66: f.x <= f.p by A64,A65,AXIOMS:22;
    consider fx' being real number such that
A67:  fx' < f.x by REAL_1:77;
    reconsider fx' as Real by XREAL_0:def 1;
      fx' <= f.p by A66,A67,AXIOMS:22;
    then left_closed_halfline(fx') in R;
then A68:  f.x in left_closed_halfline(fx') by A62,SETFAM_1:def 1;
      left_closed_halfline(fx') = {r3 : r3 <= fx'} by LIMFUNC1:def 1;
    then ex r3 st f.x = r3 & r3 <= fx' by A68;
  hence contradiction by A67;
 end;
end;

definition
 cluster compact non empty TopSpace;
 existence proof
  take 1TopSp {{}};
  thus thesis by PCOMPS_1:9;
 end;
end;

definition let T be pseudocompact non empty TopSpace;
 cluster continuous -> bounded with_max with_min RealMap of T;
 coherence proof let f be RealMap of T; assume
A1: f is continuous;
  hence f is bounded by Def27;
  A2: for f being RealMap of T st f is continuous holds f is bounded by Def27;
  then A3:for f being RealMap of T st f is continuous holds f is with_max by
Th61;
  thus f is with_max by A1,A2,Th61;
  thus f is with_min by A1,A3,Th60;
 end;
end;

theorem Th62:
for T being non empty TopSpace, X being non empty Subset of T,
    Y being compact Subset of T, f being continuous RealMap of T
 st X c= Y holds inf (f||Y) <= inf (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; assume
A1: X c= Y;
    then reconsider Y1 = Y as non empty compact Subset of T by XBOOLE_1:3;
A2: inf (f||Y) = inf ((f||Y).:the carrier of (T|Y)) by Def20;
A3: (f||Y).:the carrier of (T|Y) = (f||Y).:Y by JORDAN1:1
    .= (f|Y).:Y by Def26
    .= f.:Y by RFUNCT_2:5;
A4: inf (f||X) = inf ((f||X).:the carrier of (T|X)) by Def20;
A5: (f||X).:the carrier of (T|X) = (f||X).:X by JORDAN1:1
    .= (f|X).:X by Def26
    .= f.:X by RFUNCT_2:5;
A6: (f||Y1).:the carrier of (T|Y1) is bounded_below by Def11;
    f.:X c= f.:Y by A1,RELAT_1:156;
 hence inf (f||Y) <= inf (f||X) by A2,A3,A4,A5,A6,Th12;
end;

theorem Th63:
for T being non empty TopSpace, X being non empty Subset of T,
    Y being compact Subset of T, f being continuous RealMap of T
 st X c= Y holds sup (f||X) <= sup (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; assume
A1: X c= Y;
    then reconsider Y1 = Y as non empty compact Subset of T by XBOOLE_1:3;
A2: sup (f||Y) = sup ((f||Y).:the carrier of (T|Y)) by Def21;
A3: (f||Y).:the carrier of (T|Y) = (f||Y).:Y by JORDAN1:1
    .= (f|Y).:Y by Def26
    .= f.:Y by RFUNCT_2:5;
A4: sup (f||X) = sup ((f||X).:the carrier of (T|X)) by Def21;
A5: (f||X).:the carrier of (T|X) = (f||X).:X by JORDAN1:1
    .= (f|X).:X by Def26
    .= f.:X by RFUNCT_2:5;
A6: (f||Y1).:the carrier of (T|Y1) is bounded_above by Def12;
    f.:X c= f.:Y by A1,RELAT_1:156;
 hence sup (f||X) <= sup (f||Y) by A2,A3,A4,A5,A6,Th13;
end;

begin :: Bounding boxes of compact sets in TOP-REAL 2

definition let n be Nat; let p1, p2 be Point of TOP-REAL n;
 cluster LSeg(p1,p2) -> compact;
 coherence by SPPOL_1:28;
end;

theorem Th64:
for n being Nat, X, Y being compact Subset of TOP-REAL n
 holds X /\ Y is compact
proof let n be Nat, X, Y be compact Subset of TOP-REAL n;
    TOP-REAL n is_T2 by SPPOL_1:26;
 hence X/\Y is compact by COMPTS_1:20;
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
 func proj1 -> RealMap of TOP-REAL 2 means
:Def28: for p being Point of TOP-REAL 2 holds it.p = p`1;
 existence
 proof
  deffunc F(Point of TOP-REAL 2) = $1`1;
  thus ex f be RealMap of TOP-REAL 2 st
   for p being Point of TOP-REAL 2 holds f.p = F(p) from LambdaRF;
 end;
 uniqueness proof let it1, it2 be RealMap of TOP-REAL 2 such that
 A1:  for p being Point of TOP-REAL 2 holds it1.p = p`1 and
 A2:  for p being 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 A1 .= it2.p by A2;
   end;
  hence it1 = it2 by FUNCT_2:113;
 end;
 func proj2 -> RealMap of TOP-REAL 2 means
:Def29: for p being Point of TOP-REAL 2 holds it.p = p`2;
 existence
 proof
  deffunc F(Point of TOP-REAL 2) = $1`2;
  thus ex f be RealMap of TOP-REAL 2 st
   for p being Point of TOP-REAL 2 holds f.p = F(p) from LambdaRF;
 end;
 uniqueness proof let it1, it2 be RealMap of TOP-REAL 2 such that
 A3:  for p being Point of TOP-REAL 2 holds it1.p = p`2 and
 A4:  for p being 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 A3 .= it2.p by A4;
   end;
  hence it1 = it2 by FUNCT_2:113;
 end;
end;

theorem Th65:
proj1"].r,s.[ = {|[ r1, r2 ]| : r < r1 & r1 < s}
proof set Q = proj1"].r,s.[; set QQ = {|[ r1,r2 ]|: r < r1 & r1 < s};
A1: ].r,s.[ = {p3: r<p3 & p3<s} by RCOMP_1:def 2;
    now let z be set;
   hereby assume
   A2: z in Q;
     then reconsider p = z as Point of TOP-REAL 2;
       proj1.p in ].r,s.[ by A2,FUNCT_2:46;
     then consider t being Real such that
   A3: t = proj1.p & r<t & t<s by A1;
       p`1 = proj1.p & p = |[ p`1,p`2 ]| by Def28,EUCLID:57;
    hence z in QQ by A3;
   end; assume z in QQ; then consider r1, r2 being Real such that
   A4: z = |[ r1,r2 ]| & r<r1 & r1 <s;
   set p = |[ r1,r2 ]|;
   A5: proj1.p = p`1 by Def28 .= r1 by EUCLID:56;
        r1 in ].r,s.[ by A1,A4;
   hence z in Q by A4,A5,FUNCT_2:46;
  end;
 hence proj1"].r,s.[ = {|[ r1, r2 ]| : r < r1 & r1 < s} by TARSKI:2;
end;

theorem Th66:
for r3, q3 st P = {|[ r1, r2 ]| : r3 < r1 & r1 < q3} holds P is open
proof let r3, q3; assume
A1: P = {|[ r1, r2 ]| : r3 < r1 & r1 < q3};
deffunc F(Real,Real) = |[ $1,$2 ]|;
defpred P1[Real,Real] means r3 < $1;
defpred P2[Real,Real] means $1 < q3;
A2:{F(r1,r2) : P1[r1,r2]} is Subset of TOP-REAL 2
     from SubsetFD2;
    {F(r1,r2) : P2[r1,r2]} is Subset of TOP-REAL 2
     from SubsetFD2;
   then reconsider Q1 = {|[ r1,r2 ]|: r3 < r1}, Q2 = {|[ r1,r2 ]|: r1 < q3}
           as Subset of TOP-REAL 2 by A2;
A3: Q1 is open by JORDAN1:25;
A4: Q2 is open by JORDAN1:26;
      now let x be set;
     hereby assume x in P; then consider r1, r2 being Real such that
     A5: x = |[ r1, r2 ]| & r3 < r1 & r1 < q3 by A1;
           x in Q1 & x in Q2 by A5;
      hence x in Q1/\Q2 by XBOOLE_0:def 3;
     end; assume x in Q1/\Q2;
     then A6: x in Q1 & x in Q2 by XBOOLE_0:def 3;
         then consider r1, r2 being Real such that
     A7: x = |[ r1, r2 ]| & r3 < r1;
         consider r1', r2' being Real such that
     A8: x = |[ r1', r2' ]| & r1' < q3 by A6;
           |[ r1, r2 ]|`1 = r1 & |[ r1, r2 ]|`2 = r2 &
         |[ r1', r2' ]|`1 = r1' & |[ r1', r2' ]|`2 = r2'
            by EUCLID:56;
     hence x in P by A1,A7,A8;
    end;
    then P = Q1/\Q2 by TARSKI:2;
 hence P is open by A3,A4,TOPS_1:38;
end;

theorem Th67:
proj2"].r,s.[ = {|[ r1, r2 ]| : r < r2 & r2 < s}
proof set Q = proj2"].r,s.[; set QQ = {|[ r1,r2 ]|: r < r2 & r2 < s};
A1: ].r,s.[ = {p3: r<p3 & p3<s} by RCOMP_1:def 2;
    now let z be set;
   hereby assume
   A2: z in Q;
     then reconsider p = z as Point of TOP-REAL 2;
       proj2.p in ].r,s.[ by A2,FUNCT_2:46;
     then consider t being Real such that
   A3: t = proj2.p & r<t & t<s by A1;
       p`2 = proj2.p & p = |[ p`1,p`2 ]| by Def29,EUCLID:57;
    hence z in QQ by A3;
   end; assume z in QQ; then consider r1, r2 being Real such that
   A4: z = |[ r1,r2 ]| & r<r2 & r2 <s;
   set p = |[ r1,r2 ]|;
   A5: proj2.p = p`2 by Def29 .= r2 by EUCLID:56;
        r2 in ].r,s.[ by A1,A4;
   hence z in Q by A4,A5,FUNCT_2:46;
  end;
 hence proj2"].r,s.[ = {|[ r1, r2 ]| : r < r2 & r2 < s} by TARSKI:2;
end;

theorem Th68:
for r3, q3 st P = {|[ r1, r2 ]| : r3 < r2 & r2 < q3} holds P is open
proof let r3, q3; assume
A1: P = {|[ r1, r2 ]| : r3 < r2 & r2 < q3};
deffunc F(Real,Real) = |[ $1,$2 ]|;
defpred P1[Real,Real] means r3 < $2;
defpred P2[Real,Real] means $2 < q3;
A2:{F(r1,r2) : P1[r1,r2]}
           is Subset of TOP-REAL 2 from SubsetFD2;
    {F(r1,r2) : P2[r1,r2]}
           is Subset of TOP-REAL 2 from SubsetFD2;
   then reconsider Q1 = {|[ r1,r2 ]|: r3 < r2}, Q2 = {|[ r1,r2 ]|: r2 < q3}
           as Subset of TOP-REAL 2 by A2;
A3: Q1 is open by JORDAN1:27;
A4: Q2 is open by JORDAN1:28;
      now let x be set;
     hereby assume x in P; then consider r1, r2 being Real such that
     A5: x = |[ r1, r2 ]| & r3 < r2 & r2 < q3 by A1;
           x in Q1 & x in Q2 by A5;
      hence x in Q1/\Q2 by XBOOLE_0:def 3;
     end; assume x in Q1/\Q2;
     then A6: x in Q1 & x in Q2 by XBOOLE_0:def 3;
         then consider r1, r2 being Real such that
     A7: x = |[ r1, r2 ]| & r3 < r2;
         consider r1', r2' being Real such that
     A8: x = |[ r1', r2' ]| & r2' < q3 by A6;
           |[ r1, r2 ]|`1 = r1 & |[ r1, r2 ]|`2 = r2 &
         |[ r1', r2' ]|`1 = r1' & |[ r1', r2' ]|`2 = r2'
            by EUCLID:56;
     hence x in P by A1,A7,A8;
    end;
    then P = Q1/\Q2 by TARSKI:2;
 hence P is open by A3,A4,TOPS_1:38;
end;

definition
 cluster proj1 -> continuous;
 coherence proof
   now let Y be Subset of REAL; assume
 A1: Y is open;
  set p1Y = (proj1"Y);
     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:46; then consider g being real number such that
   A3: 0<g and
   A4: ].p1-g,p1+g.[ c= Y by A1,RCOMP_1:40;
       reconsider g as Real by XREAL_0:def 1;
   A5: p1 < p1+g by A3,REAL_1:69;
   then A6: p1-g < p1 by REAL_1:84;
         ].p1-g,p1+g.[ = {r3 : p1-g<r3 & r3<p1+g} by RCOMP_1:def 2;
   then A7: p1 in ].p1-g,p1+g.[ by A5,A6;
     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 Th65;
     hence Q is open by Th66;
     thus Q c= p1Y by A4,RELAT_1:178;
     thus x in Q by A7,FUNCT_2:46;
    end;
    assume ex Q being 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:57;
  end;
  hence thesis by Th54;
 end;
 cluster proj2 -> continuous;
 coherence proof now let Y be Subset of REAL; assume
 A8: Y is open;
  set p1Y = (proj2"Y);
     now let x be set;
    hereby assume
   A9: x in p1Y;
       then reconsider p = x as Point of TOP-REAL 2;
       set p1 = proj2.p;
         p1 in Y by A9,FUNCT_2:46; then consider g being real number such that
   A10: 0<g and
   A11: ].p1-g,p1+g.[ c= Y by A8,RCOMP_1:40;
       reconsider g as Real by XREAL_0:def 1;
   A12: p1 < p1+g by A10,REAL_1:69;
   then A13: p1-g < p1 by REAL_1:84;
         ].p1-g,p1+g.[ = {r3 : p1-g<r3 & r3<p1+g} by RCOMP_1:def 2;
   then A14: p1 in ].p1-g,p1+g.[ by A12,A13;
     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 Th67;
     hence Q is open by Th68;
     thus Q c= p1Y by A11,RELAT_1:178;
     thus x in Q by A14,FUNCT_2:46;
    end;
    assume ex Q being 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:57;
  end;
  hence thesis by Th54;
 end;
end;

theorem Th69:
 for X being Subset of TOP-REAL 2, p being 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
A1: p in X;
 thus (proj1||X).p = (proj1|X).p by Def26
   .= proj1.p by A1,FUNCT_1:72
   .= p`1 by Def28;
end;

theorem Th70:
 for X being Subset of TOP-REAL 2, p being 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
A1: p in X;
 thus (proj2||X).p = (proj2|X).p by Def26
   .= proj2.p by A1,FUNCT_1:72
   .= p`2 by Def29;
end;

Lm9:
p in X implies inf (proj1||X) <= p`1 & p`1 <= sup (proj1||X) &
                 inf (proj2||X) <= p`2 & p`2 <= sup (proj2||X)
proof assume
A1: p in X;
   then reconsider p' = p as Point of (TOP-REAL 2)|X by JORDAN1:1;
A2: ((proj1||X)).p' = p`1 by A1,Th69;
 hence inf (proj1||X) <= p`1 by Th47;
 thus p`1 <= sup (proj1||X) by A2,Th50;
A3: ((proj2||X)).p' = p`2 by A1,Th70;
 hence inf (proj2||X) <= p`2 by Th47;
 thus p`2 <= sup (proj2||X) by A3,Th50;
end;

definition let X be Subset of TOP-REAL 2;
 func W-bound X -> Real equals
:Def30: inf (proj1||X);
 coherence;
 func N-bound X -> Real equals
:Def31: sup (proj2||X);
 coherence;
 func E-bound X -> Real equals
:Def32: sup (proj1||X);
 coherence;
 func S-bound X -> Real equals
:Def33: inf (proj2||X);
 coherence;
end;

theorem Th71:
p in X implies W-bound X <= p`1 & p`1 <= E-bound X &
                 S-bound X <= p`2 & p`2 <= N-bound X
proof
   W-bound X = inf (proj1||X) & N-bound X = sup (proj2||X) &
 E-bound X = sup (proj1||X) & S-bound X = inf (proj2||X)
   by Def30,Def31,Def32,Def33;
 hence thesis by Lm9;
end;

definition let X be Subset of TOP-REAL 2;
 func SW-corner X -> Point of TOP-REAL 2 equals
:Def34: |[W-bound X, S-bound X]|;
 coherence;
 func NW-corner X -> Point of TOP-REAL 2 equals
:Def35: |[W-bound X, N-bound X]|;
 coherence;
 func NE-corner X -> Point of TOP-REAL 2 equals
:Def36: |[E-bound X, N-bound X]|;
 coherence;
 func SE-corner X -> Point of TOP-REAL 2 equals
:Def37: |[E-bound X, S-bound X]|;
 coherence;
end;

:: Corners

theorem Th72:
(SW-corner P)`1 = W-bound P
proof SW-corner P = |[W-bound P, S-bound P]| by Def34;
 hence thesis by EUCLID:56;
end;

theorem Th73:
(SW-corner P)`2 = S-bound P
proof
      SW-corner P = |[W-bound P, S-bound P]| by Def34;
 hence (SW-corner P)`2 = S-bound P by EUCLID:56;
end;

theorem Th74:
(NW-corner P)`1 = W-bound P
proof
    NW-corner P = |[W-bound P, N-bound P]| by Def35;
 hence thesis by EUCLID:56;
end;

theorem Th75:
(NW-corner P)`2 = N-bound P
proof
      NW-corner P = |[W-bound P, N-bound P]| by Def35;
 hence (NW-corner P)`2 = N-bound P by EUCLID:56;
end;

theorem Th76:
(NE-corner P)`1 = E-bound P
proof
      NE-corner P = |[E-bound P, N-bound P]| by Def36;
 hence (NE-corner P)`1 = E-bound P by EUCLID:56;
end;

theorem Th77:
(NE-corner P)`2 = N-bound P
proof
    NE-corner P = |[E-bound P, N-bound P]| by Def36;
 hence thesis by EUCLID:56;
end;

theorem Th78:
(SE-corner P)`1 = E-bound P
proof SE-corner P = |[E-bound P, S-bound P]| by Def37;
 hence thesis by EUCLID:56;
end;

theorem Th79:
(SE-corner P)`2 = S-bound P
proof
      SE-corner P = |[E-bound P, S-bound P]| by Def37;
 hence (SE-corner P)`2 = S-bound P by EUCLID:56;
end;

theorem
  (SW-corner P)`1 = (NW-corner P)`1
proof
 thus (SW-corner P)`1 = W-bound P by Th72
          .= (NW-corner P)`1 by Th74;
end;

theorem
  (SE-corner P)`1 = (NE-corner P)`1
proof
 thus (SE-corner P)`1 = E-bound P by Th78
          .= (NE-corner P)`1 by Th76;
end;

theorem
  (NW-corner P)`2 = (NE-corner P)`2
proof
 thus (NW-corner P)`2 = N-bound P by Th75
          .= (NE-corner P)`2 by Th77;
end;

theorem
  (SW-corner P)`2 = (SE-corner P)`2
proof
 thus (SW-corner P)`2 = S-bound P by Th73
          .= (SE-corner P)`2 by Th79;
end;

definition let X be Subset of TOP-REAL 2;
 func W-most X -> Subset of TOP-REAL 2 equals
:Def38: LSeg(SW-corner X, NW-corner X)/\X;
 coherence;
 func N-most X -> Subset of TOP-REAL 2 equals
:Def39: LSeg(NW-corner X, NE-corner X)/\X;
 coherence;
 func E-most X -> Subset of TOP-REAL 2 equals
:Def40: LSeg(SE-corner X, NE-corner X)/\X;
 coherence;
 func S-most X -> Subset of TOP-REAL 2 equals
:Def41: LSeg(SW-corner X, SE-corner X)/\X;
 coherence;
end;

definition let X be non empty compact Subset of TOP-REAL 2;
 cluster W-most X -> non empty compact;
 coherence proof
A1: W-most X = LSeg(SW-corner X, NW-corner X)/\X by Def38;
    SW-corner X = |[W-bound X, S-bound X]| &
  NW-corner X = |[W-bound X, N-bound X]| by Def34,Def35;
then A2: (SW-corner X)`1 = W-bound X & (NW-corner X)`1 = W-bound X &
   (SW-corner X)`2 = S-bound X & (NW-corner X)`2 = N-bound X
          by EUCLID:56;
   set p1X = (proj1||X), c = the carrier of (TOP-REAL 2)|X;
A3: inf p1X = W-bound X by Def30;
A4: c = X by JORDAN1:1;
A5: inf p1X = inf (p1X.:c) by Def20;
     p1X.:c is with_min by Def15;
   then inf (p1X.:c) in p1X.:c by Def4;
   then consider p being set such that
A6: p in c & p in c & inf (p1X.:c) = p1X.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A6;
A7: p1X.p = p`1 by A4,A6,Th69;
     S-bound X <= p`2 & p`2 <= N-bound X by A4,A6,Th71;
   then p in LSeg(SW-corner X, NW-corner X) by A2,A3,A5,A6,A7,GOBOARD7:8;
  hence thesis by A1,A4,A6,Th64,XBOOLE_0:def 3;
 end;
 cluster N-most X -> non empty compact;
 coherence proof
A8:N-most X = LSeg(NW-corner X, NE-corner X)/\X by Def39;
    NW-corner X = |[W-bound X, N-bound X]| &
  NE-corner X = |[E-bound X, N-bound X]| by Def35,Def36;
then A9: (NW-corner X)`1 = W-bound X & (NE-corner X)`1 = E-bound X &
   (NW-corner X)`2 = N-bound X & (NE-corner X)`2 = N-bound X
          by EUCLID:56;
   set p2X = (proj2||X), c = the carrier of (TOP-REAL 2)|X;
A10: sup p2X = N-bound X by Def31;
A11: c = X by JORDAN1:1;
A12: sup p2X = sup (p2X.:c) by Def21;
     p2X.:c is with_max by Def14;
   then sup (p2X.:c) in p2X.:c by Def3;
   then consider p being set such that
A13: p in c & p in c & sup (p2X.:c) = p2X.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A11,A13;
A14: p2X.p = p`2 by A11,A13,Th70;
     W-bound X <= p`1 & p`1 <= E-bound X by A11,A13,Th71;
   then p in LSeg(NW-corner X, NE-corner X) by A9,A10,A12,A13,A14,GOBOARD7:9;
  hence thesis by A8,A11,A13,Th64,XBOOLE_0:def 3;
 end;
 cluster E-most X -> non empty compact;
 coherence proof
A15:E-most X = LSeg(SE-corner X, NE-corner X)/\X by Def40;
    SE-corner X = |[E-bound X, S-bound X]| &
  NE-corner X = |[E-bound X, N-bound X]| by Def36,Def37;
then A16: (SE-corner X)`1 = E-bound X & (NE-corner X)`1 = E-bound X &
   (SE-corner X)`2 = S-bound X & (NE-corner X)`2 = N-bound X
          by EUCLID:56;
   set p1X = (proj1||X), c = the carrier of (TOP-REAL 2)|X;
A17: sup p1X = E-bound X by Def32;
A18: c = X by JORDAN1:1;
A19: sup p1X = sup (p1X.:c) by Def21;
     p1X.:c is with_max by Def14;
   then sup (p1X.:c) in p1X.:c by Def3;
   then consider p being set such that
A20: p in c & p in c & sup (p1X.:c) = p1X.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A18,A20;
A21: p1X.p = p`1 by A18,A20,Th69;
     S-bound X <= p`2 & p`2 <= N-bound X by A18,A20,Th71;
   then p in LSeg(SE-corner X, NE-corner X) by A16,A17,A19,A20,A21,GOBOARD7:8;
  hence thesis by A15,A18,A20,Th64,XBOOLE_0:def 3;
 end;
 cluster S-most X -> non empty compact;
 coherence proof
A22:S-most X = LSeg(SW-corner X, SE-corner X)/\X by Def41;
    SW-corner X = |[W-bound X, S-bound X]| &
  SE-corner X = |[E-bound X, S-bound X]| by Def34,Def37;
then A23: (SW-corner X)`1 = W-bound X & (SE-corner X)`1 = E-bound X &
   (SW-corner X)`2 = S-bound X & (SE-corner X)`2 = S-bound X
          by EUCLID:56;
   set p2X = (proj2||X), c = the carrier of (TOP-REAL 2)|X;
A24: inf p2X = S-bound X by Def33;
A25: c = X by JORDAN1:1;
A26: inf p2X = inf (p2X.:c) by Def20;
     p2X.:c is with_min by Def15;
   then inf (p2X.:c) in p2X.:c by Def4;
   then consider p being set such that
A27: p in c & p in c & inf (p2X.:c) = p2X.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A25,A27;
A28: p2X.p = p`2 by A25,A27,Th70;
     W-bound X <= p`1 & p`1 <= E-bound X by A25,A27,Th71;
   then p in LSeg(SW-corner X, SE-corner X) by A23,A24,A26,A27,A28,GOBOARD7:9;
  hence thesis by A22,A25,A27,Th64,XBOOLE_0:def 3;
 end;
end;

definition let X be Subset of TOP-REAL 2;
 func W-min X -> Point of TOP-REAL 2 equals
:Def42: |[W-bound X, inf (proj2||W-most X)]|;
 coherence;
 func W-max X -> Point of TOP-REAL 2 equals
:Def43: |[W-bound X, sup (proj2||W-most X)]|;
 coherence;
 func N-min X -> Point of TOP-REAL 2 equals
:Def44: |[inf (proj1||N-most X), N-bound X]|;
 coherence;
 func N-max X -> Point of TOP-REAL 2 equals
:Def45: |[sup (proj1||N-most X), N-bound X]|;
 coherence;
 func E-max X -> Point of TOP-REAL 2 equals
:Def46: |[E-bound X, sup (proj2||E-most X)]|;
 coherence;
 func E-min X -> Point of TOP-REAL 2 equals
:Def47: |[E-bound X, inf (proj2||E-most X)]|;
 coherence;
 func S-max X -> Point of TOP-REAL 2 equals
:Def48: |[sup (proj1||S-most X), S-bound X]|;
 coherence;
 func S-min X -> Point of TOP-REAL 2 equals
:Def49: |[inf (proj1||S-most X), S-bound X]|;
 coherence;
end;

theorem Th84:
(W-min P)`1 = W-bound P &
(W-max P)`1 = W-bound P
proof SW-corner P = |[W-bound P, S-bound P]| &
  NW-corner P = |[W-bound P, N-bound P]| &
  W-min P = |[W-bound P, inf (proj2||W-most P)]| &
  W-max P = |[W-bound P, sup (proj2||W-most P)]|
     by Def34,Def35,Def42,Def43;
 hence thesis by EUCLID:56;
end;

theorem Th85:
(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 (SW-corner P)`1 = W-bound P & (W-min P)`1 = W-bound P &
 (W-max P)`1 = W-bound P & (NW-corner P)`1 = W-bound P by Th72,Th74,Th84;
 hence thesis;
end;

theorem Th86:
(W-min P)`2 = inf (proj2||W-most P) &
(W-max P)`2 = sup (proj2||W-most P)
proof
A1: W-min P = |[W-bound P, inf (proj2||W-most P)]| by Def42;
A2: W-max P = |[W-bound P, sup (proj2||W-most P)]| by Def43;
    set LP = W-most P;
 thus (W-min P)`2 = inf (proj2||LP) by A1,EUCLID:56;
 thus (W-max P)`2 = sup (proj2||LP) by A2,EUCLID:56;
end;

theorem Th87:
(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
A1: (SW-corner X)`2 = S-bound X by Th73 .= inf (proj2||X) by Def33;
    set LX = W-most X;
A2: (W-min X)`2 = inf (proj2||LX) by Th86;
A3: (W-max X)`2 = sup (proj2||LX) by Th86;
A4: (NW-corner X)`2 = N-bound X by Th75 .= sup (proj2||X) by Def31;
       W-most X = LSeg(SW-corner X, NW-corner X)/\X by Def38;
then A5: W-most X c= X by XBOOLE_1:17;
then A6: (SW-corner X)`2 <= (W-min X)`2 by A1,A2,Th62;
A7: (W-min X)`2 <= (W-max X)`2 by A2,A3,Th53;
A8: (W-max X)`2 <= (NW-corner X)`2 by A3,A4,A5,Th63;
  thus (SW-corner X)`2 <= (W-min X)`2 by A1,A2,A5,Th62;
  thus (SW-corner X)`2 <= (W-max X)`2 by A6,A7,AXIOMS:22;
  hence (SW-corner X)`2 <= (NW-corner X)`2 by A8,AXIOMS:22;
  thus (W-min X)`2 <= (W-max X)`2 by A2,A3,Th53;
  thus (W-min X)`2 <= (NW-corner X)`2 by A7,A8,AXIOMS:22;
  thus (W-max X)`2 <= (NW-corner X)`2 by A3,A4,A5,Th63;
end;

theorem Th88:
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 assume
A1: p in W-most Z;
   then p in LSeg(SW-corner Z, NW-corner Z)/\Z by Def38;
then A2: p in LSeg(SW-corner Z, NW-corner Z) & p in Z by XBOOLE_0:def 3;
  (SW-corner Z)`1 = W-bound Z & (W-min Z)`1 = W-bound Z &
   (W-max Z)`1 = W-bound Z & (NW-corner Z)`1 = W-bound Z by Th72,Th74,Th84;
 hence p`1 = (W-min Z)`1 by A2,GOBOARD7:5;
 assume Z is compact;
   then reconsider Z as non empty compact Subset of TOP-REAL 2;
    (W-min Z)`2 = inf (proj2||W-most Z) & (W-max Z)`2 = sup (proj2||W-most Z)
      by Th86;
 hence thesis by A1,Lm9;
end;

theorem Th89:
W-most X c= LSeg(W-min X, W-max X)
proof let x be set; assume
A1: x in W-most X;
   then reconsider p = x as Point of TOP-REAL 2;
A2: (W-min X)`1 = (W-max X)`1 by Th85;
     p`1 = (W-min X)`1 & (W-min X)`2 <= p`2 & p`2 <=(W-max X)`2 by A1,Th88;
 hence x in LSeg(W-min X, W-max X) by A2,GOBOARD7:8;
end;

theorem
  LSeg(W-min X, W-max X) c= LSeg(SW-corner X, NW-corner X)
proof
A1: (SW-corner X)`1 = W-bound X & (W-min X)`1 = W-bound X &
   (W-max X)`1 = W-bound X & (NW-corner X)`1 = W-bound X by Th72,Th74,Th84;
     (SW-corner X)`2 <= (W-min X)`2 &
   (SW-corner X)`2 <= (W-max X)`2 &
   (W-min X)`2 <= (NW-corner X)`2 &
   (W-max X)`2 <= (NW-corner X)`2 by Th87;
   then W-min X in LSeg(SW-corner X, NW-corner X) &
   W-max X in LSeg(SW-corner X, NW-corner X) by A1,GOBOARD7:8;
 hence thesis by TOPREAL1:12;
end;

theorem Th91:
W-min X in W-most X & W-max X in W-most X
proof
A1: W-most X = LSeg(SW-corner X, NW-corner X)/\X by Def38;
A2: W-min X = |[W-bound X, inf (proj2||W-most X)]| by Def42;
A3: W-max X = |[W-bound X, sup (proj2||W-most X)]| by Def43;
   set p2W = (proj2||W-most X), c = the carrier of (TOP-REAL 2)|W-most X;
A4: c = W-most X by JORDAN1:1;
A5: inf p2W = inf (p2W.:c) by Def20;
     p2W.:c is with_min by Def15;
   then inf (p2W.:c) in p2W.:c by Def4;
   then consider p being set such that
A6: p in c & p in c & inf (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A6;
A7: p2W.p = p`2 by A4,A6,Th70;
A8: p in LSeg(SW-corner X, NW-corner X) by A1,A4,A6,XBOOLE_0:def 3;
     (SW-corner X)`1 = W-bound X &
   (NW-corner X)`1 = W-bound X by Th72,Th74;
    then p`1 = W-bound X by A8,GOBOARD7:5;
 hence W-min X in W-most X by A2,A4,A5,A6,A7,EUCLID:57;
A9: sup p2W = sup (p2W.:c) by Def21;
     p2W.:c is with_max by Def14;
   then sup (p2W.:c) in p2W.:c by Def3;
   then consider p being set such that
A10: p in c & p in c & sup (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A10;
A11: p2W.p = p`2 by A4,A10,Th70;
A12: p in LSeg(SW-corner X, NW-corner X) by A1,A4,A10,XBOOLE_0:def 3;
     (SW-corner X)`1 = W-bound X &
   (NW-corner X)`1 = W-bound X by Th72,Th74;
     then p`1 = W-bound X by A12,GOBOARD7:5;
 hence W-max X in W-most X by A3,A4,A9,A10,A11,EUCLID:57;
end;

theorem
  LSeg(SW-corner X, W-min X)/\X = {W-min X} &
LSeg(W-max X, NW-corner X)/\X = {W-max X}
proof
A1: W-most X = LSeg(SW-corner X, NW-corner X)/\X by Def38;
   now let x be set;
  hereby
   assume A2: x in LSeg(SW-corner X, W-min X)/\X;
  then A3: x in LSeg(SW-corner X, W-min X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A2;
       (SW-corner X)`1 = (W-min X)`1 by Th85;
  then A4: p`1 = (W-min X)`1 by A3,GOBOARD7:5;
       (SW-corner X)`2 <= (W-min X)`2 by Th87;
  then A5: p`2 <= (W-min X)`2 by A3,TOPREAL1:10;
  A6: SW-corner X in LSeg(SW-corner X, NW-corner X) by TOPREAL1:6;
       W-min X in W-most X by Th91;
     then W-min X in LSeg(SW-corner X, NW-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(SW-corner X, W-min X) c= LSeg(SW-corner X, NW-corner X)
       by A6,TOPREAL1:12;
     then p in W-most X by A1,A3,XBOOLE_0:def 3;
     then (W-min X)`2 <= p`2 by Th88;
  then A7: p`2 = (W-min X)`2 by A5,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = W-min X by A4,A7,EUCLID:57;
  end;
  assume A8: x = W-min X;
       W-min X in W-most X by Th91;
  then A9: W-min X in X by A1,XBOOLE_0:def 3;
       W-min X in LSeg(SW-corner X, W-min X) by TOPREAL1:6;
  hence x in LSeg(SW-corner X, W-min X)/\X by A8,A9,XBOOLE_0:def 3;
 end;
 hence LSeg(SW-corner X, W-min X)/\X = {W-min X} by TARSKI:def 1;
   now let x be set;
  hereby
   assume A10: x in LSeg(W-max X, NW-corner X)/\X;
  then A11: x in LSeg(W-max X, NW-corner X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A10;
       (NW-corner X)`1 = (W-max X)`1 by Th85;
  then A12: p`1 = (W-max X)`1 by A11,GOBOARD7:5;
       (W-max X)`2 <= (NW-corner X)`2 by Th87;
  then A13: (W-max X)`2 <= p`2 by A11,TOPREAL1:10;
  A14: NW-corner X in LSeg(SW-corner X, NW-corner X) by TOPREAL1:6;
       W-max X in W-most X by Th91;
     then W-max X in LSeg(SW-corner X, NW-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(W-max X, NW-corner X) c= LSeg(SW-corner X, NW-corner X)
       by A14,TOPREAL1:12;
     then p in W-most X by A1,A11,XBOOLE_0:def 3;
     then p`2 <= (W-max X)`2 by Th88;
  then A15: p`2 = (W-max X)`2 by A13,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = W-max X by A12,A15,EUCLID:57;
  end;
  assume A16: x = W-max X;
       W-max X in W-most X by Th91;
  then A17: W-max X in X by A1,XBOOLE_0:def 3;
       W-max X in LSeg(W-max X, NW-corner X) by TOPREAL1:6;
  hence x in LSeg(W-max X, NW-corner X)/\X by A16,A17,XBOOLE_0:def 3;
 end;
 hence LSeg(W-max X, NW-corner X)/\X = {W-max X} by TARSKI:def 1;
end;

theorem
  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 Th89;
  then W-most X c= {W-min X} by TOPREAL1:7;
 hence W-most X = {W-min X} by ZFMISC_1:39;
end;

:: North

theorem Th94:
(N-min P)`2 = N-bound P &
(N-max P)`2 = N-bound P
proof NW-corner P = |[W-bound P, N-bound P]| &
  NE-corner P = |[E-bound P, N-bound P]| &
  N-min P = |[inf (proj1||N-most P), N-bound P]| &
  N-max P = |[sup (proj1||N-most P), N-bound P]|
     by Def35,Def36,Def44,Def45;
 hence thesis by EUCLID:56;
end;

theorem Th95:
(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 (NW-corner P)`2 = N-bound P & (N-min P)`2 = N-bound P &
 (N-max P)`2 = N-bound P & (NE-corner P)`2 = N-bound P by Th75,Th77,Th94;
 hence thesis;
end;

theorem Th96:
(N-min P)`1 = inf (proj1||N-most P) &
(N-max P)`1 = sup (proj1||N-most P)
proof
A1: N-min P = |[inf (proj1||N-most P), N-bound P]| by Def44;
A2: N-max P = |[sup (proj1||N-most P), N-bound P]| by Def45;
    set LP = N-most P;
 thus (N-min P)`1 = inf (proj1||LP) by A1,EUCLID:56;
 thus (N-max P)`1 = sup (proj1||LP) by A2,EUCLID:56;
end;

theorem Th97:
(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
A1: (NW-corner X)`1 = W-bound X by Th74 .= inf (proj1||X) by Def30;
    set LX = N-most X;
A2: (N-min X)`1 = inf (proj1||LX) by Th96;
A3: (N-max X)`1 = sup (proj1||LX) by Th96;
A4: (NE-corner X)`1 = E-bound X by Th76 .= sup (proj1||X) by Def32;
       N-most X = LSeg(NW-corner X, NE-corner X)/\X by Def39;
then A5: N-most X c= X by XBOOLE_1:17;
then A6: (NW-corner X)`1 <= (N-min X)`1 by A1,A2,Th62;
A7: (N-min X)`1 <= (N-max X)`1 by A2,A3,Th53;
A8: (N-max X)`1 <= (NE-corner X)`1 by A3,A4,A5,Th63;
  thus (NW-corner X)`1 <= (N-min X)`1 by A1,A2,A5,Th62;
  thus (NW-corner X)`1 <= (N-max X)`1 by A6,A7,AXIOMS:22;
  hence (NW-corner X)`1 <= (NE-corner X)`1 by A8,AXIOMS:22;
  thus (N-min X)`1 <= (N-max X)`1 by A2,A3,Th53;
  thus (N-min X)`1 <= (NE-corner X)`1 by A7,A8,AXIOMS:22;
  thus (N-max X)`1 <= (NE-corner X)`1 by A3,A4,A5,Th63;
end;

theorem Th98:
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 assume
A1: p in N-most Z;
   then p in LSeg(NW-corner Z, NE-corner Z)/\Z by Def39;
then A2: p in LSeg(NW-corner Z, NE-corner Z) & p in Z by XBOOLE_0:def 3;
  (NW-corner Z)`2 = N-bound Z & (N-min Z)`2 = N-bound Z &
   (N-max Z)`2 = N-bound Z & (NE-corner Z)`2 = N-bound Z by Th75,Th77,Th94;
 hence p`2 = (N-min Z)`2 by A2,GOBOARD7:6;
 assume Z is compact;
 then reconsider Z as non empty compact Subset of TOP-REAL 2;
    (N-min Z)`1 = inf (proj1||N-most Z) & (N-max Z)`1 = sup (proj1||N-most Z)
      by Th96;
 hence thesis by A1,Lm9;
end;

theorem Th99:
N-most X c= LSeg(N-min X, N-max X)
proof let x be set; assume
A1: x in N-most X;
   then reconsider p = x as Point of TOP-REAL 2;
A2: (N-min X)`2 = (N-max X)`2 by Th95;
     p`2 = (N-min X)`2 & (N-min X)`1 <= p`1 & p`1 <=(N-max X)`1 by A1,Th98;
 hence x in LSeg(N-min X, N-max X) by A2,GOBOARD7:9;
end;

theorem
  LSeg(N-min X, N-max X) c= LSeg(NW-corner X, NE-corner X)
proof
A1: (NW-corner X)`2 = N-bound X & (N-min X)`2 = N-bound X &
   (N-max X)`2 = N-bound X & (NE-corner X)`2 = N-bound X by Th75,Th77,Th94;
     (NW-corner X)`1 <= (N-min X)`1 &
   (NW-corner X)`1 <= (N-max X)`1 &
   (N-min X)`1 <= (NE-corner X)`1 &
   (N-max X)`1 <= (NE-corner X)`1 by Th97;
   then N-min X in LSeg(NW-corner X, NE-corner X) &
   N-max X in LSeg(NW-corner X, NE-corner X) by A1,GOBOARD7:9;
 hence thesis by TOPREAL1:12;
end;

theorem Th101:
N-min X in N-most X & N-max X in N-most X
proof
A1: N-most X = LSeg(NW-corner X, NE-corner X)/\X by Def39;
A2: N-min X = |[inf (proj1||N-most X), N-bound X]| by Def44;
A3: N-max X = |[sup (proj1||N-most X), N-bound X]| by Def45;
   set p2W = (proj1||N-most X), c = the carrier of (TOP-REAL 2)|N-most X;
A4: c = N-most X by JORDAN1:1;
A5: inf p2W = inf (p2W.:c) by Def20;
     p2W.:c is with_min by Def15;
   then inf (p2W.:c) in p2W.:c by Def4;
   then consider p being set such that
A6: p in c & p in c & inf (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A6;
A7: p2W.p = p`1 by A4,A6,Th69;
A8: p in LSeg(NW-corner X, NE-corner X) by A1,A4,A6,XBOOLE_0:def 3;
     (NW-corner X)`2 = N-bound X &
   (NE-corner X)`2 = N-bound X by Th75,Th77;
    then p`2 = N-bound X by A8,GOBOARD7:6;
 hence N-min X in N-most X by A2,A4,A5,A6,A7,EUCLID:57;
A9: sup p2W = sup (p2W.:c) by Def21;
     p2W.:c is with_max by Def14;
   then sup (p2W.:c) in p2W.:c by Def3;
   then consider p being set such that
A10: p in c & p in c & sup (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A10;
A11: p2W.p = p`1 by A4,A10,Th69;
A12: p in LSeg(NW-corner X, NE-corner X) by A1,A4,A10,XBOOLE_0:def 3;
     (NW-corner X)`2 = N-bound X &
   (NE-corner X)`2 = N-bound X by Th75,Th77;
     then p`2 = N-bound X by A12,GOBOARD7:6;
 hence N-max X in N-most X by A3,A4,A9,A10,A11,EUCLID:57;
end;

theorem
  LSeg(NW-corner X, N-min X)/\X = {N-min X} &
LSeg(N-max X, NE-corner X)/\X = {N-max X}
proof
A1: N-most X = LSeg(NW-corner X, NE-corner X)/\X by Def39;
   now let x be set;
  hereby
   assume A2: x in LSeg(NW-corner X, N-min X)/\X;
  then A3: x in LSeg(NW-corner X, N-min X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A2;
       (NW-corner X)`2 = (N-min X)`2 by Th95;
  then A4: p`2 = (N-min X)`2 by A3,GOBOARD7:6;
       (NW-corner X)`1 <= (N-min X)`1 by Th97;
  then A5: p`1 <= (N-min X)`1 by A3,TOPREAL1:9;
  A6: NW-corner X in LSeg(NW-corner X, NE-corner X) by TOPREAL1:6;
       N-min X in N-most X by Th101;
     then N-min X in LSeg(NW-corner X, NE-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(NW-corner X, N-min X) c= LSeg(NW-corner X, NE-corner X)
       by A6,TOPREAL1:12;
     then p in N-most X by A1,A3,XBOOLE_0:def 3;
     then (N-min X)`1 <= p`1 by Th98;
  then A7: p`1 = (N-min X)`1 by A5,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = N-min X by A4,A7,EUCLID:57;
  end;
  assume A8: x = N-min X;
       N-min X in N-most X by Th101;
  then A9: N-min X in X by A1,XBOOLE_0:def 3;
       N-min X in LSeg(NW-corner X, N-min X) by TOPREAL1:6;
  hence x in LSeg(NW-corner X, N-min X)/\X by A8,A9,XBOOLE_0:def 3;
 end;
 hence LSeg(NW-corner X, N-min X)/\X = {N-min X} by TARSKI:def 1;
   now let x be set;
  hereby
   assume A10: x in LSeg(N-max X, NE-corner X)/\X;
  then A11: x in LSeg(N-max X, NE-corner X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A10;
       (NE-corner X)`2 = (N-max X)`2 by Th95;
  then A12: p`2 = (N-max X)`2 by A11,GOBOARD7:6;
       (N-max X)`1 <= (NE-corner X)`1 by Th97;
  then A13: (N-max X)`1 <= p`1 by A11,TOPREAL1:9;
  A14: NE-corner X in LSeg(NW-corner X, NE-corner X) by TOPREAL1:6;
       N-max X in N-most X by Th101;
     then N-max X in LSeg(NW-corner X, NE-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(N-max X, NE-corner X) c= LSeg(NW-corner X, NE-corner X)
       by A14,TOPREAL1:12;
     then p in N-most X by A1,A11,XBOOLE_0:def 3;
     then p`1 <= (N-max X)`1 by Th98;
  then A15: p`1 = (N-max X)`1 by A13,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = N-max X by A12,A15,EUCLID:57;
  end;
  assume A16: x = N-max X;
       N-max X in N-most X by Th101;
  then A17: N-max X in X by A1,XBOOLE_0:def 3;
       N-max X in LSeg(N-max X, NE-corner X) by TOPREAL1:6;
  hence x in LSeg(N-max X, NE-corner X)/\X by A16,A17,XBOOLE_0:def 3;
 end;
 hence LSeg(N-max X, NE-corner X)/\X = {N-max X} by TARSKI:def 1;
end;

theorem
  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 Th99;
  then N-most X c= {N-min X} by TOPREAL1:7;
 hence N-most X = {N-min X} by ZFMISC_1:39;
end;

:: East

theorem Th104:
(E-min P)`1 = E-bound P &
(E-max P)`1 = E-bound P
proof SE-corner P = |[E-bound P, S-bound P]| &
  NE-corner P = |[E-bound P, N-bound P]| &
  E-min P = |[E-bound P, inf (proj2||E-most P)]| &
  E-max P = |[E-bound P, sup (proj2||E-most P)]|
     by Def36,Def37,Def46,Def47;
 hence thesis by EUCLID:56;
end;

theorem Th105:
(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 (SE-corner P)`1 = E-bound P & (E-min P)`1 = E-bound P &
 (E-max P)`1 = E-bound P & (NE-corner P)`1 = E-bound P by Th76,Th78,Th104;
 hence thesis;
end;

theorem Th106:
(E-min P)`2 = inf (proj2||E-most P) &
(E-max P)`2 = sup (proj2||E-most P)
proof
A1: E-min P = |[E-bound P, inf (proj2||E-most P)]| by Def47;
A2: E-max P = |[E-bound P, sup (proj2||E-most P)]| by Def46;
    set LP = E-most P;
 thus (E-min P)`2 = inf (proj2||LP) by A1,EUCLID:56;
 thus (E-max P)`2 = sup (proj2||LP) by A2,EUCLID:56;
end;

theorem Th107:
(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
A1: (SE-corner X)`2 = S-bound X by Th79 .= inf (proj2||X) by Def33;
    set LX = E-most X;
A2: (E-min X)`2 = inf (proj2||LX) by Th106;
A3: (E-max X)`2 = sup (proj2||LX) by Th106;
A4: (NE-corner X)`2 = N-bound X by Th77 .= sup (proj2||X) by Def31;
       E-most X = LSeg(SE-corner X, NE-corner X)/\X by Def40;
then A5: E-most X c= X by XBOOLE_1:17;
then A6: (SE-corner X)`2 <= (E-min X)`2 by A1,A2,Th62;
A7: (E-min X)`2 <= (E-max X)`2 by A2,A3,Th53;
A8: (E-max X)`2 <= (NE-corner X)`2 by A3,A4,A5,Th63;
  thus (SE-corner X)`2 <= (E-min X)`2 by A1,A2,A5,Th62;
  thus (SE-corner X)`2 <= (E-max X)`2 by A6,A7,AXIOMS:22;
  hence (SE-corner X)`2 <= (NE-corner X)`2 by A8,AXIOMS:22;
  thus (E-min X)`2 <= (E-max X)`2 by A2,A3,Th53;
  thus (E-min X)`2 <= (NE-corner X)`2 by A7,A8,AXIOMS:22;
  thus (E-max X)`2 <= (NE-corner X)`2 by A3,A4,A5,Th63;
end;

theorem Th108:
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 assume
A1: p in E-most Z;
   then p in LSeg(SE-corner Z, NE-corner Z)/\Z by Def40;
then A2: p in LSeg(SE-corner Z, NE-corner Z) & p in Z by XBOOLE_0:def 3;
  (SE-corner Z)`1 = E-bound Z & (E-min Z)`1 = E-bound Z &
   (E-max Z)`1 = E-bound Z & (NE-corner Z)`1 = E-bound Z by Th76,Th78,Th104;
 hence p`1 = (E-min Z)`1 by A2,GOBOARD7:5;
 assume Z is compact;
 then reconsider Z as non empty compact Subset of TOP-REAL 2;
    (E-min Z)`2 = inf (proj2||E-most Z) & (E-max Z)`2 = sup (proj2||E-most Z)
      by Th106;
 hence thesis by A1,Lm9;
end;

theorem Th109:
E-most X c= LSeg(E-min X, E-max X)
proof let x be set; assume
A1: x in E-most X;
   then reconsider p = x as Point of TOP-REAL 2;
A2: (E-min X)`1 = (E-max X)`1 by Th105;
     p`1 = (E-min X)`1 & (E-min X)`2 <= p`2 & p`2 <=(E-max X)`2 by A1,Th108;
 hence x in LSeg(E-min X, E-max X) by A2,GOBOARD7:8;
end;

theorem
  LSeg(E-min X, E-max X) c= LSeg(SE-corner X, NE-corner X)
proof
A1: (SE-corner X)`1 = E-bound X & (E-min X)`1 = E-bound X &
   (E-max X)`1 = E-bound X & (NE-corner X)`1 = E-bound X by Th76,Th78,Th104;
     (SE-corner X)`2 <= (E-min X)`2 &
   (SE-corner X)`2 <= (E-max X)`2 &
   (E-min X)`2 <= (NE-corner X)`2 &
   (E-max X)`2 <= (NE-corner X)`2 by Th107;
   then E-min X in LSeg(SE-corner X, NE-corner X) &
   E-max X in LSeg(SE-corner X, NE-corner X) by A1,GOBOARD7:8;
 hence thesis by TOPREAL1:12;
end;

theorem Th111:
E-min X in E-most X & E-max X in E-most X
proof
A1: E-most X = LSeg(SE-corner X, NE-corner X)/\X by Def40;
A2: E-min X = |[E-bound X, inf (proj2||E-most X)]| by Def47;
A3: E-max X = |[E-bound X, sup (proj2||E-most X)]| by Def46;
   set p2W = (proj2||E-most X), c = the carrier of (TOP-REAL 2)|E-most X;
A4: c = E-most X by JORDAN1:1;
A5: inf p2W = inf (p2W.:c) by Def20;
     p2W.:c is with_min by Def15;
   then inf (p2W.:c) in p2W.:c by Def4;
   then consider p being set such that
A6: p in c & p in c & inf (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A6;
A7: p2W.p = p`2 by A4,A6,Th70;
A8: p in LSeg(SE-corner X, NE-corner X) by A1,A4,A6,XBOOLE_0:def 3;
     (SE-corner X)`1 = E-bound X &
   (NE-corner X)`1 = E-bound X by Th76,Th78;
    then p`1 = E-bound X by A8,GOBOARD7:5;
 hence E-min X in E-most X by A2,A4,A5,A6,A7,EUCLID:57;
A9: sup p2W = sup (p2W.:c) by Def21;
     p2W.:c is with_max by Def14;
   then sup (p2W.:c) in p2W.:c by Def3;
   then consider p being set such that
A10: p in c & p in c & sup (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A10;
A11: p2W.p = p`2 by A4,A10,Th70;
A12: p in LSeg(SE-corner X, NE-corner X) by A1,A4,A10,XBOOLE_0:def 3;
     (SE-corner X)`1 = E-bound X &
   (NE-corner X)`1 = E-bound X by Th76,Th78;
     then p`1 = E-bound X by A12,GOBOARD7:5;
 hence E-max X in E-most X by A3,A4,A9,A10,A11,EUCLID:57;
end;

theorem
  LSeg(SE-corner X, E-min X)/\X = {E-min X} &
LSeg(E-max X, NE-corner X)/\X = {E-max X}
proof
A1: E-most X = LSeg(SE-corner X, NE-corner X)/\X by Def40;
   now let x be set;
  hereby
   assume A2: x in LSeg(SE-corner X, E-min X)/\X;
  then A3: x in LSeg(SE-corner X, E-min X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A2;
       (SE-corner X)`1 = (E-min X)`1 by Th105;
  then A4: p`1 = (E-min X)`1 by A3,GOBOARD7:5;
       (SE-corner X)`2 <= (E-min X)`2 by Th107;
  then A5: p`2 <= (E-min X)`2 by A3,TOPREAL1:10;
  A6: SE-corner X in LSeg(SE-corner X, NE-corner X) by TOPREAL1:6;
       E-min X in E-most X by Th111;
     then E-min X in LSeg(SE-corner X, NE-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(SE-corner X, E-min X) c= LSeg(SE-corner X, NE-corner X)
       by A6,TOPREAL1:12;
     then p in E-most X by A1,A3,XBOOLE_0:def 3;
     then (E-min X)`2 <= p`2 by Th108;
  then A7: p`2 = (E-min X)`2 by A5,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = E-min X by A4,A7,EUCLID:57;
  end;
  assume A8: x = E-min X;
       E-min X in E-most X by Th111;
  then A9: E-min X in X by A1,XBOOLE_0:def 3;
       E-min X in LSeg(SE-corner X, E-min X) by TOPREAL1:6;
  hence x in LSeg(SE-corner X, E-min X)/\X by A8,A9,XBOOLE_0:def 3;
 end;
 hence LSeg(SE-corner X, E-min X)/\X = {E-min X} by TARSKI:def 1;
   now let x be set;
  hereby
   assume A10: x in LSeg(E-max X, NE-corner X)/\X;
  then A11: x in LSeg(E-max X, NE-corner X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A10;
       (NE-corner X)`1 = (E-max X)`1 by Th105;
  then A12: p`1 = (E-max X)`1 by A11,GOBOARD7:5;
       (E-max X)`2 <= (NE-corner X)`2 by Th107;
  then A13: (E-max X)`2 <= p`2 by A11,TOPREAL1:10;
  A14: NE-corner X in LSeg(SE-corner X, NE-corner X) by TOPREAL1:6;
       E-max X in E-most X by Th111;
     then E-max X in LSeg(SE-corner X, NE-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(E-max X, NE-corner X) c= LSeg(SE-corner X, NE-corner X)
       by A14,TOPREAL1:12;
     then p in E-most X by A1,A11,XBOOLE_0:def 3;
     then p`2 <= (E-max X)`2 by Th108;
  then A15: p`2 = (E-max X)`2 by A13,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = E-max X by A12,A15,EUCLID:57;
  end;
  assume A16: x = E-max X;
       E-max X in E-most X by Th111;
  then A17: E-max X in X by A1,XBOOLE_0:def 3;
       E-max X in LSeg(E-max X, NE-corner X) by TOPREAL1:6;
  hence x in LSeg(E-max X, NE-corner X)/\X by A16,A17,XBOOLE_0:def 3;
 end;
 hence LSeg(E-max X, NE-corner X)/\X = {E-max X} by TARSKI:def 1;
end;

theorem
  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 Th109;
  then E-most X c= {E-min X} by TOPREAL1:7;
 hence E-most X = {E-min X} by ZFMISC_1:39;
end;

:: South

theorem Th114:
(S-min P)`2 = S-bound P &
(S-max P)`2 = S-bound P
proof SW-corner P = |[W-bound P, S-bound P]| &
  SE-corner P = |[E-bound P, S-bound P]| &
  S-min P = |[inf (proj1||S-most P), S-bound P]| &
  S-max P = |[sup (proj1||S-most P), S-bound P]|
     by Def34,Def37,Def48,Def49;
 hence thesis by EUCLID:56;
end;

theorem Th115:
(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 (SW-corner P)`2 = S-bound P & (S-min P)`2 = S-bound P &
 (S-max P)`2 = S-bound P & (SE-corner P)`2 = S-bound P by Th73,Th79,Th114;
 hence thesis;
end;

theorem Th116:
(S-min P)`1 = inf (proj1||S-most P) &
(S-max P)`1 = sup (proj1||S-most P)
proof
A1: S-min P = |[inf (proj1||S-most P), S-bound P]| by Def49;
A2: S-max P = |[sup (proj1||S-most P), S-bound P]| by Def48;
    set LP = S-most P;
 thus (S-min P)`1 = inf (proj1||LP) by A1,EUCLID:56;
 thus (S-max P)`1 = sup (proj1||LP) by A2,EUCLID:56;
end;

theorem Th117:
(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
A1: (SW-corner X)`1 = W-bound X by Th72 .= inf (proj1||X) by Def30;
    set LX = S-most X;
A2: (S-min X)`1 = inf (proj1||LX) by Th116;
A3: (S-max X)`1 = sup (proj1||LX) by Th116;
A4: (SE-corner X)`1 = E-bound X by Th78 .= sup (proj1||X) by Def32;
       S-most X = LSeg(SW-corner X, SE-corner X)/\X by Def41;
then A5: S-most X c= X by XBOOLE_1:17;
then A6: (SW-corner X)`1 <= (S-min X)`1 by A1,A2,Th62;
A7: (S-min X)`1 <= (S-max X)`1 by A2,A3,Th53;
A8: (S-max X)`1 <= (SE-corner X)`1 by A3,A4,A5,Th63;
  thus (SW-corner X)`1 <= (S-min X)`1 by A1,A2,A5,Th62;
  thus (SW-corner X)`1 <= (S-max X)`1 by A6,A7,AXIOMS:22;
  hence (SW-corner X)`1 <= (SE-corner X)`1 by A8,AXIOMS:22;
  thus (S-min X)`1 <= (S-max X)`1 by A2,A3,Th53;
  thus (S-min X)`1 <= (SE-corner X)`1 by A7,A8,AXIOMS:22;
  thus (S-max X)`1 <= (SE-corner X)`1 by A3,A4,A5,Th63;
end;

theorem Th118:
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 assume
A1: p in S-most Z;
   then p in LSeg(SW-corner Z, SE-corner Z)/\Z by Def41;
then A2: p in LSeg(SW-corner Z, SE-corner Z) & p in Z by XBOOLE_0:def 3;
  (SW-corner Z)`2 = S-bound Z & (S-min Z)`2 = S-bound Z &
   (S-max Z)`2 = S-bound Z & (SE-corner Z)`2 = S-bound Z by Th73,Th79,Th114;
 hence p`2 = (S-min Z)`2 by A2,GOBOARD7:6;
 assume Z is compact;
 then reconsider Z as non empty compact Subset of TOP-REAL 2;
    (S-min Z)`1 = inf (proj1||S-most Z) & (S-max Z)`1 = sup (proj1||S-most Z)
      by Th116;
 hence thesis by A1,Lm9;
end;

theorem Th119:
S-most X c= LSeg(S-min X, S-max X)
proof let x be set; assume
A1: x in S-most X;
   then reconsider p = x as Point of TOP-REAL 2;
A2: (S-min X)`2 = (S-max X)`2 by Th115;
     p`2 = (S-min X)`2 & (S-min X)`1 <= p`1 & p`1 <=(S-max X)`1 by A1,Th118;
 hence x in LSeg(S-min X, S-max X) by A2,GOBOARD7:9;
end;

theorem
  LSeg(S-min X, S-max X) c= LSeg(SW-corner X, SE-corner X)
proof
A1: (SW-corner X)`2 = S-bound X & (S-min X)`2 = S-bound X &
   (S-max X)`2 = S-bound X & (SE-corner X)`2 = S-bound X by Th73,Th79,Th114;
     (SW-corner X)`1 <= (S-min X)`1 &
   (SW-corner X)`1 <= (S-max X)`1 &
   (S-min X)`1 <= (SE-corner X)`1 &
   (S-max X)`1 <= (SE-corner X)`1 by Th117;
   then S-min X in LSeg(SW-corner X, SE-corner X) &
   S-max X in LSeg(SW-corner X, SE-corner X) by A1,GOBOARD7:9;
 hence thesis by TOPREAL1:12;
end;

theorem Th121:
S-min X in S-most X & S-max X in S-most X
proof
A1: S-most X = LSeg(SW-corner X, SE-corner X)/\X by Def41;
A2: S-min X = |[inf (proj1||S-most X), S-bound X]| by Def49;
A3: S-max X = |[sup (proj1||S-most X), S-bound X]| by Def48;
   set p2W = (proj1||S-most X), c = the carrier of (TOP-REAL 2)|S-most X;
A4: c = S-most X by JORDAN1:1;
A5: inf p2W = inf (p2W.:c) by Def20;
     p2W.:c is with_min by Def15;
   then inf (p2W.:c) in p2W.:c by Def4;
   then consider p being set such that
A6: p in c & p in c & inf (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A6;
A7: p2W.p = p`1 by A4,A6,Th69;
A8: p in LSeg(SW-corner X, SE-corner X) by A1,A4,A6,XBOOLE_0:def 3;
     (SW-corner X)`2 = S-bound X &
   (SE-corner X)`2 = S-bound X by Th73,Th79;
    then p`2 = S-bound X by A8,GOBOARD7:6;
 hence S-min X in S-most X by A2,A4,A5,A6,A7,EUCLID:57;
A9: sup p2W = sup (p2W.:c) by Def21;
     p2W.:c is with_max by Def14;
   then sup (p2W.:c) in p2W.:c by Def3;
   then consider p being set such that
A10: p in c & p in c & sup (p2W.:c) = p2W.p by FUNCT_2:115;
   reconsider p as Point of TOP-REAL 2 by A4,A10;
A11: p2W.p = p`1 by A4,A10,Th69;
A12: p in LSeg(SW-corner X, SE-corner X) by A1,A4,A10,XBOOLE_0:def 3;
     (SW-corner X)`2 = S-bound X &
   (SE-corner X)`2 = S-bound X by Th73,Th79;
     then p`2 = S-bound X by A12,GOBOARD7:6;
 hence S-max X in S-most X by A3,A4,A9,A10,A11,EUCLID:57;
end;

theorem
  LSeg(SW-corner X, S-min X)/\X = {S-min X} &
LSeg(S-max X, SE-corner X)/\X = {S-max X}
proof
A1: S-most X = LSeg(SW-corner X, SE-corner X)/\X by Def41;
   now let x be set;
  hereby
   assume A2: x in LSeg(SW-corner X, S-min X)/\X;
  then A3: x in LSeg(SW-corner X, S-min X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A2;
       (SW-corner X)`2 = (S-min X)`2 by Th115;
  then A4: p`2 = (S-min X)`2 by A3,GOBOARD7:6;
       (SW-corner X)`1 <= (S-min X)`1 by Th117;
  then A5: p`1 <= (S-min X)`1 by A3,TOPREAL1:9;
  A6: SW-corner X in LSeg(SW-corner X, SE-corner X) by TOPREAL1:6;
       S-min X in S-most X by Th121;
     then S-min X in LSeg(SW-corner X, SE-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(SW-corner X, S-min X) c= LSeg(SW-corner X, SE-corner X)
       by A6,TOPREAL1:12;
     then p in S-most X by A1,A3,XBOOLE_0:def 3;
     then (S-min X)`1 <= p`1 by Th118;
  then A7: p`1 = (S-min X)`1 by A5,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = S-min X by A4,A7,EUCLID:57;
  end;
  assume A8: x = S-min X;
       S-min X in S-most X by Th121;
  then A9: S-min X in X by A1,XBOOLE_0:def 3;
       S-min X in LSeg(SW-corner X, S-min X) by TOPREAL1:6;
  hence x in LSeg(SW-corner X, S-min X)/\X by A8,A9,XBOOLE_0:def 3;
 end;
 hence LSeg(SW-corner X, S-min X)/\X = {S-min X} by TARSKI:def 1;
   now let x be set;
  hereby
   assume A10: x in LSeg(S-max X, SE-corner X)/\X;
  then A11: x in LSeg(S-max X, SE-corner X) & x in X by XBOOLE_0:def 3;
     reconsider p = x as Point of TOP-REAL 2 by A10;
       (SE-corner X)`2 = (S-max X)`2 by Th115;
  then A12: p`2 = (S-max X)`2 by A11,GOBOARD7:6;
       (S-max X)`1 <= (SE-corner X)`1 by Th117;
  then A13: (S-max X)`1 <= p`1 by A11,TOPREAL1:9;
  A14: SE-corner X in LSeg(SW-corner X, SE-corner X) by TOPREAL1:6;
       S-max X in S-most X by Th121;
     then S-max X in LSeg(SW-corner X, SE-corner X) by A1,XBOOLE_0:def 3;
     then LSeg(S-max X, SE-corner X) c= LSeg(SW-corner X, SE-corner X)
       by A14,TOPREAL1:12;
     then p in S-most X by A1,A11,XBOOLE_0:def 3;
     then p`1 <= (S-max X)`1 by Th118;
  then A15: p`1 = (S-max X)`1 by A13,AXIOMS:21;
       p = |[p`1, p`2]| by EUCLID:57;
   hence x = S-max X by A12,A15,EUCLID:57;
  end;
  assume A16: x = S-max X;
       S-max X in S-most X by Th121;
  then A17: S-max X in X by A1,XBOOLE_0:def 3;
       S-max X in LSeg(S-max X, SE-corner X) by TOPREAL1:6;
  hence x in LSeg(S-max X, SE-corner X)/\X by A16,A17,XBOOLE_0:def 3;
 end;
 hence LSeg(S-max X, SE-corner X)/\X = {S-max X} by TARSKI:def 1;
end;

theorem
  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 Th119;
  then S-most X c= {S-min X} by TOPREAL1:7;
 hence S-most X = {S-min X} by ZFMISC_1:39;
end;

:: Degenerate cases

theorem
  W-max P = N-min P implies W-max P = NW-corner P
proof assume
A1: W-max P = N-min P;
A2: (W-max P)`1 = W-bound P & (N-min P)`2 = N-bound P &
   (NW-corner P)`1 = W-bound P & (NW-corner P)`2 = N-bound P
      by Th74,Th75,Th84,Th94;
     NW-corner P = |[(NW-corner P)`1, (NW-corner P)`2]| &
   W-max P = |[(W-max P)`1, (W-max P)`2]| by EUCLID:57;
 hence W-max P = NW-corner P by A1,A2;
end;

theorem
  N-max P = E-max P implies N-max P = NE-corner P
proof assume
A1: N-max P = E-max P;
A2: (N-max P)`2 = N-bound P & (E-max P)`1 = E-bound P &
   (NE-corner P)`1 = E-bound P & (NE-corner P)`2 = N-bound P
      by Th76,Th77,Th94,Th104;
     NE-corner P = |[(NE-corner P)`1, (NE-corner P)`2]| &
   N-max P = |[(N-max P)`1, (N-max P)`2]| by EUCLID:57;
 hence N-max P = NE-corner P by A1,A2;
end;

theorem
  E-min P = S-max P implies E-min P = SE-corner P
proof assume
A1: E-min P = S-max P;
A2: (E-min P)`1 = E-bound P & (S-max P)`2 = S-bound P &
   (SE-corner P)`1 = E-bound P & (SE-corner P)`2 = S-bound P
      by Th78,Th79,Th104,Th114;
     SE-corner P = |[(SE-corner P)`1, (SE-corner P)`2]| &
   E-min P = |[(E-min P)`1, (E-min P)`2]| by EUCLID:57;
 hence E-min P = SE-corner P by A1,A2;
end;

theorem
  S-min P = W-min P implies S-min P = SW-corner P
proof assume
A1: S-min P = W-min P;
A2: (S-min P)`2 = S-bound P & (W-min P)`1 = W-bound P &
   (SW-corner P)`1 = W-bound P & (SW-corner P)`2 = S-bound P
     by Th72,Th73,Th84,Th114;
     SW-corner P = |[(SW-corner P)`1, (SW-corner P)`2]| &
   S-min P = |[(S-min P)`1, (S-min P)`2]| by EUCLID:57;
 hence S-min P = SW-corner P by A1,A2;
end;

Back to top