:: PSCOMP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

notation
let X be set ;
synonym without_zero X for with_non-empty_elements X;
antonym with_zero X for with_non-empty_elements X;
end;

definition
let X be set ;
redefine attr X is with_non-empty_elements means :Def1: :: PSCOMP_1:def 1
not 0 in X;
compatibility
( X is without_zero iff not 0 in X )
by SETFAM_1:def 9;
end;

:: deftheorem Def1 defines without_zero PSCOMP_1:def 1 :
for X being set holds
( X is without_zero iff not 0 in X );

registration
cluster REAL -> with_zero ;
coherence
not REAL is without_zero
by Def1;
cluster NAT -> with_zero ;
coherence
not NAT is without_zero
by Def1;
end;

registration
cluster non empty without_zero set ;
existence
ex b1 being set st
( not b1 is empty & b1 is without_zero )
proof end;
cluster non empty with_zero set ;
existence
ex b1 being set st
( not b1 is empty & not b1 is without_zero )
by Def1;
end;

registration
cluster non empty without_zero Element of K40(REAL );
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is without_zero )
proof end;
cluster non empty with_zero Element of K40(REAL );
existence
ex b1 being Subset of REAL st
( not b1 is empty & not b1 is without_zero )
by Def1;
end;

theorem Th1: :: PSCOMP_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being set st not F is empty & F is without_zero & F is c=-linear holds
F is centered
proof end;

registration
let F be set ;
cluster non empty c=-linear with_non-empty_elements -> centered Element of K40(K40(F));
coherence
for b1 being Subset-Family of F st not b1 is empty & b1 is without_zero & b1 is c=-linear holds
b1 is centered
by Th1;
end;

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

registration
let X, Y be non empty set ;
let f be Function of X,Y;
cluster f .: X -> non empty ;
coherence
not f .: X is empty
proof end;
end;

definition
let X, Y be set ;
let f be Function of X,Y;
func " f -> Function of bool Y, bool X means :Def2: :: PSCOMP_1:def 2
for y being Subset of Y holds it . y = f " y;
existence
ex b1 being Function of bool Y, bool X st
for y being Subset of Y holds b1 . y = f " y
proof end;
uniqueness
for b1, b2 being Function of bool Y, bool X st ( for y being Subset of Y holds b1 . y = f " y ) & ( for y being Subset of Y holds b2 . y = f " y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines " PSCOMP_1:def 2 :
for X, Y being set
for f being Function of X,Y
for b4 being Function of bool Y, bool X holds
( b4 = " f iff for y being Subset of Y holds b4 . y = f " y );

theorem Th2: :: PSCOMP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, x being set
for S being Subset-Family of Y
for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S
proof end;

theorem Th3: :: PSCOMP_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being real number st (abs r) + (abs s) = 0 holds
r = 0
proof end;

theorem Th4: :: PSCOMP_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s, t being real number st r < s & s < t holds
abs s < (abs r) + (abs t)
proof end;

theorem :: PSCOMP_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: PSCOMP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Real_Sequence st seq is convergent & seq is_not_0 & lim seq = 0 holds
not seq " is bounded
proof end;

theorem Th7: :: PSCOMP_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Real_Sequence holds
( rng seq is bounded iff seq is bounded )
proof end;

notation
let X be real-membered set ;
synonym sup X for upper_bound X;
synonym inf X for lower_bound X;
end;

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

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

:: deftheorem Def3 defines with_max PSCOMP_1:def 3 :
for X being real-membered set holds
( X is with_max iff ( X is bounded_above & sup X in X ) );

:: deftheorem Def4 defines with_min PSCOMP_1:def 4 :
for X being real-membered set holds
( X is with_min iff ( X is bounded_below & inf X in X ) );

registration
cluster non empty bounded closed Element of K40(REAL );
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is closed & b1 is bounded )
proof end;
end;

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

:: deftheorem Def5 defines open PSCOMP_1:def 5 :
for R being Subset-Family of REAL holds
( R is open iff for X being Subset of REAL st X in R holds
X is open );

:: deftheorem Def6 defines closed PSCOMP_1:def 6 :
for R being Subset-Family of REAL holds
( R is closed iff for X being Subset of REAL st X in R holds
X is closed );

