:: SPRECT_1 semantic presentation

theorem Th1: :: SPRECT_1:1
for b1 being trivial set
for b2 being set st b2 c= b1 holds
b2 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
for b1 being Function st rng b1 is trivial holds
b1 is constant
proof end;

registration
let c1 be constant Function;
cluster rng a1 -> trivial ;
coherence
rng c1 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
for b1, b2 being FinSequence st b1 ^ b2 is constant holds
( b1 is constant & b2 is constant )
proof end;

theorem Th4: :: SPRECT_1:4
for b1, b2 being set st <*b1,b2*> is constant holds
b1 = b2
proof end;

theorem Th5: :: SPRECT_1:5
for b1, b2, b3 being set st <*b1,b2,b3*> is constant holds
( b1 = b2 & b2 = b3 & b3 = b1 )
proof end;

theorem Th6: :: SPRECT_1:6
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being non empty Subset of b1 st b2 is_a_component_of b3 holds
b2 <> {}
proof end;

theorem Th7: :: SPRECT_1:7
for b1 being TopStruct
for b2, b3 being Subset of b1 st b2 is_a_component_of b3 holds
b2 c= b3
proof end;

theorem Th8: :: SPRECT_1:8
for b1 being non empty TopSpace
for b2 being non empty Subset of b1
for b3, b4, b5 being Subset of b1 st b3 is_a_component_of b2 & b4 is_a_component_of b2 & b5 is_a_component_of b2 & b3 \/ b4 = b2 & not b5 = b3 holds
b5 = b4
proof end;

theorem Th9: :: SPRECT_1:9
for b1 being non empty TopSpace
for b2 being non empty Subset of b1
for b3, b4, b5, b6 being Subset of b1 st b3 is_a_component_of b2 & b4 is_a_component_of b2 & b5 is_a_component_of b2 & b6 is_a_component_of b2 & b3 \/ b4 = b2 & b5 \/ b6 = b2 holds
{b3,b4} = {b5,b6}
proof end;

theorem Th10: :: SPRECT_1:10
for b1, b2, b3 being Point of (TOP-REAL 2) holds L~ <*b1,b2,b3*> = (LSeg b1,b2) \/ (LSeg b2,b3)
proof end;

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

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

theorem Th11: :: SPRECT_1:11
for b1, b2 being Subset of (TOP-REAL 2) st b1 c= b2 & b2 is horizontal holds
b1 is horizontal
proof end;

theorem Th12: :: SPRECT_1:12
for b1, b2 being Subset of (TOP-REAL 2) st b1 c= b2 & b2 is vertical holds
b1 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
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( N-min b1 in b1 & N-max b1 in b1 )
proof end;

theorem Th14: :: SPRECT_1:14
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( S-min b1 in b1 & S-max b1 in b1 )
proof end;

theorem Th15: :: SPRECT_1:15
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( W-min b1 in b1 & W-max b1 in b1 )
proof end;

theorem Th16: :: SPRECT_1:16
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( E-min b1 in b1 & E-max b1 in b1 )
proof end;

theorem Th17: :: SPRECT_1:17
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( b1 is vertical iff W-bound b1 = E-bound b1 )
proof end;

theorem Th18: :: SPRECT_1:18
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( b1 is horizontal iff S-bound b1 = N-bound b1 )
proof end;

theorem Th19: :: SPRECT_1:19
for b1 being non empty compact Subset of (TOP-REAL 2) st NW-corner b1 = NE-corner b1 holds
b1 is vertical
proof end;

theorem Th20: :: SPRECT_1:20
for b1 being non empty compact Subset of (TOP-REAL 2) st SW-corner b1 = SE-corner b1 holds
b1 is vertical
proof end;

theorem Th21: :: SPRECT_1:21
for b1 being non empty compact Subset of (TOP-REAL 2) st NW-corner b1 = SW-corner b1 holds
b1 is horizontal
proof end;

theorem Th22: :: SPRECT_1:22
for b1 being non empty compact Subset of (TOP-REAL 2) st NE-corner b1 = SE-corner b1 holds
b1 is horizontal
proof end;

theorem Th23: :: SPRECT_1:23
for b1 being non empty compact Subset of (TOP-REAL 2) holds W-bound b1 <= E-bound b1
proof end;

