:: Bounding boxes for compact sets in ${\calE}^2$
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

Lm1:  for X being Subset of REAL st X is bounded_below holds
-- X is bounded_above
proofend;

Lm2:  for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max
proofend;

begin

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

registration
let T be non empty 1-sorted ;
cluster non empty Relation-like the carrier of T -defined REAL -valued Function-like V29( the carrier of T) V30( the carrier of T, REAL ) complex-valued ext-real-valued real-valued bounded for Element of K32(K33( the carrier of T,REAL));
existence
 ex b1 being RealMap of T st b1 is bounded
proofend;
end;

definition
let T be 1-sorted ;
let f be RealMap of T;
func lower_bound f ->  Real equals :: PSCOMP_1:def 1
 lower_bound (f .: the carrier of T);
coherence
 lower_bound (f .: the carrier of T) is Real ;
func upper_bound f ->  Real equals :: PSCOMP_1:def 2
 upper_bound (f .: the carrier of T);
coherence
 upper_bound (f .: the carrier of T) is Real ;
end;

:: deftheorem  defines lower_bound PSCOMP_1:def_1_:_
 for T being 1-sorted
for f being RealMap of T holds lower_bound f = lower_bound (f .: the carrier of T);

:: deftheorem  defines upper_bound PSCOMP_1:def_2_:_
 for T being 1-sorted
for f being RealMap of T holds upper_bound f = upper_bound (f .: the carrier of T);

theorem Th1: :: PSCOMP_1:1
for T being non empty TopSpace
for f being V44() RealMap of T
for p being Point of T holds f . p >= lower_bound f
proofend;

theorem :: PSCOMP_1:2
for T being non empty TopSpace
for f being V44() RealMap of T
for s being Real st ( for t being Point of T holds f . t >= s ) holds
lower_bound f >= s
proofend;

theorem :: PSCOMP_1:3
for r being real number
for T being non empty TopSpace
for f being RealMap of T st ( for p being Point of T holds f . p >= r ) & ( for t being real number st ( for p being Point of T holds f . p >= t ) holds
r >= t ) holds
r = lower_bound f
proofend;

theorem Th4: :: PSCOMP_1:4
for T being non empty TopSpace
for f being V43() RealMap of T
for p being Point of T holds f . p <= upper_bound f
proofend;

theorem :: PSCOMP_1:5
for T being non empty TopSpace
for f being V43() RealMap of T
for t being real number st ( for p being Point of T holds f . p <= t ) holds
upper_bound f <= t
proofend;

theorem :: PSCOMP_1:6
for r being real number
for T being non empty TopSpace
for f being RealMap of T st ( for p being Point of T holds f . p <= r ) &amp; ( for t being real number st ( for p being Point of T holds f . p <= t ) holds
r <= t ) holds
r = upper_bound f
proofend;

theorem Th7: :: PSCOMP_1:7
for T being non empty 1-sorted
for f being bounded RealMap of T holds lower_bound f <= upper_bound f
proofend;

definition
let T be TopStruct ;
let f be RealMap of T;
attrf is continuous  means :Def3: :: PSCOMP_1:def 3
 for Y being Subset of REAL st Y is closed holds
f " Y is closed ;
end;

:: deftheorem Def3 defines continuous PSCOMP_1:def_3_:_
 for T being TopStruct