definition
let X be Subset of REAL ;
func - X -> Subset of REAL equals :: PSCOMP_1:def 7
{ (- r3) where r3 is Real : r3 in X } ;
coherence
{ (- r3) where r3 is Real : r3 in X } is Subset of REAL
proof end;
involutiveness
for b1, b2 being Subset of REAL st b1 = { (- r3) where r3 is Real : r3 in b2 } holds
b2 = { (- r3) where r3 is Real : r3 in b1 }
proof end;
end;

:: deftheorem defines - PSCOMP_1:def 7 :
for X being Subset of REAL holds - X = { (- r3) where r3 is Real : r3 in X } ;

theorem :: PSCOMP_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PSCOMP_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PSCOMP_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PSCOMP_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PSCOMP_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PSCOMP_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th14: :: PSCOMP_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for X being Subset of REAL holds
( r in X iff - r in - X )
proof end;

registration
let X be non empty Subset of REAL ;
cluster - X -> non empty ;
coherence
not - X is empty
proof end;
end;

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

Lm2: for X being Subset of REAL st X is bounded_below holds
- X is bounded_above
proof end;

theorem Th15: :: PSCOMP_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL holds
( X is bounded_above iff - X is bounded_below )
proof end;

theorem :: PSCOMP_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL holds
( X is bounded_below iff - X is bounded_above )
proof end;

theorem Th17: :: PSCOMP_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty Subset of REAL st X is bounded_below holds
inf X = - (sup (- X))
proof end;

theorem Th18: :: PSCOMP_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty Subset of REAL st X is bounded_above holds
sup X = - (inf (- X))
proof end;

Lm3: for X being Subset of REAL st X is closed holds
- X is closed
proof end;

theorem Th19: :: PSCOMP_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL holds
( X is closed iff - X is closed )
proof end;

definition
let X be Subset of REAL ;
let p be Real;
redefine func p + X equals :: PSCOMP_1:def 8
{ (p + r3) where r3 is Real : r3 in X } ;
compatibility
for b1 being Element of K40(K311()) holds
( b1 = p + X iff b1 = { (p + r3) where r3 is Real : r3 in X } )
proof end;
end;

:: deftheorem defines + PSCOMP_1:def 8 :
for X being Subset of REAL
for p being Real holds p + X = { (p + r3) where r3 is Real : r3 in X } ;

theorem Th20: :: PSCOMP_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for X being Subset of REAL
for q3 being Real holds
( r in X iff q3 + r in q3 + X )
proof end;

registration
let X be non empty Subset of REAL ;
let s be Real;
cluster s + X -> non empty ;
coherence
not s + X is empty
proof end;
end;

theorem Th21: :: PSCOMP_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL holds X = 0 + X
proof end;

theorem Th22: :: PSCOMP_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL
for q3, p3 being Real holds q3 + (p3 + X) = (q3 + p3) + X
proof end;

Lm4: for X being Subset of REAL
for s being Real st X is bounded_above holds
s + X is bounded_above
proof end;

theorem :: PSCOMP_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL
for q3 being Real holds
( X is bounded_above iff q3 + X is bounded_above )
proof end;

Lm5: for X being Subset of REAL
for p being Real st X is bounded_below holds
p + X is bounded_below
proof end;

theorem :: PSCOMP_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL
for q3 being Real holds
( X is bounded_below iff q3 + X is bounded_below )
proof end;

theorem :: PSCOMP_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q3 being Real
for X being non empty Subset of REAL st X is bounded_below holds
inf (q3 + X) = q3 + (inf X)
proof end;

theorem :: PSCOMP_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q3 being Real
for X being non empty Subset of REAL st X is bounded_above holds
sup (q3 + X) = q3 + (sup X)
proof end;

Lm6: for q3 being Real
for X being Subset of REAL st X is closed holds
q3 + X is closed
proof end;

theorem Th27: :: PSCOMP_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL
for q3 being Real holds
( X is closed iff q3 + X is closed )
proof end;

definition
let X be Subset of REAL ;
func Inv X -> Subset of REAL equals :: PSCOMP_1:def 9
{ (1 / r3) where r3 is Real : r3 in X } ;
coherence
{ (1 / r3) where r3 is Real : r3 in X } is Subset of REAL
proof end;
end;

:: deftheorem defines Inv PSCOMP_1:def 9 :
for X being Subset of REAL holds Inv X = { (1 / r3) where r3 is Real : r3 in X } ;