theorem Th24: :: SPRECT_1:24
for b1 being non empty compact Subset of (TOP-REAL 2) holds S-bound b1 <= N-bound b1
proof end;

theorem Th25: :: SPRECT_1:25
for b1 being non empty compact Subset of (TOP-REAL 2) holds LSeg (SE-corner b1),(NE-corner b1) = { b2 where B is Point of (TOP-REAL 2) : ( b2 `1 = E-bound b1 & b2 `2 <= N-bound b1 & b2 `2 >= S-bound b1 ) }
proof end;

theorem Th26: :: SPRECT_1:26
for b1 being non empty compact Subset of (TOP-REAL 2) holds LSeg (SW-corner b1),(SE-corner b1) = { b2 where B is Point of (TOP-REAL 2) : ( b2 `1 <= E-bound b1 & b2 `1 >= W-bound b1 & b2 `2 = S-bound b1 ) }
proof end;

theorem Th27: :: SPRECT_1:27
for b1 being non empty compact Subset of (TOP-REAL 2) holds LSeg (NW-corner b1),(NE-corner b1) = { b2 where B is Point of (TOP-REAL 2) : ( b2 `1 <= E-bound b1 & b2 `1 >= W-bound b1 & b2 `2 = N-bound b1 ) }
proof end;

theorem Th28: :: SPRECT_1:28
for b1 being non empty compact Subset of (TOP-REAL 2) holds LSeg (SW-corner b1),(NW-corner b1) = { b2 where B is Point of (TOP-REAL 2) : ( b2 `1 = W-bound b1 & b2 `2 <= N-bound b1 & b2 `2 >= S-bound b1 ) }
proof end;

theorem Th29: :: SPRECT_1:29
for b1 being non empty compact Subset of (TOP-REAL 2) holds (LSeg (SW-corner b1),(NW-corner b1)) /\ (LSeg (NW-corner b1),(NE-corner b1)) = {(NW-corner b1)}
proof end;

theorem Th30: :: SPRECT_1:30
for b1 being non empty compact Subset of (TOP-REAL 2) holds (LSeg (NW-corner b1),(NE-corner b1)) /\ (LSeg (NE-corner b1),(SE-corner b1)) = {(NE-corner b1)}
proof end;

theorem Th31: :: SPRECT_1:31
for b1 being non empty compact Subset of (TOP-REAL 2) holds (LSeg (SE-corner b1),(NE-corner b1)) /\ (LSeg (SW-corner b1),(SE-corner b1)) = {(SE-corner b1)}
proof end;

theorem Th32: :: SPRECT_1:32
for b1 being non empty compact Subset of (TOP-REAL 2) holds (LSeg (NW-corner b1),(SW-corner b1)) /\ (LSeg (SW-corner b1),(SE-corner b1)) = {(SW-corner b1)}
proof end;

theorem Th33: :: SPRECT_1:33
for b1 being non empty non vertical compact Subset of (TOP-REAL 2) holds W-bound b1 < E-bound b1
proof end;

theorem Th34: :: SPRECT_1:34
for b1 being non empty non horizontal compact Subset of (TOP-REAL 2) holds S-bound b1 < N-bound b1
proof end;

theorem Th35: :: SPRECT_1:35
for b1 being non empty non vertical compact Subset of (TOP-REAL 2) holds LSeg (SW-corner b1),(NW-corner b1) misses LSeg (SE-corner b1),(NE-corner b1)
proof end;

theorem Th36: :: SPRECT_1:36
for b1 being non empty non horizontal compact Subset of (TOP-REAL 2) holds LSeg (SW-corner b1),(SE-corner b1) misses LSeg (NW-corner b1),(NE-corner b1)
proof end;

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

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

theorem Th37: :: SPRECT_1:37
for b1 being Subset of (TOP-REAL 2) holds (SpStSeq b1) /. 1 = NW-corner b1
proof end;

theorem Th38: :: SPRECT_1:38
for b1 being Subset of (TOP-REAL 2) holds (SpStSeq b1) /. 2 = NE-corner b1
proof end;

theorem Th39: :: SPRECT_1:39
for b1 being Subset of (TOP-REAL 2) holds (SpStSeq b1) /. 3 = SE-corner b1
proof end;

