The abstract of the Mizar article:

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

by

Czeslaw Bylinski, and

Piotr Rudnicki

Received July 29, 1997

MML identifier: PSCOMP_1

[ Mizar article, 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;


begin :: Preliminaries

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

definition
 cluster REAL -> with_zero;
 cluster NAT -> with_zero;
end;

definition
 cluster non empty without_zero set;
 cluster non empty with_zero set;
end;

definition
 cluster non empty without_zero Subset of REAL;
 cluster non empty with_zero Subset of REAL;
end;

theorem :: PSCOMP_1:1
 for F being set st F is non empty with_non-empty_elements c=-linear
  holds F is centered;

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

definition let A, B be set, f be Function of A, B;
 redefine func rng f -> Subset of B;
end;

definition let X, Y be non empty set, f be Function of X, Y;
   :: see WAYBEL_2
 cluster f.:X -> non empty;
end;

definition let X, Y be set, f be Function of X, Y;
 func "f -> Function of bool Y, bool X means
:: PSCOMP_1:def 2
 :: see FUNCT_3:def 2
 for y being Subset of Y holds it.y = f"y;
end;

theorem :: PSCOMP_1:2
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;

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

theorem :: PSCOMP_1:3
 abs r + abs s = 0 implies r = 0;

theorem :: PSCOMP_1:4
r < s & s < t implies abs s < abs r + abs t;

theorem :: PSCOMP_1:5
-s < r & r < s implies abs r < s;

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

theorem :: PSCOMP_1:6
seq is convergent & seq is_not_0 & lim seq = 0 implies seq" is non bounded;

theorem :: PSCOMP_1:7
rng seq is bounded iff seq is bounded;

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;
 redefine func inf X -> Element of REAL;
end;

theorem :: PSCOMP_1:8
 for X being non empty real-membered set
 for t st for s st s in X holds s >= t holds inf X >= t;

theorem :: PSCOMP_1:9
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;

theorem :: PSCOMP_1:10
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;

theorem :: PSCOMP_1:11
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;

theorem :: PSCOMP_1:12
 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;

theorem :: PSCOMP_1:13
 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;

definition let X be real-membered set;
 attr X is with_max means
:: PSCOMP_1:def 3
 X is bounded_above & sup X in X;
 attr X is with_min means
:: PSCOMP_1:def 4
 X is bounded_below & inf X in X;
end;

definition
 cluster non empty closed bounded Subset of REAL;
end;

definition let R be Subset-Family of REAL;
  attr R is open means
:: PSCOMP_1:def 5
 for X being Subset of REAL st X in R holds X is open;
  attr R is closed means
:: PSCOMP_1:def 6
 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
:: PSCOMP_1:def 7
 { -r3 : r3 in X};
 involutiveness;
end;

theorem :: PSCOMP_1:14
r in X iff -r in -X;

definition let X be non empty Subset of REAL;
 cluster -X -> non empty;
end;

theorem :: PSCOMP_1:15
X is bounded_above iff -X is bounded_below;

theorem :: PSCOMP_1:16
  X is bounded_below iff -X is bounded_above;

theorem :: PSCOMP_1:17
for X being non empty Subset of REAL
 st X is bounded_below holds inf X = - sup -X;

theorem :: PSCOMP_1:18
for X being non empty Subset of REAL
 st X is bounded_above holds sup X = - inf -X;

theorem :: PSCOMP_1:19
X is closed iff -X is closed;

definition let X be Subset of REAL, p be Real;
 func p+X -> Subset of REAL equals
:: PSCOMP_1:def 8
 { p+r3 : r3 in X};
end;

theorem :: PSCOMP_1:20
r in X iff q3+r in q3+X;

definition let X be non empty Subset of REAL, s be Real;
 cluster s+X -> non empty;
end;

theorem :: PSCOMP_1:21
X = 0+X;

theorem :: PSCOMP_1:22
q3+(p3+X) = (q3+p3)+X;

theorem :: PSCOMP_1:23
  X is bounded_above iff q3+X is bounded_above;

theorem :: PSCOMP_1:24
  X is bounded_below iff q3+X is bounded_below;

theorem :: PSCOMP_1:25
  for X being non empty Subset of REAL
 st X is bounded_below holds inf (q3+X) = q3+inf X;

theorem :: PSCOMP_1:26
  for X being non empty Subset of REAL
 st X is bounded_above holds sup (q3+X) = q3+sup X;

theorem :: PSCOMP_1:27
X is closed iff q3+X is closed;

definition let X be Subset of REAL;
 func Inv X -> Subset of REAL equals
:: PSCOMP_1:def 9
 { 1/r3 : r3 in X};
end;

theorem :: PSCOMP_1:28
for X being without_zero Subset of REAL holds r in X iff 1/r in Inv X;

definition let X be non empty without_zero Subset of REAL;
 cluster Inv X -> non empty without_zero;
end;

definition let X be without_zero Subset of REAL;
 cluster Inv X -> without_zero;
end;

theorem :: PSCOMP_1:29
for X being without_zero Subset of REAL holds Inv Inv X = X;

theorem :: PSCOMP_1:30
  for X being without_zero Subset of REAL
 st X is closed & X is bounded holds Inv X is closed;

theorem :: PSCOMP_1:31
 for Z being Subset-Family of REAL st Z is closed holds meet Z is closed;

definition let X be Subset of REAL;
 func Cl X -> Subset of REAL equals
:: PSCOMP_1:def 10
 meet { A where A is Element of bool REAL : X c= A & A is closed };
 projectivity;
end;

definition let X be Subset of REAL;
 cluster Cl X -> closed;
end;

theorem :: PSCOMP_1:32
 for Y being closed Subset of REAL st X c= Y holds Cl X c= Y;

theorem :: PSCOMP_1:33
X c= Cl X;

theorem :: PSCOMP_1:34
X is closed iff X = Cl X;

theorem :: PSCOMP_1:35
   Cl ({}REAL) = {};

theorem :: PSCOMP_1:36
   Cl ([#]REAL) = REAL;

theorem :: PSCOMP_1:37
  X c= Y implies Cl X c= Cl Y;

theorem :: PSCOMP_1:38
r3 in Cl X iff for O being open Subset of REAL st r3 in
 O holds O /\ X is non empty;

theorem :: PSCOMP_1:39
r3 in Cl X implies ex seq st rng seq c= X & seq is convergent & lim seq = r3;

begin :: Functions into Reals

definition let X be set, f be Function of X, REAL;
 redefine attr f is bounded_below means
:: PSCOMP_1:def 11
 f.:X is bounded_below;
 attr f is bounded_above means
:: PSCOMP_1:def 12
  f.:X is bounded_above;
end;

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

 attr f is with_max means
:: PSCOMP_1:def 14
 f.:X is with_max;
 attr f is with_min means
:: PSCOMP_1:def 15
 f.:X is with_min;
end;

definition let X be set, f be Function of X, REAL;
 func -f -> Function of X, REAL means
:: PSCOMP_1:def 16
 for p being set st p in X holds it.p = -(f.p);
 involutiveness;
end;

theorem :: PSCOMP_1:40
 for X, A being set, f being Function of X, REAL holds (-f).:A = -(f.:A);

theorem :: PSCOMP_1:41
for X being non empty set, f being Function of X, REAL
 holds f is with_min iff -f is with_max;

theorem :: PSCOMP_1:42
  for X being non empty set, f being Function of X, REAL
 holds f is with_max iff -f is with_min;

theorem :: PSCOMP_1:43
for X being set, A being Subset of REAL, f being Function of X, REAL
 holds (-f)"A = f"(-A);

definition let X be set, r be Real, f be Function of X, REAL;
 func r+f -> Function of X, REAL means
:: PSCOMP_1:def 17
 for p being set st p in X holds it.p = r+f.p;
end;

theorem :: PSCOMP_1:44
   for X, A being set, f being Function of X, REAL, s being Real
  holds (s+f).:A = s+(f.:A);

theorem :: PSCOMP_1:45
for X being set, A being Subset of REAL, f being Function of X, REAL, q3
 holds (q3+f)"A = f"(-q3+A);

definition let X be set, f be Function of X, REAL;
 func Inv f -> Function of X, REAL means
:: PSCOMP_1:def 18
 for p being set st p in X holds it.p = 1/(f.p);
 involutiveness;
end;

theorem :: PSCOMP_1:46
for X being set, A being without_zero Subset of REAL,
    f being Function of X, REAL holds (Inv f)"A = f"(Inv A);

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;
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
 for x being set st x in the carrier of X() ex r3 st P[x, r3];

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);

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

definition let T be 1-sorted, f be RealMap of T;
 func inf f -> Real equals
:: PSCOMP_1:def 20
 inf (f.:the carrier of T);
 func sup f -> Real equals
:: PSCOMP_1:def 21
 sup (f.:the carrier of T);
end;

theorem :: PSCOMP_1:47
for T being non empty TopSpace, f being bounded_below RealMap of T
 for p being Point of T holds f.p >= inf f;

theorem :: PSCOMP_1:48
  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;

theorem :: PSCOMP_1:49
  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;

theorem :: PSCOMP_1:50
for T being non empty TopSpace, f being bounded_above RealMap of T
 for p being Point of T holds f.p <= sup f;

theorem :: PSCOMP_1:51
  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;

theorem :: PSCOMP_1:52
  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;

theorem :: PSCOMP_1:53
 for T being non empty 1-sorted, f being bounded RealMap of T
  holds inf f <= sup f;

definition
 canceled 3;
end;

definition let T be TopStruct, f be RealMap of T;
 attr f is continuous means
:: PSCOMP_1:def 25
 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;
end;

definition let T be non empty TopSpace, S be non empty SubSpace of T;
 cluster continuous RealMap of S;
end;

 reserve T for TopStruct,
         f for RealMap of T;

theorem :: PSCOMP_1:54
f is continuous iff for Y being Subset of REAL st Y is open holds f"Y is open;

theorem :: PSCOMP_1:55
f is continuous implies -f is continuous;

theorem :: PSCOMP_1:56
f is continuous implies r3+f is continuous;

theorem :: PSCOMP_1:57
 f is continuous & not 0 in rng f implies Inv f is continuous;

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;
end;

theorem :: PSCOMP_1:58
  for R being Subset-Family of REAL
 st f is continuous & R is open holds ("f).:R is open;

theorem :: PSCOMP_1:59
for R being Subset-Family of REAL
 st f is continuous & R is closed holds ("f).:R is closed;

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
:: PSCOMP_1:def 26
 f|X;
end;

definition let T be non empty TopSpace;
 cluster compact non empty Subset of T;
end;

definition let T be non empty TopSpace, f be continuous RealMap of T,
               X be Subset of T;
 cluster f||X -> continuous;
end;

definition let T be non empty TopSpace, P be compact non empty Subset of T;
 cluster T|P -> compact;
end;

begin :: Pseudocompact spaces

theorem :: PSCOMP_1:60
 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);

theorem :: PSCOMP_1:61
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);

definition let T be TopStruct;
 attr T is pseudocompact means
:: PSCOMP_1:def 27

 for f being RealMap of T st f is continuous holds f is bounded;
end;

definition
 cluster compact -> pseudocompact (non empty TopSpace);
end;

definition
 cluster compact non empty TopSpace;
end;

definition let T be pseudocompact non empty TopSpace;
 cluster continuous -> bounded with_max with_min RealMap of T;
end;

theorem :: PSCOMP_1:62
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);

theorem :: PSCOMP_1:63
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);

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;
end;