theorem Th28: :: PSCOMP_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for X being without_zero Subset of REAL holds
( r in X iff 1 / r in Inv X )
proof end;

registration
let X be non empty without_zero Subset of REAL ;
cluster Inv X -> non empty without_zero ;
coherence
( not Inv X is empty & Inv X is without_zero )
proof end;
end;

registration
let X be without_zero Subset of REAL ;
cluster Inv X -> without_zero ;
coherence
Inv X is without_zero
proof end;
end;

theorem Th29: :: PSCOMP_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being without_zero Subset of REAL holds Inv (Inv X) = X
proof end;

theorem :: PSCOMP_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being without_zero Subset of REAL st X is closed & X is bounded holds
Inv X is closed
proof end;

theorem Th31: :: PSCOMP_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being Subset-Family of REAL st Z is closed holds
meet Z is closed
proof end;

definition
let X be Subset of REAL ;
func Cl X -> Subset of REAL equals :: PSCOMP_1:def 10
meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
coherence
meet { A where A is Subset of REAL : ( X c= A & A is closed ) } is Subset of REAL
proof end;
projectivity
for b1, b2 being Subset of REAL st b1 = meet { A where A is Subset of REAL : ( b2 c= A & A is closed ) } holds
b1 = meet { A where A is Subset of REAL : ( b1 c= A & A is closed ) }
proof end;
end;

:: deftheorem defines Cl PSCOMP_1:def 10 :
for X being Subset of REAL holds Cl X = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;

registration
let X be Subset of REAL ;
cluster Cl X -> closed ;
coherence
Cl X is closed
proof end;
end;

theorem Th32: :: PSCOMP_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL
for Y being closed Subset of REAL st X c= Y holds
Cl X c= Y
proof end;

theorem Th33: :: PSCOMP_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL holds X c= Cl X
proof end;

theorem Th34: :: PSCOMP_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL holds
( X is closed iff X = Cl X )
proof end;

theorem :: PSCOMP_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl ({} REAL ) = {} by Th34, FCONT_3:3;