theorem Th40: :: SPRECT_1:40
for b1 being Subset of (TOP-REAL 2) holds (SpStSeq b1) /. 4 = SW-corner b1
proof end;

theorem Th41: :: SPRECT_1:41
for b1 being Subset of (TOP-REAL 2) holds (SpStSeq b1) /. 5 = NW-corner b1
proof end;

theorem Th42: :: SPRECT_1:42
for b1 being Subset of (TOP-REAL 2) holds len (SpStSeq b1) = 5
proof end;

theorem Th43: :: SPRECT_1:43
for b1 being Subset of (TOP-REAL 2) holds L~ (SpStSeq b1) = ((LSeg (NW-corner b1),(NE-corner b1)) \/ (LSeg (NE-corner b1),(SE-corner b1))) \/ ((LSeg (SE-corner b1),(SW-corner b1)) \/ (LSeg (SW-corner b1),(NW-corner b1)))
proof end;

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

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

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

theorem Th44: :: SPRECT_1:44
for b1 being non empty non horizontal non vertical compact Subset of (TOP-REAL 2) holds L~ (SpStSeq b1) = [.(W-bound b1),(E-bound b1),(S-bound b1),(N-bound b1).]
proof end;

theorem Th45: :: SPRECT_1:45
for b1 being non empty TopStruct
for b2 being Subset of b1
for b3 being RealMap of b1 holds rng (b3 || b2) = b3 .: b2
proof end;

theorem Th46: :: SPRECT_1:46
for b1 being non empty TopSpace
for b2 being non empty compact Subset of b1
for b3 being continuous RealMap of b1 holds b3 .: b2 is bounded_below
proof end;

theorem Th47: :: SPRECT_1:47
for b1 being non empty TopSpace
for b2 being non empty compact Subset of b1
for b3 being continuous RealMap of b1 holds b3 .: b2 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
for b1 being Subset of (TOP-REAL 2) holds W-bound b1 = inf (proj1 .: b1)
proof end;

theorem Th49: :: SPRECT_1:49
for b1 being Subset of (TOP-REAL 2) holds S-bound b1 = inf (proj2 .: b1)
proof end;

theorem Th50: :: SPRECT_1:50
for b1 being Subset of (TOP-REAL 2) holds N-bound b1 = sup (proj2 .: b1)
proof end;

theorem Th51: :: SPRECT_1:51
for b1 being Subset of (TOP-REAL 2) holds E-bound b1 = sup (proj1 .: b1)
proof end;

theorem Th52: :: SPRECT_1:52
for b1, b2 being non empty bounded_below Subset of REAL holds inf (b1 \/ b2) = min (inf b1),(inf b2)
proof end;

theorem Th53: :: SPRECT_1:53
for b1, b2 being non empty bounded_above Subset of REAL holds sup (b1 \/ b2) = max (sup b1),(sup b2)
proof end;

theorem Th54: :: SPRECT_1:54
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being non empty compact Subset of (TOP-REAL 2) st b1 = b2 \/ b3 holds
W-bound b1 = min (W-bound b2),(W-bound b3)
proof end;

theorem Th55: :: SPRECT_1:55
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being non empty compact Subset of (TOP-REAL 2) st b1 = b2 \/ b3 holds
S-bound b1 = min (S-bound b2),(S-bound b3)
proof end;

theorem Th56: :: SPRECT_1:56
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being non empty compact Subset of (TOP-REAL 2) st b1 = b2 \/ b3 holds
N-bound b1 = max (N-bound b2),(N-bound b3)
proof end;

theorem Th57: :: SPRECT_1:57
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being non empty compact Subset of (TOP-REAL 2) st b1 = b2 \/ b3 holds
E-bound b1 = max (E-bound b2),(E-bound b3)
proof end;

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

registration
let c1, c2 be real number ;
cluster [.a1,a2.] -> bounded ;
coherence
[.c1,c2.] 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 Th58: :: SPRECT_1:58
canceled;

theorem Th59: :: SPRECT_1:59
for b1, b2, b3 being Real st b1 <= b2 holds
( b3 in [.b1,b2.] iff ex b4 being Real st
( 0 <= b4 & b4 <= 1 & b3 = (b4 * b1) + ((1 - b4) * b2) ) )
proof end;

