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

theorem Th1: :: SPRECT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being trivial set
for B being set st B c= A holds
B is trivial
proof end;

registration
cluster non constant -> non trivial set ;
coherence
for b1 being Function st not b1 is constant holds
not b1 is trivial
proof end;
end;

registration
cluster trivial -> constant set ;
coherence
for b1 being Function st b1 is trivial holds
b1 is constant
proof end;
end;

theorem Th2: :: SPRECT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function st rng f is trivial holds
f is constant
proof end;

registration
let f be constant Function;
cluster rng f -> trivial ;
coherence
rng f is trivial
proof end;
end;

registration
cluster non empty constant set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is constant )
proof end;
end;

theorem Th3: :: SPRECT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence st f ^ g is constant holds
( f is constant & g is constant )
proof end;

theorem Th4: :: SPRECT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set st <*x,y*> is constant holds
x = y
proof end;

theorem Th5: :: SPRECT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set st <*x,y,z*> is constant holds
( x = y & y = z & z = x )
proof end;

theorem Th6: :: SPRECT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GX being non empty TopSpace
for A being Subset of GX
for B being non empty Subset of GX st A is_a_component_of B holds
A <> {}
proof end;

theorem Th7: :: SPRECT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GX being TopStruct
for A, B being Subset of GX st A is_a_component_of B holds
A c= B
proof end;

theorem Th8: :: SPRECT_1:8  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 A being non empty Subset of T
for B1, B2, S being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & S is_a_component_of A & B1 \/ B2 = A & not S = B1 holds
S = B2
proof end;

theorem Th9: :: SPRECT_1:9  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 A being non empty Subset of T
for B1, B2, C1, C2 being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & C1 is_a_component_of A & C2 is_a_component_of A & B1 \/ B2 = A & C1 \/ C2 = A holds
{B1,B2} = {C1,C2}
proof end;

theorem Th10: :: SPRECT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Point of (TOP-REAL 2) holds L~ <*p,q,r*> = (LSeg p,q) \/ (LSeg q,r)
proof end;

registration
let n be Nat;
let f be non trivial FinSequence of (TOP-REAL n);
cluster L~ f -> non empty ;
coherence
not L~ f is empty
proof end;
end;

registration
let f be FinSequence of (TOP-REAL 2);
cluster L~ f -> compact ;
coherence
L~ f is compact
proof end;
end;

theorem Th11: :: SPRECT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of (TOP-REAL 2) st A c= B & B is horizontal holds
A is horizontal
proof end;

theorem Th12: :: SPRECT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of (TOP-REAL 2) st A c= B & B is vertical holds
A is vertical
proof end;

registration
cluster R^2-unit_square -> non horizontal non vertical special_polygonal ;
coherence
( R^2-unit_square is special_polygonal & not R^2-unit_square is horizontal & not R^2-unit_square is vertical )
proof end;
end;

registration
cluster non empty non horizontal non vertical compact Element of bool the carrier of (TOP-REAL 2);
existence
ex b1 being Subset of (TOP-REAL 2) st
( not b1 is vertical & not b1 is horizontal & not b1 is empty & b1 is compact )
proof end;
end;

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

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

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

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

theorem Th17: :: SPRECT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is vertical iff W-bound C = E-bound C )
proof end;

theorem Th18: :: SPRECT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is horizontal iff S-bound C = N-bound C )
proof end;

theorem :: SPRECT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) st NW-corner C = NE-corner C holds
C is vertical
proof end;

theorem :: SPRECT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) st SW-corner C = SE-corner C holds
C is vertical
proof end;

theorem :: SPRECT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) st NW-corner C = SW-corner C holds
C is horizontal
proof end;

theorem :: SPRECT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) st NE-corner C = SE-corner C holds
C is horizontal
proof end;

theorem Th23: :: SPRECT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds W-bound C <= E-bound C
proof end;

theorem Th24: :: SPRECT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds S-bound C <= N-bound C
proof end;

theorem Th25: :: SPRECT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds LSeg (SE-corner C),(NE-corner C) = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) }
proof end;

theorem Th26: :: SPRECT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds LSeg (SW-corner C),(SE-corner C) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C ) }
proof end;

theorem Th27: :: SPRECT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds LSeg (NW-corner C),(NE-corner C) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) }
proof end;

theorem Th28: :: SPRECT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds LSeg (SW-corner C),(NW-corner C) = { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) }
proof end;

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