theorem :: PSCOMP_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl ([#] REAL ) = REAL
proof end;

theorem :: PSCOMP_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being Subset of REAL st X c= Y holds
Cl X c= Cl Y
proof end;

theorem Th38: :: PSCOMP_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL
for r3 being Real holds
( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
not O /\ X is empty )
proof end;

theorem Th39: :: PSCOMP_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of REAL
for r3 being Real st r3 in Cl X holds
ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )
proof end;

definition
let X be set ;
let f be Function of X, REAL ;
:: original: bounded_below
redefine attr f is bounded_below means :Def11: :: PSCOMP_1:def 11
f .: X is bounded_below;
compatibility
( f is bounded_below iff f .: X is bounded_below )
proof end;
:: original: bounded_above
redefine attr f is bounded_above means :Def12: :: PSCOMP_1:def 12
f .: X is bounded_above;
compatibility
( f is bounded_above iff f .: X is bounded_above )
proof end;
end;

:: deftheorem Def11 defines bounded_below PSCOMP_1:def 11 :
for X being set
for f being Function of X, REAL holds
( f is bounded_below iff f .: X is bounded_below );

:: deftheorem Def12 defines bounded_above PSCOMP_1:def 12 :
for X being set
for f being Function of X, REAL holds
( f is bounded_above iff f .: X is bounded_above );

definition
let X be set ;
let f be Function of X, REAL ;
canceled;
attr f is with_max means :Def14: :: PSCOMP_1:def 14
f .: X is with_max;
attr f is with_min means :Def15: :: PSCOMP_1:def 15
f .: X is with_min;
end;

:: deftheorem PSCOMP_1:def 13 :
canceled;

:: deftheorem Def14 defines with_max PSCOMP_1:def 14 :
for X being set
for f being Function of X, REAL holds
( f is with_max iff f .: X is with_max );

:: deftheorem Def15 defines with_min PSCOMP_1:def 15 :
for X being set
for f being Function of X, REAL holds
( f is with_min iff f .: X is with_min );

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

:: deftheorem Def16 defines - PSCOMP_1:def 16 :
for X being set
for f, b3 being Function of X, REAL holds
( b3 = - f iff for p being set st p in X holds
b3 . p = - (f . p) );

theorem Th40: :: PSCOMP_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, A being set
for f being Function of X, REAL holds (- f) .: A = - (f .: A)
proof end;

Lm7: for X being non empty set
for f being Function of X, REAL st f is with_max holds
- f is with_min
proof end;

Lm8: for X being non empty set
for f being Function of X, REAL st f is with_min holds
- f is with_max
proof end;

theorem Th41: :: PSCOMP_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being Function of X, REAL holds
( f is with_min iff - f is with_max )
proof end;

theorem :: PSCOMP_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being Function of X, REAL holds
( f is with_max iff - f is with_min )
proof end;

theorem Th43: :: PSCOMP_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Subset of REAL
for f being Function of X, REAL holds (- f) " A = f " (- A)
proof end;

definition
let X be set ;
let r be Real;
let f be Function of X, REAL ;
func r + f -> Function of X, REAL means :Def17: :: PSCOMP_1:def 17
for p being set st p in X holds
it . p = r + (f . p);
existence
ex b1 being Function of X, REAL st
for p being set st p in X holds
b1 . p = r + (f . p)
proof end;
uniqueness
for b1, b2 being Function of X, REAL st ( for p being set st p in X holds
b1 . p = r + (f . p) ) & ( for p being set st p in X holds
b2 . p = r + (f . p) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines + PSCOMP_1:def 17 :
for X being set
for r being Real
for f, b4 being Function of X, REAL holds
( b4 = r + f iff for p being set st p in X holds
b4 . p = r + (f . p) );

theorem :: PSCOMP_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, A being set
for f being Function of X, REAL
for s being Real holds (s + f) .: A = s + (f .: A)
proof end;

theorem Th45: :: PSCOMP_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Subset of REAL
for f being Function of X, REAL
for q3 being Real holds (q3 + f) " A = f " ((- q3) + A)
proof end;

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

:: deftheorem Def18 defines Inv PSCOMP_1:def 18 :
for X being set
for f, b3 being Function of X, REAL holds
( b3 = Inv f iff for p being set st p in X holds
b3 . p = 1 / (f . p) );

theorem Th46: :: PSCOMP_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being without_zero Subset of REAL
for f being Function of X, REAL holds (Inv f) " A = f " (Inv A)
proof end;

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

registration
let T be non empty 1-sorted ;
cluster bounded M5(the carrier of T, REAL );
existence
ex b1 being RealMap of T st b1 is bounded
proof end;
end;

scheme :: PSCOMP_1:sch 1
NonUniqExRF{ F1() -> non empty TopStruct , P1[ set , set ] } :
ex f being RealMap of F1() st
for x being Element of F1() holds P1[x,f . x]
provided
A1: for x being set st x in the carrier of F1() holds
ex r3 being Real st P1[x,r3]
proof end;

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

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

:: deftheorem PSCOMP_1:def 19 :
canceled;

:: deftheorem Def20 defines inf PSCOMP_1:def 20 :
for T being 1-sorted
for f being RealMap of T holds inf f = inf (f .: the carrier of T);

:: deftheorem Def21 defines sup PSCOMP_1:def 21 :
for T being 1-sorted
for f being RealMap of T holds sup f = sup (f .: the carrier of T);

theorem Th47: :: PSCOMP_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for f being V53 RealMap of T
for p being Point of T holds f . p >= inf f
proof end;

theorem :: PSCOMP_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for f being V53 RealMap of T
for s being Real st ( for t being Point of T holds f . t >= s ) holds
inf f >= s
proof end;

theorem :: PSCOMP_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = inf f
proof end;

theorem Th50: :: PSCOMP_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for f being V52 RealMap of T
for p being Point of T holds f . p <= sup f
proof end;

theorem :: PSCOMP_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for f being V52 RealMap of T
for t being real number st ( for p being Point of T holds f . p <= t ) holds
sup f <= t
proof end;

theorem :: PSCOMP_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = sup f
proof end;

theorem Th53: :: PSCOMP_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty 1-sorted
for f being bounded RealMap of T holds inf f <= sup f
proof end;

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

:: deftheorem PSCOMP_1:def 22 :
canceled;

:: deftheorem PSCOMP_1:def 23 :
canceled;

:: deftheorem PSCOMP_1:def 24 :
canceled;

:: deftheorem Def25 defines continuous PSCOMP_1:def 25 :
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 continuous M5(the carrier of T, REAL );
existence
ex b1 being RealMap of T st b1 is continuous
proof end;
end;

registration
let T be non empty TopSpace;
let S be non empty SubSpace of T;
cluster continuous M5(the carrier of S, REAL );
existence
ex b1 being RealMap of S st b1 is continuous
proof end;
end;

theorem Th54: :: PSCOMP_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th55: :: PSCOMP_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for f being RealMap of T st f is continuous holds
- f is continuous
proof end;

theorem Th56: :: PSCOMP_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r3 being Real
for T being TopStruct
for f being RealMap of T st f is continuous holds
r3 + f is continuous
proof end;

theorem Th57: :: PSCOMP_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for f being RealMap of T st f is continuous & not 0 in rng f holds
Inv f is continuous
proof end;

definition
let X, Y be set ;
let f be Function of bool X, bool Y;
let R be Subset-Family of X;
:: original: .:
redefine func f .: R -> Subset-Family of Y;
coherence
f .: R is Subset-Family of Y
proof end;
end;

theorem :: PSCOMP_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for f being RealMap of T
for R being Subset-Family of REAL st f is continuous & R is open holds
(" f) .: R is open
proof end;

theorem Th59: :: PSCOMP_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for f being RealMap of T
for R being Subset-Family of REAL st f is continuous & R is closed holds
(" f) .: R is closed
proof end;

definition
let T be non empty TopStruct ;
let X be Subset of T;
let f be RealMap of T;
func f || X -> RealMap of (T | X) equals :: PSCOMP_1:def 26
f | X;
coherence
f | X is RealMap of (T | X)
proof end;
end;

:: deftheorem defines || PSCOMP_1:def 26 :
for T being non empty TopStruct
for X being Subset of T
for f being RealMap of T holds f || X = f | X;

registration
let T be non empty TopSpace;
cluster non empty compact Element of K40(the carrier of T);
existence
ex b1 being Subset of T st
( b1 is compact & not b1 is empty )
proof end;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let X be Subset of T;
cluster f || X -> continuous ;
coherence
f || X is continuous
proof end;
end;

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

theorem Th60: :: PSCOMP_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th61: :: PSCOMP_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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

:: deftheorem Def27 defines pseudocompact PSCOMP_1:def 27 :
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 compact -> non empty pseudocompact TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is compact holds
b1 is pseudocompact
proof end;
end;

registration
cluster non empty compact pseudocompact TopStruct ;
existence
ex b1 being TopSpace st
( b1 is compact & not b1 is empty )
proof end;
end;

registration
let T be non empty pseudocompact TopSpace;
cluster continuous -> bounded with_max with_min M5(the carrier of T, REAL );
coherence
for b1 being RealMap of T st b1 is continuous holds
( b1 is bounded & b1 is with_max & b1 is with_min )
proof end;
end;

theorem Th62: :: PSCOMP_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
inf (f || Y) <= inf (f || X)
proof end;

theorem Th63: :: PSCOMP_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
sup (f || X) <= sup (f || Y)
proof end;

theorem Th64: :: PSCOMP_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for X, Y being compact Subset of (TOP-REAL n) holds X /\ Y is compact
proof end;

definition
func proj1 -> RealMap of (TOP-REAL 2) means :Def28: :: PSCOMP_1:def 28
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
proof end;
uniqueness
for b1, b2 being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = p `1 ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = p `1 ) holds
b1 = b2
proof end;
func proj2 -> RealMap of (TOP-REAL 2) means :Def29: :: PSCOMP_1:def 29
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
proof end;
uniqueness
for b1, b2 being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = p `2 ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = p `2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def28 defines proj1 PSCOMP_1:def 28 :
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 Def29 defines proj2 PSCOMP_1:def 29 :
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 Th65: :: PSCOMP_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being real number holds proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
proof end;

theorem Th66: :: PSCOMP_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } holds
P is open
proof end;

theorem Th67: :: PSCOMP_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being real number holds proj2 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) }
proof end;