theorem Th60: :: SPRECT_1:60
for b1, b2 being Point of (TOP-REAL 2) st b1 `1 <= b2 `1 holds
proj1 .: (LSeg b1,b2) = [.(b1 `1 ),(b2 `1 ).]
proof end;

theorem Th61: :: SPRECT_1:61
for b1, b2 being Point of (TOP-REAL 2) st b1 `2 <= b2 `2 holds
proj2 .: (LSeg b1,b2) = [.(b1 `2 ),(b2 `2 ).]
proof end;

theorem Th62: :: SPRECT_1:62
for b1, b2 being Point of (TOP-REAL 2) st b1 `1 <= b2 `1 holds
W-bound (LSeg b1,b2) = b1 `1
proof end;

theorem Th63: :: SPRECT_1:63
for b1, b2 being Point of (TOP-REAL 2) st b1 `2 <= b2 `2 holds
S-bound (LSeg b1,b2) = b1 `2
proof end;

theorem Th64: :: SPRECT_1:64
for b1, b2 being Point of (TOP-REAL 2) st b1 `2 <= b2 `2 holds
N-bound (LSeg b1,b2) = b2 `2
proof end;

theorem Th65: :: SPRECT_1:65
for b1, b2 being Point of (TOP-REAL 2) st b1 `1 <= b2 `1 holds
E-bound (LSeg b1,b2) = b2 `1
proof end;

theorem Th66: :: SPRECT_1:66
for b1 being non empty compact Subset of (TOP-REAL 2) holds W-bound (L~ (SpStSeq b1)) = W-bound b1
proof end;

theorem Th67: :: SPRECT_1:67
for b1 being non empty compact Subset of (TOP-REAL 2) holds S-bound (L~ (SpStSeq b1)) = S-bound b1
proof end;

theorem Th68: :: SPRECT_1:68
for b1 being non empty compact Subset of (TOP-REAL 2) holds N-bound (L~ (SpStSeq b1)) = N-bound b1
proof end;

theorem Th69: :: SPRECT_1:69
for b1 being non empty compact Subset of (TOP-REAL 2) holds E-bound (L~ (SpStSeq b1)) = E-bound b1
proof end;

theorem Th70: :: SPRECT_1:70
for b1 being non empty compact Subset of (TOP-REAL 2) holds NW-corner (L~ (SpStSeq b1)) = NW-corner b1
proof end;

theorem Th71: :: SPRECT_1:71
for b1 being non empty compact Subset of (TOP-REAL 2) holds NE-corner (L~ (SpStSeq b1)) = NE-corner b1
proof end;

theorem Th72: :: SPRECT_1:72
for b1 being non empty compact Subset of (TOP-REAL 2) holds SW-corner (L~ (SpStSeq b1)) = SW-corner b1
proof end;

theorem Th73: :: SPRECT_1:73
for b1 being non empty compact Subset of (TOP-REAL 2) holds SE-corner (L~ (SpStSeq b1)) = SE-corner b1
proof end;

theorem Th74: :: SPRECT_1:74
for b1 being non empty compact Subset of (TOP-REAL 2) holds W-most (L~ (SpStSeq b1)) = LSeg (SW-corner b1),(NW-corner b1)
proof end;

theorem Th75: :: SPRECT_1:75
for b1 being non empty compact Subset of (TOP-REAL 2) holds N-most (L~ (SpStSeq b1)) = LSeg (NW-corner b1),(NE-corner b1)
proof end;

theorem Th76: :: SPRECT_1:76
for b1 being non empty compact Subset of (TOP-REAL 2) holds S-most (L~ (SpStSeq b1)) = LSeg (SW-corner b1),(SE-corner b1)
proof end;

theorem Th77: :: SPRECT_1:77
for b1 being non empty compact Subset of (TOP-REAL 2) holds E-most (L~ (SpStSeq b1)) = LSeg (SE-corner b1),(NE-corner b1)
proof end;

theorem Th78: :: SPRECT_1:78
for b1 being non empty compact Subset of (TOP-REAL 2) holds proj2 .: (LSeg (SW-corner b1),(NW-corner b1)) = [.(S-bound b1),(N-bound b1).]
proof end;