theorem Th30: :: SPRECT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds (LSeg (NW-corner C),(NE-corner C)) /\ (LSeg (NE-corner C),(SE-corner C)) = {(NE-corner C)}
proof end;

theorem Th31: :: SPRECT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds (LSeg (SE-corner C),(NE-corner C)) /\ (LSeg (SW-corner C),(SE-corner C)) = {(SE-corner C)}
proof end;

theorem Th32: :: SPRECT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds (LSeg (NW-corner C),(SW-corner C)) /\ (LSeg (SW-corner C),(SE-corner C)) = {(SW-corner C)}
proof end;

theorem Th33: :: SPRECT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1 being non empty non vertical compact Subset of (TOP-REAL 2) holds W-bound D1 < E-bound D1
proof end;

theorem Th34: :: SPRECT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D2 being non empty non horizontal compact Subset of (TOP-REAL 2) holds S-bound D2 < N-bound D2
proof end;

theorem Th35: :: SPRECT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1 being non empty non vertical compact Subset of (TOP-REAL 2) holds LSeg (SW-corner D1),(NW-corner D1) misses LSeg (SE-corner D1),(NE-corner D1)
proof end;

theorem Th36: :: SPRECT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D2 being non empty non horizontal compact Subset of (TOP-REAL 2) holds LSeg (SW-corner D2),(SE-corner D2) misses LSeg (NW-corner D2),(NE-corner D2)
proof end;

definition
let C be Subset of (TOP-REAL 2);
func SpStSeq C -> FinSequence of (TOP-REAL 2) equals :: SPRECT_1:def 1
<*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*>;
coherence
<*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*> is FinSequence of (TOP-REAL 2)
;
end;

:: deftheorem defines SpStSeq SPRECT_1:def 1 :
for C being Subset of (TOP-REAL 2) holds SpStSeq C = <*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*>;

theorem Th37: :: SPRECT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 1 = NW-corner S
proof end;

theorem Th38: :: SPRECT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 2 = NE-corner S
proof end;

theorem Th39: :: SPRECT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 3 = SE-corner S
proof end;

theorem Th40: :: SPRECT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 4 = SW-corner S
proof end;

theorem :: SPRECT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 5 = NW-corner S
proof end;

theorem Th42: :: SPRECT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds len (SpStSeq S) = 5
proof end;

theorem Th43: :: SPRECT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds L~ (SpStSeq S) = ((LSeg (NW-corner S),(NE-corner S)) \/ (LSeg (NE-corner S),(SE-corner S))) \/ ((LSeg (SE-corner S),(SW-corner S)) \/ (LSeg (SW-corner S),(NW-corner S)))
proof end;

registration
let D be non empty non vertical compact Subset of (TOP-REAL 2);
cluster SpStSeq D -> non trivial non constant ;
coherence
not SpStSeq D is constant
proof end;
end;

registration
let D be non empty non horizontal compact Subset of (TOP-REAL 2);
cluster SpStSeq D -> non trivial non constant ;
coherence
not SpStSeq D is constant
proof end;
end;

registration
let D be non empty non horizontal non vertical compact Subset of (TOP-REAL 2);
cluster SpStSeq D -> non trivial non constant special unfolded circular s.c.c. standard ;
coherence
( SpStSeq D is special & SpStSeq D is unfolded & SpStSeq D is circular & SpStSeq D is s.c.c. & SpStSeq D is standard )
proof end;
end;

theorem Th44: :: SPRECT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty non horizontal non vertical compact Subset of (TOP-REAL 2) holds L~ (SpStSeq D) = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).]
proof end;

theorem Th45: :: SPRECT_1:45  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 TopStruct
for X being Subset of T
for f being RealMap of T holds rng (f || X) = f .: X
proof end;

theorem Th46: :: SPRECT_1:46  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 compact Subset of T
for f being continuous RealMap of T holds f .: X is bounded_below
proof end;

theorem Th47: :: SPRECT_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 X being non empty compact Subset of T
for f being continuous RealMap of T holds f .: X is bounded_above
proof end;

registration
cluster non empty bounded_above bounded_below Element of bool REAL ;
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is bounded_above & b1 is bounded_below )
proof end;
end;

theorem Th48: :: SPRECT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds W-bound S = inf (proj1 .: S)
proof end;

theorem Th49: :: SPRECT_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds S-bound S = inf (proj2 .: S)
proof end;

theorem Th50: :: SPRECT_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds N-bound S = sup (proj2 .: S)
proof end;

theorem Th51: :: SPRECT_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2) holds E-bound S = sup (proj1 .: S)
proof end;