theorem Th68: :: PSCOMP_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } holds
P is open
proof end;

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

theorem Th69: :: PSCOMP_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th70: :: PSCOMP_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

Lm9: for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( inf (proj1 || X) <= p `1 & p `1 <= sup (proj1 || X) & inf (proj2 || X) <= p `2 & p `2 <= sup (proj2 || X) )
proof end;

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

:: deftheorem defines W-bound PSCOMP_1:def 30 :
for X being Subset of (TOP-REAL 2) holds W-bound X = inf (proj1 || X);

:: deftheorem Def31 defines N-bound PSCOMP_1:def 31 :
for X being Subset of (TOP-REAL 2) holds N-bound X = sup (proj2 || X);

:: deftheorem Def32 defines E-bound PSCOMP_1:def 32 :
for X being Subset of (TOP-REAL 2) holds E-bound X = sup (proj1 || X);

:: deftheorem defines S-bound PSCOMP_1:def 33 :
for X being Subset of (TOP-REAL 2) holds S-bound X = inf (proj2 || X);

theorem Th71: :: PSCOMP_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X ) by Lm9;

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)]|;
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 35
|[(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 36
|[(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 37
|[(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 34 :
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 35 :
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 36 :
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 37 :
for X being Subset of (TOP-REAL 2) holds SE-corner X = |[(E-bound X),(S-bound X)]|;

theorem Th72: :: PSCOMP_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `1 = W-bound P by EUCLID:56;

theorem Th73: :: PSCOMP_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `2 = S-bound P by EUCLID:56;

theorem Th74: :: PSCOMP_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (NW-corner P) `1 = W-bound P by EUCLID:56;

theorem Th75: :: PSCOMP_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (NW-corner P) `2 = N-bound P by EUCLID:56;

theorem Th76: :: PSCOMP_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (NE-corner P) `1 = E-bound P by EUCLID:56;

theorem Th77: :: PSCOMP_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (NE-corner P) `2 = N-bound P by EUCLID:56;

theorem Th78: :: PSCOMP_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (SE-corner P) `1 = E-bound P by EUCLID:56;

theorem Th79: :: PSCOMP_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (SE-corner P) `2 = S-bound P by EUCLID:56;

theorem :: PSCOMP_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `1 = (NW-corner P) `1
proof end;

theorem :: PSCOMP_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (SE-corner P) `1 = (NE-corner P) `1
proof end;

theorem :: PSCOMP_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (NW-corner P) `2 = (NE-corner P) `2
proof end;

theorem :: PSCOMP_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `2 = (SE-corner P) `2
proof end;

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;
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 39
(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 40
(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 41
(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 38 :
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 39 :
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 40 :
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 41 :
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 & W-most X is compact )
proof end;
cluster N-most X -> non empty compact ;
coherence
( not N-most X is empty & N-most X is compact )
proof end;
cluster E-most X -> non empty compact ;
coherence
( not E-most X is empty & E-most X is compact )
proof end;
cluster S-most X -> non empty compact ;
coherence
( not S-most X is empty & S-most X is compact )
proof end;
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)))]|;
coherence
|[(W-bound X),(inf (proj2 || (W-most X)))]| is Point of (TOP-REAL 2)
;
func W-max X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 43
|[(W-bound X),(sup (proj2 || (W-most X)))]|;
coherence
|[(W-bound X),(sup (proj2 || (W-most X)))]| is Point of (TOP-REAL 2)
;
func N-min X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 44
|[(inf (proj1 || (N-most X))),(N-bound X)]|;
coherence
|[(inf (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 45
|[(sup (proj1 || (N-most X))),(N-bound X)]|;
coherence
|[(sup (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 46
|[(E-bound X),(sup (proj2 || (E-most X)))]|;
coherence
|[(E-bound X),(sup (proj2 || (E-most X)))]| is Point of (TOP-REAL 2)
;
func E-min X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 47
|[(E-bound X),(inf (proj2 || (E-most X)))]|;
coherence
|[(E-bound X),(inf (proj2 || (E-most X)))]| is Point of (TOP-REAL 2)
;
func S-max X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 48
|[(sup (proj1 || (S-most X))),(S-bound X)]|;
coherence
|[(sup (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 49
|[(inf (proj1 || (S-most X))),(S-bound X)]|;
coherence
|[(inf (proj1 || (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2)
;
end;

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

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

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

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

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

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

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

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

theorem Th84: :: PSCOMP_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (W-min P) `1 = W-bound P & (W-max P) `1 = W-bound P ) by EUCLID:56;

theorem Th85: :: PSCOMP_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th86: :: PSCOMP_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (W-min P) `2 = inf (proj2 || (W-most P)) & (W-max P) `2 = sup (proj2 || (W-most P)) ) by EUCLID:56;

theorem Th87: :: PSCOMP_1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th88: :: PSCOMP_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) )
proof end;

theorem Th89: :: PSCOMP_1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds W-most X c= LSeg (W-min X),(W-max X)
proof end;

theorem :: PSCOMP_1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th91: :: PSCOMP_1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( W-min X in W-most X & W-max X in W-most X )
proof end;

theorem :: PSCOMP_1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SW-corner X),(W-min X)) /\ X = {(W-min X)} & (LSeg (W-max X),(NW-corner X)) /\ X = {(W-max X)} )
proof end;

theorem :: PSCOMP_1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem Th94: :: PSCOMP_1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (N-min P) `2 = N-bound P & (N-max P) `2 = N-bound P ) by EUCLID:56;

theorem Th95: :: PSCOMP_1:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th96: :: PSCOMP_1:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (N-min P) `1 = inf (proj1 || (N-most P)) & (N-max P) `1 = sup (proj1 || (N-most P)) ) by EUCLID:56;

theorem Th97: :: PSCOMP_1:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th98: :: PSCOMP_1:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ( Z is compact implies ( (N-min Z) `1 <= p `1 & p `1 <= (N-max Z) `1 ) ) )
proof end;

theorem Th99: :: PSCOMP_1:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds N-most X c= LSeg (N-min X),(N-max X)
proof end;

theorem :: PSCOMP_1:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th101: :: PSCOMP_1:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( N-min X in N-most X & N-max X in N-most X )
proof end;

theorem :: PSCOMP_1:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (NW-corner X),(N-min X)) /\ X = {(N-min X)} & (LSeg (N-max X),(NE-corner X)) /\ X = {(N-max X)} )
proof end;

theorem :: PSCOMP_1:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem Th104: :: PSCOMP_1:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (E-min P) `1 = E-bound P & (E-max P) `1 = E-bound P ) by EUCLID:56;

theorem Th105: :: PSCOMP_1:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th106: :: PSCOMP_1:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (E-min P) `2 = inf (proj2 || (E-most P)) & (E-max P) `2 = sup (proj2 || (E-most P)) ) by EUCLID:56;

theorem Th107: :: PSCOMP_1:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th108: :: PSCOMP_1:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ( Z is compact implies ( (E-min Z) `2 <= p `2 & p `2 <= (E-max Z) `2 ) ) )
proof end;

theorem Th109: :: PSCOMP_1:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds E-most X c= LSeg (E-min X),(E-max X)
proof end;

theorem :: PSCOMP_1:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th111: :: PSCOMP_1:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( E-min X in E-most X & E-max X in E-most X )
proof end;

theorem :: PSCOMP_1:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SE-corner X),(E-min X)) /\ X = {(E-min X)} & (LSeg (E-max X),(NE-corner X)) /\ X = {(E-max X)} )
proof end;