theorem :: PSCOMP_1:64
for n being Nat, X, Y being compact Subset of TOP-REAL n
 holds X /\ Y is compact;

 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
:: PSCOMP_1:def 28
 for p being Point of TOP-REAL 2 holds it.p = p`1;
 func proj2 -> RealMap of TOP-REAL 2 means
:: PSCOMP_1:def 29
 for p being Point of TOP-REAL 2 holds it.p = p`2;
end;

theorem :: PSCOMP_1:65
proj1"].r,s.[ = {|[ r1, r2 ]| : r < r1 & r1 < s};

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

theorem :: PSCOMP_1:67
proj2"].r,s.[ = {|[ r1, r2 ]| : r < r2 & r2 < s};

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

definition
 cluster proj1 -> continuous;
 cluster proj2 -> continuous;
end;

theorem :: PSCOMP_1:69
 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;

theorem :: PSCOMP_1:70
 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;

definition let X be Subset of TOP-REAL 2;
 func W-bound X -> Real equals
:: PSCOMP_1:def 30
 inf (proj1||X);
 func N-bound X -> Real equals
:: PSCOMP_1:def 31
 sup (proj2||X);
 func E-bound X -> Real equals
:: PSCOMP_1:def 32
 sup (proj1||X);
 func S-bound X -> Real equals