for f being RealMap of T holds
( f is continuous iff for Y being Subset of REAL st Y is closed holds
f " Y is closed );

registration
let T be non empty TopSpace;
cluster non empty Relation-like the carrier of T -defined REAL -valued Function-like V29( the carrier of T) V30( the carrier of T, REAL ) complex-valued ext-real-valued real-valued continuous for Element of K32(K33( the carrier of T,REAL));
existence
 ex b1 being RealMap of T st b1 is continuous
proofend;
end;

registration
let T be non empty TopSpace;
let S be non empty SubSpace of T;
cluster non empty Relation-like the carrier of S -defined REAL -valued Function-like V29( the carrier of S) V30( the carrier of S, REAL ) complex-valued ext-real-valued real-valued continuous for Element of K32(K33( the carrier of S,REAL));
existence
 ex b1 being RealMap of S st b1 is continuous
proofend;
end;

theorem Th8: :: PSCOMP_1:8
for T being TopStruct
for f being RealMap of T holds
( f is continuous iff for Y being Subset of REAL st Y is open holds
f " Y is open )
proofend;

theorem Th9: :: PSCOMP_1:9
for T being TopStruct
for f being RealMap of T st f is continuous holds
- f is continuous
proofend;

theorem Th10: :: PSCOMP_1:10
for r3 being Real
for T being TopStruct
for f being RealMap of T st f is continuous holds
r3 + f is continuous
proofend;

theorem Th11: :: PSCOMP_1:11
for T being TopStruct
for f being RealMap of T st f is continuous &amp; not 0 in rng f holds
Inv f is continuous
proofend;

theorem :: PSCOMP_1:12
for T being TopStruct
for f being RealMap of T
for R being Subset-Family of REAL st f is continuous &amp; R is open holds
(" f) .: R is open
proofend;

theorem Th13: :: PSCOMP_1:13
for T being TopStruct
for f being RealMap of T
for R being Subset-Family of REAL st f is continuous &amp; R is closed holds
(" f) .: R is closed
proofend;

definition
let T be non empty TopStruct ;
let f be RealMap of T;
let X be Subset of T;
:: original:|
redefine funcf | X ->  RealMap of (T | X);
coherence
 f | X is RealMap of (T | X)
proofend;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let X be Subset of T;
clusterf | X ->  continuous for RealMap of (T | X);
coherence
 for b1 being RealMap of (T | X) st b1 = f | X holds
b1 is continuous
proofend;
end;

registration
let T be non empty TopSpace;
let P be non empty compact Subset of T;
clusterT | P ->  compact ;
coherence
 T | P is compact by COMPTS_1:3;
end;

begin

theorem Th14: :: PSCOMP_1:14
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 )
proofend;

theorem Th15: :: PSCOMP_1:15
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 )
proofend;

definition
let T be TopStruct ;
attrT is pseudocompact  means :Def4: :: PSCOMP_1:def 4
 for f being RealMap of T st f is continuous holds
f is bounded ;
end;

:: deftheorem Def4 defines pseudocompact PSCOMP_1:def_4_:_
 for T being TopStruct holds
( T is pseudocompact iff for f being RealMap of T st f is continuous holds
f is bounded );

registration
cluster non empty TopSpace-like compact  ->  non empty pseudocompact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is compact holds
b1 is pseudocompact
proofend;
end;

registration
cluster non empty TopSpace-like compact for TopStruct ;
existence
 ex b1 being TopSpace st
( not b1 is empty &amp; b1 is compact )
proofend;
end;

registration
let T be non empty pseudocompact TopSpace;
cluster Function-like V30( the carrier of T, REAL ) continuous  ->  with_max with_min bounded for Element of K32(K33( the carrier of T,REAL));
coherence
 for b1 being RealMap of T st b1 is continuous holds
( b1 is bounded &amp; b1 is with_max &amp; b1 is with_min )
proofend;
end;

theorem Th16: :: PSCOMP_1:16
for T being non empty TopSpace
for X being non empty Subset of T
for Y being compact Subset of T
for f being continuous RealMap of T st X c= Y holds
lower_bound (f | Y) <= lower_bound (f | X)
proofend;

theorem Th17: :: PSCOMP_1:17
for T being non empty TopSpace
for X being non empty Subset of T
for Y being compact Subset of T
for f being continuous RealMap of T st X c= Y holds
upper_bound (f | X) <= upper_bound (f | Y)
proofend;

begin

registration
let n be Element of NAT ;
let X, Y be compact Subset of (TOP-REAL n);
clusterX /\ Y ->  compact for Subset of (TOP-REAL n);
coherence
 for b1 being Subset of (TOP-REAL n) st b1 = X /\ Y holds
b1 is compact by COMPTS_1:11;
end;

definition
func proj1  ->  RealMap of (TOP-REAL 2) means :Def5: :: PSCOMP_1:def 5
 for p being Point of (TOP-REAL 2) holds it . p = p `1 ;
existence
 ex b1 being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds b1 . p = p `1
proofend;
uniqueness
 for b1, b2 being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = p `1 ) &amp; ( for p being Point of (TOP-REAL 2) holds b2 . p = p `1 ) holds
b1 = b2
proofend;
func proj2  ->  RealMap of (TOP-REAL 2) means :Def6: :: PSCOMP_1:def 6
 for p being Point of (TOP-REAL 2) holds it . p = p `2 ;
existence
 ex b1 being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds b1 . p = p `2
proofend;
uniqueness
 for b1, b2 being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = p `2 ) &amp; ( for p being Point of (TOP-REAL 2) holds b2 . p = p `2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines proj1 PSCOMP_1:def_5_:_
 for b1 being RealMap of (TOP-REAL 2) holds
( b1 = proj1 iff for p being Point of (TOP-REAL 2) holds b1 . p = p `1 );

:: deftheorem Def6 defines proj2 PSCOMP_1:def_6_:_
 for b1 being RealMap of (TOP-REAL 2) holds
( b1 = proj2 iff for p being Point of (TOP-REAL 2) holds b1 . p = p `2 );

theorem Th18: :: PSCOMP_1:18
for r, s being real number holds proj1 " ].r,s.[ =  {  |[r1,r2]| where r1, r2 is Real : ( r < r1 &amp; r1 < s )  }
proofend;

theorem Th19: :: PSCOMP_1:19
for P being Subset of (TOP-REAL 2)
for r3, q3 being Real st P =  {  |[r1,r2]| where r1, r2 is Real : ( r3 < r1 &amp; r1 < q3 )  }  holds
P is open
proofend;

theorem Th20: :: PSCOMP_1:20
for r, s being real number holds proj2 " ].r,s.[ =  {  |[r1,r2]| where r1, r2 is Real : ( r < r2 &amp; r2 < s )  }
proofend;

theorem Th21: :: PSCOMP_1:21
for P being Subset of (TOP-REAL 2)
for r3, q3 being Real st P =  {  |[r1,r2]| where r1, r2 is Real : ( r3 < r2 &amp; r2 < q3 )  }  holds
P is open
proofend;

registration
cluster proj1  ->  continuous ;
coherence
 proj1 is continuous
proofend;
cluster proj2  ->  continuous ;
coherence
 proj2 is continuous
proofend;
end;

theorem Th22: :: PSCOMP_1:22
for X being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in X holds
(proj1 | X) . p = p `1
proofend;

theorem Th23: :: PSCOMP_1:23
for X being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in X holds
(proj2 | X) . p = p `2
proofend;

definition
let X be Subset of (TOP-REAL 2);
func W-bound X ->  Real equals :: PSCOMP_1:def 7
 lower_bound (proj1 | X);
coherence
 lower_bound (proj1 | X) is Real ;
func N-bound X ->  Real equals :: PSCOMP_1:def 8
 upper_bound (proj2 | X);
coherence
 upper_bound (proj2 | X) is Real ;
func E-bound X ->  Real equals :: PSCOMP_1:def 9
 upper_bound (proj1 | X);
coherence
 upper_bound (proj1 | X) is Real ;
func S-bound X ->  Real equals :: PSCOMP_1:def 10
 lower_bound (proj2 | X);
coherence
 lower_bound (proj2 | X) is Real ;
end;

:: deftheorem  defines W-bound PSCOMP_1:def_7_:_
 for X being Subset of (TOP-REAL 2) holds W-bound X = lower_bound (proj1 | X);

:: deftheorem  defines N-bound PSCOMP_1:def_8_:_
 for X being Subset of (TOP-REAL 2) holds N-bound X = upper_bound (proj2 | X);

:: deftheorem  defines E-bound PSCOMP_1:def_9_:_
 for X being Subset of (TOP-REAL 2) holds E-bound X = upper_bound (proj1 | X);

:: deftheorem  defines S-bound PSCOMP_1:def_10_:_
 for X being Subset of (TOP-REAL 2) holds S-bound X = lower_bound (proj2 | X);

Lm3:  for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( lower_bound (proj1 | X) <= p `1 &amp; p `1 <= upper_bound (proj1 | X) &amp; lower_bound (proj2 | X) <= p `2 &amp; p `2 <= upper_bound (proj2 | X) )
proofend;

theorem :: PSCOMP_1:24
for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( W-bound X <= p `1 &amp; p `1 <= E-bound X &amp; S-bound X <= p `2 &amp; p `2 <= N-bound X ) by Lm3;

definition
let X be Subset of (TOP-REAL 2);
func SW-corner X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 11
|[(W-bound X),(S-bound X)]|;
coherence
 |[(W-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;
func NW-corner X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 12
|[(W-bound X),(N-bound X)]|;
coherence
 |[(W-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;
func NE-corner X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 13
|[(E-bound X),(N-bound X)]|;
coherence
 |[(E-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;
func SE-corner X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 14
|[(E-bound X),(S-bound X)]|;
coherence
 |[(E-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;
end;

:: deftheorem  defines SW-corner PSCOMP_1:def_11_:_
 for X being Subset of (TOP-REAL 2) holds SW-corner X = |[(W-bound X),(S-bound X)]|;

:: deftheorem  defines NW-corner PSCOMP_1:def_12_:_
 for X being Subset of (TOP-REAL 2) holds NW-corner X = |[(W-bound X),(N-bound X)]|;

:: deftheorem  defines NE-corner PSCOMP_1:def_13_:_
 for X being Subset of (TOP-REAL 2) holds NE-corner X = |[(E-bound X),(N-bound X)]|;

:: deftheorem  defines SE-corner PSCOMP_1:def_14_:_
 for X being Subset of (TOP-REAL 2) holds SE-corner X = |[(E-bound X),(S-bound X)]|;

theorem :: PSCOMP_1:25
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `1 = (NW-corner P) `1
proofend;

theorem :: PSCOMP_1:26
for P being Subset of (TOP-REAL 2) holds (SE-corner P) `1 = (NE-corner P) `1
proofend;

theorem :: PSCOMP_1:27
for P being Subset of (TOP-REAL 2) holds (NW-corner P) `2 = (NE-corner P) `2
proofend;

theorem :: PSCOMP_1:28
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `2 = (SE-corner P) `2
proofend;

definition
let X be Subset of (TOP-REAL 2);
func W-most X ->  Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 15
(LSeg ((SW-corner X),(NW-corner X))) /\ X;
coherence
 (LSeg ((SW-corner X),(NW-corner X))) /\ X is Subset of (TOP-REAL 2) ;
func N-most X ->  Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 16
(LSeg ((NW-corner X),(NE-corner X))) /\ X;
coherence
 (LSeg ((NW-corner X),(NE-corner X))) /\ X is Subset of (TOP-REAL 2) ;
func E-most X ->  Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 17
(LSeg ((SE-corner X),(NE-corner X))) /\ X;
coherence
 (LSeg ((SE-corner X),(NE-corner X))) /\ X is Subset of (TOP-REAL 2) ;
func S-most X ->  Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 18
(LSeg ((SW-corner X),(SE-corner X))) /\ X;
coherence
 (LSeg ((SW-corner X),(SE-corner X))) /\ X is Subset of (TOP-REAL 2) ;
end;

:: deftheorem  defines W-most PSCOMP_1:def_15_:_
 for X being Subset of (TOP-REAL 2) holds W-most X = (LSeg ((SW-corner X),(NW-corner X))) /\ X;

:: deftheorem  defines N-most PSCOMP_1:def_16_:_
 for X being Subset of (TOP-REAL 2) holds N-most X = (LSeg ((NW-corner X),(NE-corner X))) /\ X;

:: deftheorem  defines E-most PSCOMP_1:def_17_:_
 for X being Subset of (TOP-REAL 2) holds E-most X = (LSeg ((SE-corner X),(NE-corner X))) /\ X;

:: deftheorem  defines S-most PSCOMP_1:def_18_:_
 for X being Subset of (TOP-REAL 2) holds S-most X = (LSeg ((SW-corner X),(SE-corner X))) /\ X;

registration
let X be non empty compact Subset of (TOP-REAL 2);
cluster W-most X ->  non empty compact ;
coherence
 ( not W-most X is empty &amp; W-most X is compact )
proofend;
cluster N-most X ->  non empty compact ;
coherence
 ( not N-most X is empty &amp; N-most X is compact )
proofend;
cluster E-most X ->  non empty compact ;
coherence
 ( not E-most X is empty &amp; E-most X is compact )
proofend;
cluster S-most X ->  non empty compact ;
coherence
 ( not S-most X is empty &amp; S-most X is compact )
proofend;
end;

definition
let X be Subset of (TOP-REAL 2);
func W-min X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 19
|[(W-bound X),(lower_bound (proj2 | (W-most X)))]|;
coherence
 |[(W-bound X),(lower_bound (proj2 | (W-most X)))]| is Point of (TOP-REAL 2) ;
func W-max X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 20
|[(W-bound X),(upper_bound (proj2 | (W-most X)))]|;
coherence
 |[(W-bound X),(upper_bound (proj2 | (W-most X)))]| is Point of (TOP-REAL 2) ;
func N-min X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 21
|[(lower_bound (proj1 | (N-most X))),(N-bound X)]|;
coherence
 |[(lower_bound (proj1 | (N-most X))),(N-bound X)]| is Point of (TOP-REAL 2) ;
func N-max X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 22
|[(upper_bound (proj1 | (N-most X))),(N-bound X)]|;
coherence
 |[(upper_bound (proj1 | (N-most X))),(N-bound X)]| is Point of (TOP-REAL 2) ;
func E-max X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 23
|[(E-bound X),(upper_bound (proj2 | (E-most X)))]|;
coherence
 |[(E-bound X),(upper_bound (proj2 | (E-most X)))]| is Point of (TOP-REAL 2) ;
func E-min X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 24
|[(E-bound X),(lower_bound (proj2 | (E-most X)))]|;
coherence
 |[(E-bound X),(lower_bound (proj2 | (E-most X)))]| is Point of (TOP-REAL 2) ;
func S-max X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 25
|[(upper_bound (proj1 | (S-most X))),(S-bound X)]|;
coherence
 |[(upper_bound (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2) ;
func S-min X ->  Point of (TOP-REAL 2) equals :: PSCOMP_1:def 26
|[(lower_bound (proj1 | (S-most X))),(S-bound X)]|;
coherence
 |[(lower_bound (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2) ;
end;

:: deftheorem  defines W-min PSCOMP_1:def_19_:_
 for X being Subset of (TOP-REAL 2) holds W-min X = |[(W-bound X),(lower_bound (proj2 | (W-most X)))]|;

:: deftheorem  defines W-max PSCOMP_1:def_20_:_
 for X being Subset of (TOP-REAL 2) holds W-max X = |[(W-bound X),(upper_bound (proj2 | (W-most X)))]|;

:: deftheorem  defines N-min PSCOMP_1:def_21_:_
 for X being Subset of (TOP-REAL 2) holds N-min X = |[(lower_bound (proj1 | (N-most X))),(N-bound X)]|;

:: deftheorem  defines N-max PSCOMP_1:def_22_:_
 for X being Subset of (TOP-REAL 2) holds N-max X = |[(upper_bound (proj1 | (N-most X))),(N-bound X)]|;

:: deftheorem  defines E-max PSCOMP_1:def_23_:_
 for X being Subset of (TOP-REAL 2) holds E-max X = |[(E-bound X),(upper_bound (proj2 | (E-most X)))]|;

:: deftheorem  defines E-min PSCOMP_1:def_24_:_
 for X being Subset of (TOP-REAL 2) holds E-min X = |[(E-bound X),(lower_bound (proj2 | (E-most X)))]|;

:: deftheorem  defines S-max PSCOMP_1:def_25_:_
 for X being Subset of (TOP-REAL 2) holds S-max X = |[(upper_bound (proj1 | (S-most X))),(S-bound X)]|;

:: deftheorem  defines S-min PSCOMP_1:def_26_:_
 for X being Subset of (TOP-REAL 2) holds S-min X = |[(lower_bound (proj1 | (S-most X))),(S-bound X)]|;

theorem Th29: :: PSCOMP_1:29
for P being Subset of (TOP-REAL 2) holds
( (SW-corner P) `1 = (W-min P) `1 &amp; (SW-corner P) `1 = (W-max P) `1 &amp; (W-min P) `1 = (W-max P) `1 &amp; (W-min P) `1 = (NW-corner P) `1 &amp; (W-max P) `1 = (NW-corner P) `1 )
proofend;

theorem Th30: :: PSCOMP_1:30
for X being non empty compact Subset of (TOP-REAL 2) holds
( (SW-corner X) `2 <= (W-min X) `2 &amp; (SW-corner X) `2 <= (W-max X) `2 &amp; (SW-corner X) `2 <= (NW-corner X) `2 &amp; (W-min X) `2 <= (W-max X) `2 &amp; (W-min X) `2 <= (NW-corner X) `2 &amp; (W-max X) `2 <= (NW-corner X) `2 )
proofend;

theorem Th31: :: PSCOMP_1:31
for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in W-most Z holds
( p `1 = (W-min Z) `1 &amp; ( Z is compact implies ( (W-min Z) `2 <= p `2 &amp; p `2 <= (W-max Z) `2 ) ) )
proofend;

theorem Th32: :: PSCOMP_1:32
for X being non empty compact Subset of (TOP-REAL 2) holds W-most X c= LSeg ((W-min X),(W-max X))
proofend;

theorem :: PSCOMP_1:33
for X being non empty compact Subset of (TOP-REAL 2) holds LSeg ((W-min X),(W-max X)) c= LSeg ((SW-corner X),(NW-corner X))
proofend;

theorem Th34: :: PSCOMP_1:34
for X being non empty compact Subset of (TOP-REAL 2) holds
( W-min X in W-most X &amp; W-max X in W-most X )
proofend;

theorem :: PSCOMP_1:35
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg ((SW-corner X),(W-min X))) /\ X = {(W-min X)} &amp; (LSeg ((W-max X),(NW-corner X))) /\ X = {(W-max X)} )
proofend;

theorem :: PSCOMP_1:36
for X being non empty compact Subset of (TOP-REAL 2) st W-min X = W-max X holds
W-most X = {(W-min X)}
proofend;

theorem Th37: :: PSCOMP_1:37
for P being Subset of (TOP-REAL 2) holds
( (NW-corner P) `2 = (N-min P) `2 &amp; (NW-corner P) `2 = (N-max P) `2 &amp; (N-min P) `2 = (N-max P) `2 &amp; (N-min P) `2 = (NE-corner P) `2 &amp; (N-max P) `2 = (NE-corner P) `2 )
proofend;

theorem Th38: :: PSCOMP_1:38
for X being non empty compact Subset of (TOP-REAL 2) holds
( (NW-corner X) `1 <= (N-min X) `1 &amp; (NW-corner X) `1 <= (N-max X) `1 &amp; (NW-corner X) `1 <= (NE-corner X) `1 &amp; (N-min X) `1 <= (N-max X) `1 &amp; (N-min X) `1 <= (NE-corner X) `1 &amp; (N-max X) `1 <= (NE-corner X) `1 )
proofend;

theorem Th39: :: PSCOMP_1:39
for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in N-most Z holds
( p `2 = (N-min Z) `2 &amp; ( Z is compact implies ( (N-min Z) `1 <= p `1 &amp; p `1 <= (N-max Z) `1 ) ) )
proofend;

theorem Th40: :: PSCOMP_1:40
for X being non empty compact Subset of (TOP-REAL 2) holds N-most X c= LSeg ((N-min X),(N-max X))
proofend;

theorem :: PSCOMP_1:41
for X being non empty compact Subset of (TOP-REAL 2) holds LSeg ((N-min X),(N-max X)) c= LSeg ((NW-corner X),(NE-corner X))
proofend;

theorem Th42: :: PSCOMP_1:42
for X being non empty compact Subset of (TOP-REAL 2) holds
( N-min X in N-most X &amp; N-max X in N-most X )
proofend;

theorem :: PSCOMP_1:43
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg ((NW-corner X),(N-min X))) /\ X = {(N-min X)} &amp; (LSeg ((N-max X),(NE-corner X))) /\ X = {(N-max X)} )
proofend;

theorem :: PSCOMP_1:44
for X being non empty compact Subset of (TOP-REAL 2) st N-min X = N-max X holds
N-most X = {(N-min X)}
proofend;

theorem Th45: :: PSCOMP_1:45
for P being Subset of (TOP-REAL 2) holds
( (SE-corner P) `1 = (E-min P) `1 &amp; (SE-corner P) `1 = (E-max P) `1 &amp; (E-min P) `1 = (E-max P) `1 &amp; (E-min P) `1 = (NE-corner P) `1 &amp; (E-max P) `1 = (NE-corner P) `1 )
proofend;

theorem Th46: :: PSCOMP_1:46
for X being non empty compact Subset of (TOP-REAL 2) holds
( (SE-corner X) `2 <= (E-min X) `2 &amp; (SE-corner X) `2 <= (E-max X) `2 &amp; (SE-corner X) `2 <= (NE-corner X) `2 &amp; (E-min X) `2 <= (E-max X) `2 &amp; (E-min X) `2 <= (NE-corner X) `2 &amp; (E-max X) `2 <= (NE-corner X) `2 )
proofend;

theorem Th47: :: PSCOMP_1:47
for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in E-most Z holds
( p `1 = (E-min Z) `1 &amp; ( Z is compact implies ( (E-min Z) `2 <= p `2 &amp; p `2 <= (E-max Z) `2 ) ) )
proofend;

theorem Th48: :: PSCOMP_1:48
for X being non empty compact Subset of (TOP-REAL 2) holds E-most X c= LSeg ((E-min X),(E-max X))
proofend;

theorem :: PSCOMP_1:49
for X being non empty compact Subset of (TOP-REAL 2) holds LSeg ((E-min X),(E-max X)) c= LSeg ((SE-corner X),(NE-corner X))
proofend;

theorem Th50: :: PSCOMP_1:50
for X being non empty compact Subset of (TOP-REAL 2) holds
( E-min X in E-most X &amp; E-max X in E-most X )
proofend;

theorem :: PSCOMP_1:51
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg ((SE-corner X),(E-min X))) /\ X = {(E-min X)} &amp; (LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)} )
proofend;

theorem :: PSCOMP_1:52
for X being non empty compact Subset of (TOP-REAL 2) st E-min X = E-max X holds
E-most X = {(E-min X)}
proofend;

theorem Th53: :: PSCOMP_1:53
for P being Subset of (TOP-REAL 2) holds
( (SW-corner P) `2 = (S-min P) `2 &amp; (SW-corner P) `2 = (S-max P) `2 &amp; (S-min P) `2 = (S-max P) `2 &amp; (S-min P) `2 = (SE-corner P) `2 &amp; (S-max P) `2 = (SE-corner P) `2 )
proofend;

theorem Th54: :: PSCOMP_1:54
for X being non empty compact Subset of (TOP-REAL 2) holds
( (SW-corner X) `1 <= (S-min X) `1 &amp; (SW-corner X) `1 <= (S-max X) `1 &amp; (SW-corner X) `1 <= (SE-corner X) `1 &amp; (S-min X) `1 <= (S-max X) `1 &amp; (S-min X) `1 <= (SE-corner X) `1 &amp; (S-max X) `1 <= (SE-corner X) `1 )
proofend;

theorem Th55: :: PSCOMP_1:55
for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in S-most Z holds
( p `2 = (S-min Z) `2 &amp; ( Z is compact implies ( (S-min Z) `1 <= p `1 &amp; p `1 <= (S-max Z) `1 ) ) )
proofend;

theorem Th56: :: PSCOMP_1:56
for X being non empty compact Subset of (TOP-REAL 2) holds S-most X c= LSeg ((S-min X),(S-max X))
proofend;

theorem :: PSCOMP_1:57
for X being non empty compact Subset of (TOP-REAL 2) holds LSeg ((S-min X),(S-max X)) c= LSeg ((SW-corner X),(SE-corner X))
proofend;

theorem Th58: :: PSCOMP_1:58
for X being non empty compact Subset of (TOP-REAL 2) holds
( S-min X in S-most X &amp; S-max X in S-most X )
proofend;

theorem :: PSCOMP_1:59
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg ((SW-corner X),(S-min X))) /\ X = {(S-min X)} &amp; (LSeg ((S-max X),(SE-corner X))) /\ X = {(S-max X)} )
proofend;

theorem :: PSCOMP_1:60
for X being non empty compact Subset of (TOP-REAL 2) st S-min X = S-max X holds
S-most X = {(S-min X)}
proofend;

:: Degenerate cases
theorem :: PSCOMP_1:61
for P being Subset of (TOP-REAL 2) st W-max P = N-min P holds
W-max P = NW-corner P
proofend;

theorem :: PSCOMP_1:62
for P being Subset of (TOP-REAL 2) st N-max P = E-max P holds
N-max P = NE-corner P
proofend;

theorem :: PSCOMP_1:63
for P being Subset of (TOP-REAL 2) st E-min P = S-max P holds
E-min P = SE-corner P
proofend;

theorem :: PSCOMP_1:64
for P being Subset of (TOP-REAL 2) st S-min P = W-min P holds
S-min P = SW-corner P
proofend;

theorem :: PSCOMP_1:65
for r, s being real number holds
( proj2 . |[r,s]| = s &amp; proj1 . |[r,s]| = r )
proofend;

:: Moved from JORDAN1E, AK, 23.02.2006
theorem :: PSCOMP_1:66
for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
N-bound X <= N-bound Y by Th17;

theorem :: PSCOMP_1:67
for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
E-bound X <= E-bound Y by Th17;

theorem :: PSCOMP_1:68
for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
S-bound X >= S-bound Y by Th16;

theorem :: PSCOMP_1:69
for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
W-bound X >= W-bound Y by Th16;