theorem :: PSCOMP_1:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem Th114: :: PSCOMP_1:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (S-min P) `2 = S-bound P & (S-max P) `2 = S-bound P ) by EUCLID:56;

theorem Th115: :: PSCOMP_1:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th116: :: PSCOMP_1:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) holds
( (S-min P) `1 = inf (proj1 || (S-most P)) & (S-max P) `1 = sup (proj1 || (S-most P)) ) by EUCLID:56;

theorem Th117: :: PSCOMP_1:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (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 end;

theorem Th118: :: PSCOMP_1:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ( Z is compact implies ( (S-min Z) `1 <= p `1 & p `1 <= (S-max Z) `1 ) ) )
proof end;

theorem Th119: :: PSCOMP_1:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds S-most X c= LSeg (S-min X),(S-max X)
proof end;

theorem :: PSCOMP_1:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th121: :: PSCOMP_1:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( S-min X in S-most X & S-max X in S-most X )
proof end;

theorem :: PSCOMP_1:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SW-corner X),(S-min X)) /\ X = {(S-min X)} & (LSeg (S-max X),(SE-corner X)) /\ X = {(S-max X)} )
proof end;

theorem :: PSCOMP_1:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem :: PSCOMP_1:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) st W-max P = N-min P holds
W-max P = NW-corner P
proof end;

theorem :: PSCOMP_1:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) st N-max P = E-max P holds
N-max P = NE-corner P
proof end;

theorem :: PSCOMP_1:126  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) st E-min P = S-max P holds
E-min P = SE-corner P
proof end;

theorem :: PSCOMP_1:127  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) st S-min P = W-min P holds
S-min P = SW-corner P
proof end;