:: PSCOMP_1:def 33
 inf (proj2||X);
end;

theorem :: PSCOMP_1:71
p in X implies W-bound X <= p`1 & p`1 <= E-bound X &
                 S-bound X <= p`2 & p`2 <= N-bound X;

definition let X be Subset of TOP-REAL 2;
 func SW-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 34
 |[W-bound X, S-bound X]|;
 func NW-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 35
 |[W-bound X, N-bound X]|;
 func NE-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 36
 |[E-bound X, N-bound X]|;
 func SE-corner X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 37
 |[E-bound X, S-bound X]|;
end;

:: Corners

theorem :: PSCOMP_1:72
(SW-corner P)`1 = W-bound P;

theorem :: PSCOMP_1:73
(SW-corner P)`2 = S-bound P;

theorem :: PSCOMP_1:74
(NW-corner P)`1 = W-bound P;

theorem :: PSCOMP_1:75
(NW-corner P)`2 = N-bound P;

theorem :: PSCOMP_1:76
(NE-corner P)`1 = E-bound P;

theorem :: PSCOMP_1:77
(NE-corner P)`2 = N-bound P;

theorem :: PSCOMP_1:78
(SE-corner P)`1 = E-bound P;

theorem :: PSCOMP_1:79
(SE-corner P)`2 = S-bound P;