theorem Th52: :: SPRECT_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty bounded_below Subset of REAL holds inf (A \/ B) = min (inf A),(inf B)
proof end;

theorem Th53: :: SPRECT_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty bounded_above Subset of REAL holds sup (A \/ B) = max (sup A),(sup B)
proof end;

theorem Th54: :: SPRECT_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2)
for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds
W-bound S = min (W-bound C1),(W-bound C2)
proof end;

theorem Th55: :: SPRECT_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2)
for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds
S-bound S = min (S-bound C1),(S-bound C2)
proof end;

theorem Th56: :: SPRECT_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2)
for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds
N-bound S = max (N-bound C1),(N-bound C2)
proof end;

theorem Th57: :: SPRECT_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2)
for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds
E-bound S = max (E-bound C1),(E-bound C2)
proof end;

registration
cluster {} REAL -> bounded ;
coherence
{} REAL is bounded
proof end;
end;

registration
let r1, r2 be real number ;
cluster [.r1,r2.] -> bounded ;
coherence
[.r1,r2.] is bounded
proof end;
end;

registration
cluster bounded -> bounded_above bounded_below Element of bool REAL ;
coherence
for b1 being Subset of REAL st b1 is bounded holds
( b1 is bounded_below & b1 is bounded_above )
by SEQ_4:def 3;
cluster bounded_above bounded_below -> bounded Element of bool REAL ;
coherence
for b1 being Subset of REAL st b1 is bounded_below & b1 is bounded_above holds
b1 is bounded
by SEQ_4:def 3;
end;

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

theorem Th59: :: SPRECT_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r1, r2, t being Real st r1 <= r2 holds
( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )
proof end;

theorem Th60: :: SPRECT_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p `1 <= q `1 holds
proj1 .: (LSeg p,q) = [.(p `1 ),(q `1 ).]
proof end;

theorem Th61: :: SPRECT_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds
proj2 .: (LSeg p,q) = [.(p `2 ),(q `2 ).]
proof end;

theorem Th62: :: SPRECT_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p `1 <= q `1 holds
W-bound (LSeg p,q) = p `1
proof end;

theorem Th63: :: SPRECT_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds
S-bound (LSeg p,q) = p `2
proof end;

theorem Th64: :: SPRECT_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds
N-bound (LSeg p,q) = q `2
proof end;

theorem Th65: :: SPRECT_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p `1 <= q `1 holds
E-bound (LSeg p,q) = q `1
proof end;

theorem Th66: :: SPRECT_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds W-bound (L~ (SpStSeq C)) = W-bound C
proof end;

theorem Th67: :: SPRECT_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds S-bound (L~ (SpStSeq C)) = S-bound C
proof end;

theorem Th68: :: SPRECT_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds N-bound (L~ (SpStSeq C)) = N-bound C
proof end;

theorem Th69: :: SPRECT_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds E-bound (L~ (SpStSeq C)) = E-bound C
proof end;

theorem Th70: :: SPRECT_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds NW-corner (L~ (SpStSeq C)) = NW-corner C
proof end;

theorem Th71: :: SPRECT_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds NE-corner (L~ (SpStSeq C)) = NE-corner C
proof end;

theorem Th72: :: SPRECT_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds SW-corner (L~ (SpStSeq C)) = SW-corner C
proof end;

theorem Th73: :: SPRECT_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds SE-corner (L~ (SpStSeq C)) = SE-corner C
proof end;

theorem Th74: :: SPRECT_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds W-most (L~ (SpStSeq C)) = LSeg (SW-corner C),(NW-corner C)
proof end;

theorem Th75: :: SPRECT_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds N-most (L~ (SpStSeq C)) = LSeg (NW-corner C),(NE-corner C)
proof end;

theorem Th76: :: SPRECT_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds S-most (L~ (SpStSeq C)) = LSeg (SW-corner C),(SE-corner C)
proof end;

theorem Th77: :: SPRECT_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds E-most (L~ (SpStSeq C)) = LSeg (SE-corner C),(NE-corner C)
proof end;

theorem Th78: :: SPRECT_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds proj2 .: (LSeg (SW-corner C),(NW-corner C)) = [.(S-bound C),(N-bound C).]
proof end;

theorem Th79: :: SPRECT_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds proj1 .: (LSeg (NW-corner C),(NE-corner C)) = [.(W-bound C),(E-bound C).]
proof end;