theorem Th79: :: SPRECT_1:79
for b1 being non empty compact Subset of (TOP-REAL 2) holds proj1 .: (LSeg (NW-corner b1),(NE-corner b1)) = [.(W-bound b1),(E-bound b1).]
proof end;

theorem Th80: :: SPRECT_1:80
for b1 being non empty compact Subset of (TOP-REAL 2) holds proj2 .: (LSeg (NE-corner b1),(SE-corner b1)) = [.(S-bound b1),(N-bound b1).]
proof end;

theorem Th81: :: SPRECT_1:81
for b1 being non empty compact Subset of (TOP-REAL 2) holds proj1 .: (LSeg (SE-corner b1),(SW-corner b1)) = [.(W-bound b1),(E-bound b1).]
proof end;

theorem Th82: :: SPRECT_1:82
for b1 being non empty compact Subset of (TOP-REAL 2) holds W-min (L~ (SpStSeq b1)) = SW-corner b1
proof end;

theorem Th83: :: SPRECT_1:83
for b1 being non empty compact Subset of (TOP-REAL 2) holds W-max (L~ (SpStSeq b1)) = NW-corner b1
proof end;

theorem Th84: :: SPRECT_1:84
for b1 being non empty compact Subset of (TOP-REAL 2) holds N-min (L~ (SpStSeq b1)) = NW-corner b1
proof end;

theorem Th85: :: SPRECT_1:85
for b1 being non empty compact Subset of (TOP-REAL 2) holds N-max (L~ (SpStSeq b1)) = NE-corner b1
proof end;

theorem Th86: :: SPRECT_1:86
for b1 being non empty compact Subset of (TOP-REAL 2) holds E-min (L~ (SpStSeq b1)) = SE-corner b1
proof end;

theorem Th87: :: SPRECT_1:87
for b1 being non empty compact Subset of (TOP-REAL 2) holds E-max (L~ (SpStSeq b1)) = NE-corner b1
proof end;

theorem Th88: :: SPRECT_1:88
for b1 being non empty compact Subset of (TOP-REAL 2) holds S-min (L~ (SpStSeq b1)) = SW-corner b1
proof end;

theorem Th89: :: SPRECT_1:89
for b1 being non empty compact Subset of (TOP-REAL 2) holds S-max (L~ (SpStSeq b1)) = SE-corner b1
proof end;

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

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

registration
let c1 be non empty non horizontal non vertical compact Subset of (TOP-REAL 2);
cluster SpStSeq a1 -> non trivial non constant special unfolded circular s.c.c. standard rectangular ;
coherence
SpStSeq c1 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 Th90: :: SPRECT_1:90
for b1 being rectangular FinSequence of (TOP-REAL 2) holds len b1 = 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 Th91: :: SPRECT_1:91
for b1 being rectangular FinSequence of (TOP-REAL 2) holds
( b1 /. 1 = N-min (L~ b1) & b1 /. 1 = W-max (L~ b1) )
proof end;

theorem Th92: :: SPRECT_1:92
for b1 being rectangular FinSequence of (TOP-REAL 2) holds
( b1 /. 2 = N-max (L~ b1) & b1 /. 2 = E-max (L~ b1) )
proof end;

theorem Th93: :: SPRECT_1:93
for b1 being rectangular FinSequence of (TOP-REAL 2) holds
( b1 /. 3 = S-max (L~ b1) & b1 /. 3 = E-min (L~ b1) )
proof end;

theorem Th94: :: SPRECT_1:94
for b1 being rectangular FinSequence of (TOP-REAL 2) holds
( b1 /. 4 = S-min (L~ b1) & b1 /. 4 = W-min (L~ b1) )
proof end;

theorem Th95: :: SPRECT_1:95
for b1, b2, b3, b4 being Real st b1 < b2 & b3 < b4 holds
[.b1,b2,b3,b4.] is Jordan
proof end;

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

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

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

theorem Th96: :: SPRECT_1:96
for b1 being rectangular FinSequence of (TOP-REAL 2) holds LeftComp b1 misses RightComp b1
proof end;

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

theorem Th97: :: SPRECT_1:97
for b1 being rectangular FinSequence of (TOP-REAL 2) holds LeftComp b1 <> RightComp b1
proof end;