theorem :: PSCOMP_1:80
  (SW-corner P)`1 = (NW-corner P)`1;

theorem :: PSCOMP_1:81
  (SE-corner P)`1 = (NE-corner P)`1;

theorem :: PSCOMP_1:82
  (NW-corner P)`2 = (NE-corner P)`2;

theorem :: PSCOMP_1:83
  (SW-corner P)`2 = (SE-corner P)`2;

definition let X be Subset of TOP-REAL 2;
 func W-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 38
 LSeg(SW-corner X, NW-corner X)/\X;
 func N-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 39
 LSeg(NW-corner X, NE-corner X)/\X;
 func E-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 40
 LSeg(SE-corner X, NE-corner X)/\X;
 func S-most X -> Subset of TOP-REAL 2 equals
:: PSCOMP_1:def 41
 LSeg(SW-corner X, SE-corner X)/\X;
end;

definition let X be non empty compact Subset of TOP-REAL 2;
 cluster W-most X -> non empty compact;
 cluster N-most X -> non empty compact;
 cluster E-most X -> non empty compact;
 cluster S-most X -> non empty compact;
end;

definition let X be Subset of TOP-REAL 2;
 func W-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 42
 |[W-bound X, inf (proj2||W-most X)]|;
 func W-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 43
 |[W-bound X, sup (proj2||W-most X)]|;
 func N-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 44
 |[inf (proj1||N-most X), N-bound X]|;
 func N-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 45
 |[sup (proj1||N-most X), N-bound X]|;
 func E-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 46
 |[E-bound X, sup (proj2||E-most X)]|;
 func E-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 47
 |[E-bound X, inf (proj2||E-most X)]|;
 func S-max X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 48
 |[sup (proj1||S-most X), S-bound X]|;
 func S-min X -> Point of TOP-REAL 2 equals
:: PSCOMP_1:def 49
 |[inf (proj1||S-most X), S-bound X]|;
end;

theorem :: PSCOMP_1:84
(W-min P)`1 = W-bound P &
(W-max P)`1 = W-bound P;