theorem Th80: :: SPRECT_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds proj2 .: (LSeg (NE-corner C),(SE-corner C)) = [.(S-bound C),(N-bound C).]
proof end;

theorem Th81: :: SPRECT_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds proj1 .: (LSeg (SE-corner C),(SW-corner C)) = [.(W-bound C),(E-bound C).]
proof end;

theorem Th82: :: SPRECT_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds W-min (L~ (SpStSeq C)) = SW-corner C
proof end;

theorem Th83: :: SPRECT_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds W-max (L~ (SpStSeq C)) = NW-corner C
proof end;

theorem Th84: :: SPRECT_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds N-min (L~ (SpStSeq C)) = NW-corner C
proof end;

theorem Th85: :: SPRECT_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds N-max (L~ (SpStSeq C)) = NE-corner C
proof end;

theorem Th86: :: SPRECT_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds E-min (L~ (SpStSeq C)) = SE-corner C
proof end;

theorem Th87: :: SPRECT_1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds E-max (L~ (SpStSeq C)) = NE-corner C
proof end;

theorem Th88: :: SPRECT_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds S-min (L~ (SpStSeq C)) = SW-corner C
proof end;

theorem Th89: :: SPRECT_1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact Subset of (TOP-REAL 2) holds S-max (L~ (SpStSeq C)) = SE-corner C
proof end;

definition
let f be FinSequence of (TOP-REAL 2);
attr f is rectangular means :Def2: :: SPRECT_1:def 2
ex D being non empty non horizontal non vertical compact Subset of (TOP-REAL 2) st f = SpStSeq D;
end;

:: deftheorem Def2 defines rectangular SPRECT_1:def 2 :
for f being FinSequence of (TOP-REAL 2) holds
( f is rectangular iff ex D being non empty non horizontal non vertical compact Subset of (TOP-REAL 2) st f = SpStSeq D );

registration
let D be non empty non horizontal non vertical compact Subset of (TOP-REAL 2);
cluster SpStSeq D -> non trivial non constant special unfolded circular s.c.c. standard rectangular ;
coherence
SpStSeq D is rectangular
by Def2;
end;

registration
cluster rectangular FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being FinSequence of (TOP-REAL 2) st b1 is rectangular
proof end;
end;

theorem :: SPRECT_1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being rectangular FinSequence of (TOP-REAL 2) holds len s = 5
proof end;

registration
cluster rectangular -> non constant FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 is rectangular holds
not b1 is constant
proof end;
end;

registration
cluster non empty rectangular -> non empty special unfolded circular s.c.c. standard FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being non empty FinSequence of (TOP-REAL 2) st b1 is rectangular holds
( b1 is standard & b1 is special & b1 is unfolded & b1 is circular & b1 is s.c.c. )
proof end;
end;

theorem :: SPRECT_1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )
proof end;

theorem :: SPRECT_1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 2 = N-max (L~ s) & s /. 2 = E-max (L~ s) )
proof end;

theorem :: SPRECT_1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 3 = S-max (L~ s) & s /. 3 = E-min (L~ s) )
proof end;

theorem :: SPRECT_1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 4 = S-min (L~ s) & s /. 4 = W-min (L~ s) )
proof end;

theorem Th95: :: SPRECT_1:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r1, r2, s1, s2 being Real st r1 < r2 & s1 < s2 holds
[.r1,r2,s1,s2.] is Jordan
proof end;

registration
let f be rectangular FinSequence of (TOP-REAL 2);
cluster L~ f -> non empty Jordan compact ;
coherence
L~ f is Jordan
proof end;
end;

definition
let S be Subset of (TOP-REAL 2);
redefine attr S is Jordan means :Def3: :: SPRECT_1:def 3
( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` ) );
compatibility
( S is Jordan iff ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` ) ) )
proof end;
end;

:: deftheorem Def3 defines Jordan SPRECT_1:def 3 :
for S being Subset of (TOP-REAL 2) holds
( S is Jordan iff ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` ) ) );

theorem Th96: :: SPRECT_1:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being rectangular FinSequence of (TOP-REAL 2) holds LeftComp f misses RightComp f
proof end;

registration
let f be non constant standard special_circular_sequence;
cluster LeftComp f -> non empty ;
coherence
not LeftComp f is empty
proof end;
cluster RightComp f -> non empty ;
coherence
not RightComp f is empty
proof end;
end;

theorem :: SPRECT_1:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being rectangular FinSequence of (TOP-REAL 2) holds LeftComp f <> RightComp f
proof end;