theorem :: PSCOMP_1:85
(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;

theorem :: PSCOMP_1:86
(W-min P)`2 = inf (proj2||W-most P) &
(W-max P)`2 = sup (proj2||W-most P);

theorem :: PSCOMP_1:87
(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;

theorem :: PSCOMP_1:88
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);

theorem :: PSCOMP_1:89
W-most X c= LSeg(W-min X, W-max X);

theorem :: PSCOMP_1:90
  LSeg(W-min X, W-max X) c= LSeg(SW-corner X, NW-corner X);

theorem :: PSCOMP_1:91
W-min X in W-most X & W-max X in W-most X;

theorem :: PSCOMP_1:92
  LSeg(SW-corner X, W-min X)/\X = {W-min X} &
LSeg(W-max X, NW-corner X)/\X = {W-max X};

theorem :: PSCOMP_1:93
  W-min X = W-max X implies W-most X = {W-min X};

:: North

theorem :: PSCOMP_1:94
(N-min P)`2 = N-bound P &
(N-max P)`2 = N-bound P;

theorem :: PSCOMP_1:95
(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;

theorem :: PSCOMP_1:96
(N-min P)`1 = inf (proj1||N-most P) &
(N-max P)`1 = sup (proj1||N-most P);

theorem :: PSCOMP_1:97
(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;

theorem :: PSCOMP_1:98
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);

theorem :: PSCOMP_1:99
N-most X c= LSeg(N-min X, N-max X);

theorem :: PSCOMP_1:100
  LSeg(N-min X, N-max X) c= LSeg(NW-corner X, NE-corner X);

theorem :: PSCOMP_1:101
N-min X in N-most X & N-max X in N-most X;

theorem :: PSCOMP_1:102
  LSeg(NW-corner X, N-min X)/\X = {N-min X} &
LSeg(N-max X, NE-corner X)/\X = {N-max X};

theorem :: PSCOMP_1:103
  N-min X = N-max X implies N-most X = {N-min X};

:: East

theorem :: PSCOMP_1:104
(E-min P)`1 = E-bound P &
(E-max P)`1 = E-bound P;

theorem :: PSCOMP_1:105
(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;

theorem :: PSCOMP_1:106
(E-min P)`2 = inf (proj2||E-most P) &
(E-max P)`2 = sup (proj2||E-most P);

theorem :: PSCOMP_1:107
(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;

theorem :: PSCOMP_1:108
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);

theorem :: PSCOMP_1:109
E-most X c= LSeg(E-min X, E-max X);

theorem :: PSCOMP_1:110
  LSeg(E-min X, E-max X) c= LSeg(SE-corner X, NE-corner X);

theorem :: PSCOMP_1:111
E-min X in E-most X & E-max X in E-most X;

theorem :: PSCOMP_1:112
  LSeg(SE-corner X, E-min X)/\X = {E-min X} &
LSeg(E-max X, NE-corner X)/\X = {E-max X};

theorem :: PSCOMP_1:113
  E-min X = E-max X implies E-most X = {E-min X};

:: South

theorem :: PSCOMP_1:114
(S-min P)`2 = S-bound P &
(S-max P)`2 = S-bound P;

theorem :: PSCOMP_1:115
(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;

theorem :: PSCOMP_1:116
(S-min P)`1 = inf (proj1||S-most P) &
(S-max P)`1 = sup (proj1||S-most P);

theorem :: PSCOMP_1:117
(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;

theorem :: PSCOMP_1:118
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);

theorem :: PSCOMP_1:119
S-most X c= LSeg(S-min X, S-max X);

theorem :: PSCOMP_1:120
  LSeg(S-min X, S-max X) c= LSeg(SW-corner X, SE-corner X);

theorem :: PSCOMP_1:121
S-min X in S-most X & S-max X in S-most X;

theorem :: PSCOMP_1:122
  LSeg(SW-corner X, S-min X)/\X = {S-min X} &
LSeg(S-max X, SE-corner X)/\X = {S-max X};

theorem :: PSCOMP_1:123
  S-min X = S-max X implies S-most X = {S-min X};

:: Degenerate cases

theorem :: PSCOMP_1:124
  W-max P = N-min P implies W-max P = NW-corner P;

theorem :: PSCOMP_1:125
  N-max P = E-max P implies N-max P = NE-corner P;

theorem :: PSCOMP_1:126
  E-min P = S-max P implies E-min P = SE-corner P;

theorem :: PSCOMP_1:127
  S-min P = W-min P implies S-min P = SW-corner P;