:: SPRECT_1 semantic presentation

begin

registration
cluster non empty V19() V22( NAT ) Function-like constant V32() FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st
( not b1 is empty & b1 is constant )
proof
take  <*0*> ; ::_thesis: ( not <*0*> is empty & <*0*> is constant )
thus  ( not <*0*> is empty & <*0*> is constant ) ; ::_thesis: verum
end;
end;

theorem Th1: :: SPRECT_1:1
for f, g being FinSequence st f ^ g is constant holds
( f is constant & g is constant )
proof
let f, g be FinSequence; ::_thesis: ( f ^ g is constant implies ( f is constant & g is constant ) )
assume  f ^ g is constant ; ::_thesis: ( f is constant & g is constant )
then reconsider h = f ^ g as constant FinSequence ;
 rng f c= rng h by FINSEQ_1:29;
hence  f is constant ; ::_thesis: g is constant
 rng g c= rng h by FINSEQ_1:30;
hence  g is constant ; ::_thesis: verum
end;

theorem Th2: :: SPRECT_1:2
for x, y being set st <*x,y*> is constant holds
x = y
proof
let x, y be set ; ::_thesis: ( <*x,y*> is constant implies x = y )
A1: rng <*x,y*> = rng (<*x*> ^ <*y*>) by FINSEQ_1:def_9
.= (rng <*x*>) \/ (rng <*y*>) by FINSEQ_1:31
.= (rng <*x*>) \/ {y} by FINSEQ_1:38
.= {x} \/ {y} by FINSEQ_1:38
.= {x,y} by ENUMSET1:1 ;
A2: y in {x,y} by TARSKI:def_2;
assume  <*x,y*> is constant ; ::_thesis: x = y
then reconsider s = <*x,y*> as constant Function ;
A3: x in {x,y} by TARSKI:def_2;
 rng s is trivial ;
hence  x = y by A1, A3, A2, ZFMISC_1:def_10; ::_thesis: verum
end;

theorem Th3: :: SPRECT_1:3
for x, y, z being set st <*x,y,z*> is constant holds
( x = y & y = z & z = x )
proof
let x, y, z be set ; ::_thesis: ( <*x,y,z*> is constant implies ( x = y & y = z & z = x ) )
A1: rng <*x,y,z*> = rng ((<*x*> ^ <*y*>) ^ <*z*>) by FINSEQ_1:def_10
.= (rng (<*x*> ^ <*y*>)) \/ (rng <*z*>) by FINSEQ_1:31
.= (rng (<*x*> ^ <*y*>)) \/ {z} by FINSEQ_1:38
.= ((rng <*x*>) \/ (rng <*y*>)) \/ {z} by FINSEQ_1:31
.= ((rng <*x*>) \/ {y}) \/ {z} by FINSEQ_1:38
.= ({x} \/ {y}) \/ {z} by FINSEQ_1:38
.= {x,y} \/ {z} by ENUMSET1:1
.= {x,y,z} by ENUMSET1:3 ;
A2: y in {x,y,z} by ENUMSET1:def_1;
assume  <*x,y,z*> is constant ; ::_thesis: ( x = y & y = z & z = x )
then reconsider s = <*x,y,z*> as constant Function ;
A3: x in {x,y,z} by ENUMSET1:def_1;
A4: z in {x,y,z} by ENUMSET1:def_1;
 rng s is trivial ;
hence  ( x = y & y = z & z = x ) by A1, A3, A2, A4, ZFMISC_1:def_10; ::_thesis: verum
end;

begin

theorem Th4: :: SPRECT_1:4
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
let GX be non empty TopSpace; ::_thesis: for A being Subset of GX
for B being non empty Subset of GX st A is_a_component_of B holds
A <> {}
let A be Subset of GX; ::_thesis: for B being non empty Subset of GX st A is_a_component_of B holds
A <> {}
let B be non empty Subset of GX; ::_thesis: ( A is_a_component_of B implies A <> {} )
assume  A is_a_component_of B ; ::_thesis: A <> {}
then consider B1 being Subset of (GX | B) such that
A1: B1 = A and
A2: B1 is a_component by CONNSP_1:def_6;
 B1 <> {} (GX | B) by A2, CONNSP_1:32;
hence  A <> {} by A1; ::_thesis: verum
end;

theorem Th5: :: SPRECT_1:5
for GX being TopStruct
for A, B being Subset of GX st A is_a_component_of B holds
A c= B
proof
let GX be TopStruct ; ::_thesis: for A, B being Subset of GX st A is_a_component_of B holds
A c= B
let A, B be Subset of GX; ::_thesis: ( A is_a_component_of B implies A c= B )
assume  A is_a_component_of B ; ::_thesis: A c= B
then A1: ex B1 being Subset of (GX | B) st
( B1 = A & B1 is a_component ) by CONNSP_1:def_6;
 the carrier of (GX | B) = B by PRE_TOPC:8;
hence  A c= B by A1; ::_thesis: verum
end;

theorem Th6: :: SPRECT_1:6
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
let T be non empty TopSpace; ::_thesis: 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
let A be non empty Subset of T; ::_thesis: 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
let B1, B2, S be Subset of T; ::_thesis: ( B1 is_a_component_of A & B2 is_a_component_of A & S is_a_component_of A & B1 \/ B2 = A & not S = B1 implies S = B2 )
assume that
A1: B1 is_a_component_of A and
A2: B2 is_a_component_of A and
A3: S is_a_component_of A and
A4: B1 \/ B2 = A ; ::_thesis: ( S = B1 or S = B2 )
 S c= A by A3, Th5;
then  S meets A by A3, Th4, XBOOLE_1:67;
then  ( S meets B1 or S meets B2 ) by A4, XBOOLE_1:70;
hence  ( S = B1 or S = B2 ) by A1, A2, A3, GOBOARD9:1; ::_thesis: verum
end;

theorem Th7: :: SPRECT_1:7
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
let T be non empty TopSpace; ::_thesis: 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}
let A be non empty Subset of T; ::_thesis: 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}
let B1, B2, C1, C2 be Subset of T; ::_thesis: ( 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 implies {B1,B2} = {C1,C2} )
assume that
A1: B1 is_a_component_of A and
A2: B2 is_a_component_of A and
A3: C1 is_a_component_of A and
A4: C2 is_a_component_of A and
A5: B1 \/ B2 = A and
A6: C1 \/ C2 = A ; ::_thesis: {B1,B2} = {C1,C2}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{B1,B2}_iff_(_x_=_C1_or_x_=_C2_)_)
let x be set ; ::_thesis: ( x in {B1,B2} iff ( x = C1 or x = C2 ) )
 ( ( ( not x = B1 & not x = B2 ) or x = C1 or x = C2 ) & ( ( not x = C1 & not x = C2 ) or x = B1 or x = B2 ) ) by A1, A2, A3, A4, A5, A6, Th6;
hence  ( x in {B1,B2} iff ( x = C1 or x = C2 ) ) by TARSKI:def_2; ::_thesis: verum
end;
hence  {B1,B2} = {C1,C2} by TARSKI:def_2; ::_thesis: verum
end;

begin


theorem Th8: :: SPRECT_1:8
for p, q, r being Point of (TOP-REAL 2) holds L~ <*p,q,r*> = (LSeg (p,q)) \/ (LSeg (q,r))
proof
let p, q, r be Point of (TOP-REAL 2); ::_thesis: L~ <*p,q,r*> = (LSeg (p,q)) \/ (LSeg (q,r))
A1: <*p,q*> /. 2 = q by FINSEQ_4:17;
A2: <*r*> /. 1 = r by FINSEQ_4:16;
A3: <*p,q,r*> = <*p,q*> ^ <*r*> by FINSEQ_1:43;
 len <*p,q*> = 2 by FINSEQ_1:44;
hence  L~ <*p,q,r*> = ((L~ <*p,q*>) \/ (LSeg (q,r))) \/ (L~ <*r*>) by A1, A2, A3, SPPOL_2:23
.= ((L~ <*p,q*>) \/ (LSeg (q,r))) \/ {} by SPPOL_2:12
.= (LSeg (p,q)) \/ (LSeg (q,r)) by SPPOL_2:21 ;
::_thesis: verum
end;

registration
let n be Element of NAT ;
let f be non trivial FinSequence of (TOP-REAL n);
cluster L~ f ->  non empty ;
coherence
 not L~ f is empty
proof
A1: len f <> 1 by NAT_D:60;
 len f <> 0 by NAT_D:60;
hence  not L~ f is empty by A1, TOPREAL1:22; ::_thesis: verum
end;
end;

registration
let f be FinSequence of (TOP-REAL 2);
cluster L~ f ->  compact ;
coherence
 L~ f is compact
proof
defpred S1[ Element of NAT ] means  for f being FinSequence of (TOP-REAL 2) st len f = f holds
L~ f is compact ;
A1: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: for f being FinSequence of (TOP-REAL 2) st len f = m holds
L~ f is compact ; ::_thesis: S1[m + 1]
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f = m + 1 implies L~ f is compact )
assume A3: len f = m + 1 ; ::_thesis: L~ f is compact
then consider q being FinSequence of (TOP-REAL 2), x being Point of (TOP-REAL 2) such that
A4: f = q ^ <*x*> by FINSEQ_2:19;
len f = (len q) + (len <*x*>) by A4, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:39 ;
then A5: L~ q is compact by A2, A3;
percases ( q is empty or not q is empty ) ;
suppose q is empty ; ::_thesis: L~ f is compact
then  L~ f = L~ <*x*> by A4, FINSEQ_1:34
.= {} (TOP-REAL 2) by SPPOL_2:12 ;
hence  L~ f is compact ; ::_thesis: verum
end;
suppose not q is empty ; ::_thesis: L~ f is compact
then  L~ f = ((L~ q) \/ (LSeg ((q /. (len q)),(<*x*> /. 1)))) \/ (L~ <*x*>) by A4, SPPOL_2:23
.= ((L~ q) \/ (LSeg ((q /. (len q)),(<*x*> /. 1)))) \/ {} by SPPOL_2:12
.= (L~ q) \/ (LSeg ((q /. (len q)),(<*x*> /. 1))) ;
hence  L~ f is compact by A5, COMPTS_1:10; ::_thesis: verum
end;
end;
end;
A6: S1[ 0 ]
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f = 0 implies L~ f is compact )
assume  len f = 0 ; ::_thesis: L~ f is compact
then  L~ f = {} (TOP-REAL 2) by TOPREAL1:22;
hence  L~ f is compact ; ::_thesis: verum
end;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A6, A1);
hence  L~ f is compact ; ::_thesis: verum
end;
end;

theorem Th9: :: SPRECT_1:9
for A, B being Subset of (TOP-REAL 2) st A c= B & B is horizontal holds
A is horizontal
proof
let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A c= B & B is horizontal implies A is horizontal )
assume that
A1: A c= B and
A2: B is horizontal ; ::_thesis: A is horizontal
let p be Point of (TOP-REAL 2); :: according to SPPOL_1:def_2 ::_thesis: for b1 being Element of the carrier of (TOP-REAL 2) holds
( not p in A or not b1 in A or p `2 = b1 `2 )
let q be Point of (TOP-REAL 2); ::_thesis: ( not p in A or not q in A or p `2 = q `2 )
assume that
A3: p in A and
A4: q in A ; ::_thesis: p `2 = q `2
thus  p `2 = q `2 by A1, A2, A3, A4, SPPOL_1:def_2; ::_thesis: verum
end;

theorem Th10: :: SPRECT_1:10
for A, B being Subset of (TOP-REAL 2) st A c= B & B is vertical holds
A is vertical
proof
let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A c= B & B is vertical implies A is vertical )
assume that
A1: A c= B and
A2: B is vertical ; ::_thesis: A is vertical
let p be Point of (TOP-REAL 2); :: according to SPPOL_1:def_3 ::_thesis: for b1 being Element of the carrier of (TOP-REAL 2) holds
( not p in A or not b1 in A or p `1 = b1 `1 )
let q be Point of (TOP-REAL 2); ::_thesis: ( not p in A or not q in A or p `1 = q `1 )
assume that
A3: p in A and
A4: q in A ; ::_thesis: p `1 = q `1
thus  p `1 = q `1 by A1, A2, A3, A4, SPPOL_1:def_3; ::_thesis: verum
end;

registration
cluster R^2-unit_square  ->  special_polygonal non horizontal non vertical ;
coherence
 ( R^2-unit_square is special_polygonal & not R^2-unit_square is horizontal & not R^2-unit_square is vertical )
proof
A1: |[0,1]| `2 = 1 by EUCLID:52;
 |[0,0]| `2 = 0 by EUCLID:52;
then A2: not LSeg (|[0,0]|,|[0,1]|) is horizontal by A1, SPPOL_1:15;
set Sq = R^2-unit_square ;
thus  R^2-unit_square is special_polygonal ; ::_thesis: ( not R^2-unit_square is horizontal & not R^2-unit_square is vertical )
A3: (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) c= R^2-unit_square by XBOOLE_1:7;
 LSeg (|[0,0]|,|[0,1]|) c= (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) by XBOOLE_1:7;
hence  not R^2-unit_square is horizontal by A3, A2, Th9, XBOOLE_1:1; ::_thesis: not R^2-unit_square is vertical
A4: |[1,1]| `1 = 1 by EUCLID:52;
 |[0,1]| `1 = 0 by EUCLID:52;
then A5: not LSeg (|[0,1]|,|[1,1]|) is vertical by A4, SPPOL_1:16;
 LSeg (|[0,1]|,|[1,1]|) c= (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) by XBOOLE_1:7;
hence  not R^2-unit_square is vertical by A3, A5, Th10, XBOOLE_1:1; ::_thesis: verum
end;
end;

registration
cluster non empty compact non horizontal non vertical for 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
take  R^2-unit_square ; ::_thesis: ( not R^2-unit_square is vertical & not R^2-unit_square is horizontal & not R^2-unit_square is empty & R^2-unit_square is compact )
thus  ( not R^2-unit_square is vertical & not R^2-unit_square is horizontal & not R^2-unit_square is empty & R^2-unit_square is compact ) ; ::_thesis: verum
end;
end;

begin

theorem Th11: :: SPRECT_1:11
for C being non empty compact Subset of (TOP-REAL 2) holds
( N-min C in C & N-max C in C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( N-min C in C & N-max C in C )
A1: N-min C in N-most C by PSCOMP_1:42;
A2: N-max C in N-most C by PSCOMP_1:42;
 N-most C c= C by XBOOLE_1:17;
hence  ( N-min C in C & N-max C in C ) by A1, A2; ::_thesis: verum
end;

theorem Th12: :: SPRECT_1:12
for C being non empty compact Subset of (TOP-REAL 2) holds
( S-min C in C & S-max C in C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( S-min C in C & S-max C in C )
A1: S-min C in S-most C by PSCOMP_1:58;
A2: S-max C in S-most C by PSCOMP_1:58;
 S-most C c= C by XBOOLE_1:17;
hence  ( S-min C in C & S-max C in C ) by A1, A2; ::_thesis: verum
end;

theorem Th13: :: SPRECT_1:13
for C being non empty compact Subset of (TOP-REAL 2) holds
( W-min C in C & W-max C in C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( W-min C in C & W-max C in C )
A1: W-min C in W-most C by PSCOMP_1:34;
A2: W-max C in W-most C by PSCOMP_1:34;
 W-most C c= C by XBOOLE_1:17;
hence  ( W-min C in C & W-max C in C ) by A1, A2; ::_thesis: verum
end;

theorem Th14: :: SPRECT_1:14
for C being non empty compact Subset of (TOP-REAL 2) holds
( E-min C in C & E-max C in C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( E-min C in C & E-max C in C )
A1: E-min C in E-most C by PSCOMP_1:50;
A2: E-max C in E-most C by PSCOMP_1:50;
 E-most C c= C by XBOOLE_1:17;
hence  ( E-min C in C & E-max C in C ) by A1, A2; ::_thesis: verum
end;

theorem Th15: :: SPRECT_1:15
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is vertical iff W-bound C = E-bound C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is vertical iff W-bound C = E-bound C )
thus  ( C is vertical implies W-bound C = E-bound C ) ::_thesis: ( W-bound C = E-bound C implies C is vertical )
proof
A1: E-min C in C by Th14;
A2: W-min C in C by Th13;
assume A3: C is vertical ; ::_thesis: W-bound C = E-bound C
thus  W-bound C = (W-min C) `1 by EUCLID:52
.= (E-min C) `1 by A3, A2, A1, SPPOL_1:def_3
.= E-bound C by EUCLID:52 ; ::_thesis: verum
end;
assume A4: W-bound C = E-bound C ; ::_thesis: C is vertical
let p be Point of (TOP-REAL 2); :: according to SPPOL_1:def_3 ::_thesis: for b1 being Element of the carrier of (TOP-REAL 2) holds
( not p in C or not b1 in C or p `1 = b1 `1 )
let q be Point of (TOP-REAL 2); ::_thesis: ( not p in C or not q in C or p `1 = q `1 )
assume that
A5: p in C and
A6: q in C ; ::_thesis: p `1 = q `1
A7: p `1 <= E-bound C by A5, PSCOMP_1:24;
 W-bound C <= p `1 by A5, PSCOMP_1:24;
then A8: p `1 = W-bound C by A4, A7, XXREAL_0:1;
A9: q `1 <= E-bound C by A6, PSCOMP_1:24;
 W-bound C <= q `1 by A6, PSCOMP_1:24;
hence  p `1 = q `1 by A4, A9, A8, XXREAL_0:1; ::_thesis: verum
end;

theorem Th16: :: SPRECT_1:16
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is horizontal iff S-bound C = N-bound C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is horizontal iff S-bound C = N-bound C )
thus  ( C is horizontal implies S-bound C = N-bound C ) ::_thesis: ( S-bound C = N-bound C implies C is horizontal )
proof
A1: N-min C in C by Th11;
A2: S-min C in C by Th12;
assume A3: C is horizontal ; ::_thesis: S-bound C = N-bound C
thus  S-bound C = (S-min C) `2 by EUCLID:52
.= (N-min C) `2 by A3, A2, A1, SPPOL_1:def_2
.= N-bound C by EUCLID:52 ; ::_thesis: verum
end;
assume A4: S-bound C = N-bound C ; ::_thesis: C is horizontal
let p be Point of (TOP-REAL 2); :: according to SPPOL_1:def_2 ::_thesis: for b1 being Element of the carrier of (TOP-REAL 2) holds
( not p in C or not b1 in C or p `2 = b1 `2 )
let q be Point of (TOP-REAL 2); ::_thesis: ( not p in C or not q in C or p `2 = q `2 )
assume that
A5: p in C and
A6: q in C ; ::_thesis: p `2 = q `2
A7: p `2 <= N-bound C by A5, PSCOMP_1:24;
 S-bound C <= p `2 by A5, PSCOMP_1:24;
then A8: p `2 = S-bound C by A4, A7, XXREAL_0:1;
A9: q `2 <= N-bound C by A6, PSCOMP_1:24;
 S-bound C <= q `2 by A6, PSCOMP_1:24;
hence  p `2 = q `2 by A4, A9, A8, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_1:17
for C being non empty compact Subset of (TOP-REAL 2) st NW-corner C = NE-corner C holds
C is vertical
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( NW-corner C = NE-corner C implies C is vertical )
assume  NW-corner C = NE-corner C ; ::_thesis: C is vertical
then  W-bound C = E-bound C by SPPOL_2:1;
hence  C is vertical by Th15; ::_thesis: verum
end;

theorem :: SPRECT_1:18
for C being non empty compact Subset of (TOP-REAL 2) st SW-corner C = SE-corner C holds
C is vertical
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( SW-corner C = SE-corner C implies C is vertical )
assume  SW-corner C = SE-corner C ; ::_thesis: C is vertical
then  W-bound C = E-bound C by SPPOL_2:1;
hence  C is vertical by Th15; ::_thesis: verum
end;

theorem :: SPRECT_1:19
for C being non empty compact Subset of (TOP-REAL 2) st NW-corner C = SW-corner C holds
C is horizontal
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( NW-corner C = SW-corner C implies C is horizontal )
assume  NW-corner C = SW-corner C ; ::_thesis: C is horizontal
then  S-bound C = N-bound C by SPPOL_2:1;
hence  C is horizontal by Th16; ::_thesis: verum
end;

theorem :: SPRECT_1:20
for C being non empty compact Subset of (TOP-REAL 2) st NE-corner C = SE-corner C holds
C is horizontal
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( NE-corner C = SE-corner C implies C is horizontal )
assume  NE-corner C = SE-corner C ; ::_thesis: C is horizontal
then  S-bound C = N-bound C by SPPOL_2:1;
hence  C is horizontal by Th16; ::_thesis: verum
end;


theorem Th21: :: SPRECT_1:21
for C being non empty compact Subset of (TOP-REAL 2) holds W-bound C <= E-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: W-bound C <= E-bound C
A1: N-min C in C by Th11;
then A2: (N-min C) `1 <= E-bound C by PSCOMP_1:24;
 W-bound C <= (N-min C) `1 by A1, PSCOMP_1:24;
hence  W-bound C <= E-bound C by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem Th22: :: SPRECT_1:22
for C being non empty compact Subset of (TOP-REAL 2) holds S-bound C <= N-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: S-bound C <= N-bound C
A1: W-min C in C by Th13;
then A2: (W-min C) `2 <= N-bound C by PSCOMP_1:24;
 S-bound C <= (W-min C) `2 by A1, PSCOMP_1:24;
hence  S-bound C <= N-bound C by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem Th23: :: SPRECT_1:23
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: 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 )  }
set L =  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  ;
set q1 = SE-corner C;
set q2 = NE-corner C;
A1: (SE-corner C) `1 = E-bound C by EUCLID:52;
A2: (SE-corner C) `2 = S-bound C by EUCLID:52;
A3: (NE-corner C) `1 = E-bound C by EUCLID:52;
A4: (NE-corner C) `2 = N-bound C by EUCLID:52;
A5: S-bound C <= N-bound C by Th22;
thus  LSeg ((SE-corner C),(NE-corner C)) 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 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  c= LSeg ((SE-corner C),(NE-corner C))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg ((SE-corner C),(NE-corner C)) or a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  )
assume A6: a in LSeg ((SE-corner C),(NE-corner C)) ; ::_thesis: a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }
then reconsider p = a as Point of (TOP-REAL 2) ;
A7: p `1 = E-bound C by A1, A3, A6, GOBOARD7:5;
A8: p `2 >= S-bound C by A2, A4, A5, A6, TOPREAL1:4;
 p `2 <= N-bound C by A2, A4, A5, A6, TOPREAL1:4;
hence  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  by A7, A8; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  or a in LSeg ((SE-corner C),(NE-corner C)) )
assume  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  ; ::_thesis: a in LSeg ((SE-corner C),(NE-corner C))
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
hence  a in LSeg ((SE-corner C),(NE-corner C)) by A1, A2, A3, A4, GOBOARD7:7; ::_thesis: verum
end;

theorem Th24: :: SPRECT_1:24
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: 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 )  }
set L =  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  ;
set q1 = SW-corner C;
set q2 = SE-corner C;
A1: (SW-corner C) `1 = W-bound C by EUCLID:52;
A2: (SE-corner C) `2 = S-bound C by EUCLID:52;
A3: (SW-corner C) `2 = S-bound C by EUCLID:52;
A4: (SE-corner C) `1 = E-bound C by EUCLID:52;
A5: W-bound C <= E-bound C by Th21;
thus  LSeg ((SW-corner C),(SE-corner C)) 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 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  c= LSeg ((SW-corner C),(SE-corner C))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg ((SW-corner C),(SE-corner C)) or a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  )
assume A6: a in LSeg ((SW-corner C),(SE-corner C)) ; ::_thesis: a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }
then reconsider p = a as Point of (TOP-REAL 2) ;
A7: p `2 = S-bound C by A3, A2, A6, GOBOARD7:6;
A8: p `1 >= W-bound C by A1, A4, A5, A6, TOPREAL1:3;
 p `1 <= E-bound C by A1, A4, A5, A6, TOPREAL1:3;
hence  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  by A7, A8; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  or a in LSeg ((SW-corner C),(SE-corner C)) )
assume  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  ; ::_thesis: a in LSeg ((SW-corner C),(SE-corner C))
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C ) ;
hence  a in LSeg ((SW-corner C),(SE-corner C)) by A1, A3, A4, A2, GOBOARD7:8; ::_thesis: verum
end;

theorem Th25: :: SPRECT_1:25
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: 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 )  }
set L =  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  ;
set q1 = NW-corner C;
set q2 = NE-corner C;
A1: (NW-corner C) `1 = W-bound C by EUCLID:52;
A2: (NE-corner C) `2 = N-bound C by EUCLID:52;
A3: (NW-corner C) `2 = N-bound C by EUCLID:52;
A4: (NE-corner C) `1 = E-bound C by EUCLID:52;
A5: W-bound C <= E-bound C by Th21;
thus  LSeg ((NW-corner C),(NE-corner C)) 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 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  c= LSeg ((NW-corner C),(NE-corner C))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg ((NW-corner C),(NE-corner C)) or a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  )
assume A6: a in LSeg ((NW-corner C),(NE-corner C)) ; ::_thesis: a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }
then reconsider p = a as Point of (TOP-REAL 2) ;
A7: p `2 = N-bound C by A3, A2, A6, GOBOARD7:6;
A8: p `1 >= W-bound C by A1, A4, A5, A6, TOPREAL1:3;
 p `1 <= E-bound C by A1, A4, A5, A6, TOPREAL1:3;
hence  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  by A7, A8; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  or a in LSeg ((NW-corner C),(NE-corner C)) )
assume  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  ; ::_thesis: a in LSeg ((NW-corner C),(NE-corner C))
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) ;
hence  a in LSeg ((NW-corner C),(NE-corner C)) by A1, A3, A4, A2, GOBOARD7:8; ::_thesis: verum
end;

theorem Th26: :: SPRECT_1:26
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: 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 )  }
set L =  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  ;
set q1 = SW-corner C;
set q2 = NW-corner C;
A1: (SW-corner C) `1 = W-bound C by EUCLID:52;
A2: (SW-corner C) `2 = S-bound C by EUCLID:52;
A3: (NW-corner C) `1 = W-bound C by EUCLID:52;
A4: (NW-corner C) `2 = N-bound C by EUCLID:52;
A5: S-bound C <= N-bound C by Th22;
thus  LSeg ((SW-corner C),(NW-corner C)) 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 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  c= LSeg ((SW-corner C),(NW-corner C))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg ((SW-corner C),(NW-corner C)) or a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  )
assume A6: a in LSeg ((SW-corner C),(NW-corner C)) ; ::_thesis: a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }
then reconsider p = a as Point of (TOP-REAL 2) ;
A7: p `1 = W-bound C by A1, A3, A6, GOBOARD7:5;
A8: p `2 >= S-bound C by A2, A4, A5, A6, TOPREAL1:4;
 p `2 <= N-bound C by A2, A4, A5, A6, TOPREAL1:4;
hence  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  by A7, A8; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  or a in LSeg ((SW-corner C),(NW-corner C)) )
assume  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  ; ::_thesis: a in LSeg ((SW-corner C),(NW-corner C))
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
hence  a in LSeg ((SW-corner C),(NW-corner C)) by A1, A2, A3, A4, GOBOARD7:7; ::_thesis: verum
end;

theorem :: SPRECT_1:27
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) = {(NW-corner C)}
 for a being set holds
( a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) iff a = NW-corner C )
proof
let a be set ; ::_thesis: ( a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) iff a = NW-corner C )
thus  ( a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) implies a = NW-corner C ) ::_thesis: ( a = NW-corner C implies a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) )
proof
assume A1: a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) ; ::_thesis: a = NW-corner C
then  a in LSeg ((NW-corner C),(NE-corner C)) by XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  by Th25;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) ;
 a in LSeg ((SW-corner C),(NW-corner C)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  by Th26;
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
hence  a = NW-corner C by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = NW-corner C ; ::_thesis: a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C)))
then A4: a in LSeg ((NW-corner C),(NE-corner C)) by RLTOPSP1:68;
 a in LSeg ((SW-corner C),(NW-corner C)) by A3, RLTOPSP1:68;
hence  a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) = {(NW-corner C)} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th28: :: SPRECT_1:28
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) = {(NE-corner C)}
 for a being set holds
( a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) iff a = NE-corner C )
proof
let a be set ; ::_thesis: ( a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) iff a = NE-corner C )
thus  ( a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) implies a = NE-corner C ) ::_thesis: ( a = NE-corner C implies a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) )
proof
assume A1: a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) ; ::_thesis: a = NE-corner C
then  a in LSeg ((NE-corner C),(SE-corner C)) by XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  by Th23;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
 a in LSeg ((NW-corner C),(NE-corner C)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C )  }  by Th25;
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) ;
hence  a = NE-corner C by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = NE-corner C ; ::_thesis: a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C)))
then A4: a in LSeg ((NE-corner C),(SE-corner C)) by RLTOPSP1:68;
 a in LSeg ((NW-corner C),(NE-corner C)) by A3, RLTOPSP1:68;
hence  a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) = {(NE-corner C)} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th29: :: SPRECT_1:29
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: (LSeg ((SE-corner C),(NE-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) = {(SE-corner C)}
 for a being set holds
( a in (LSeg ((NE-corner C),(SE-corner C))) /\ (LSeg ((SE-corner C),(SW-corner C))) iff a = SE-corner C )
proof
let a be set ; ::_thesis: ( a in (LSeg ((NE-corner C),(SE-corner C))) /\ (LSeg ((SE-corner C),(SW-corner C))) iff a = SE-corner C )
thus  ( a in (LSeg ((NE-corner C),(SE-corner C))) /\ (LSeg ((SE-corner C),(SW-corner C))) implies a = SE-corner C ) ::_thesis: ( a = SE-corner C implies a in (LSeg ((NE-corner C),(SE-corner C))) /\ (LSeg ((SE-corner C),(SW-corner C))) )
proof
assume A1: a in (LSeg ((NE-corner C),(SE-corner C))) /\ (LSeg ((SE-corner C),(SW-corner C))) ; ::_thesis: a = SE-corner C
then  a in LSeg ((SE-corner C),(SW-corner C)) by XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  by Th24;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C ) ;
 a in LSeg ((NE-corner C),(SE-corner C)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  by Th23;
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
hence  a = SE-corner C by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = SE-corner C ; ::_thesis: a in (LSeg ((NE-corner C),(SE-corner C))) /\ (LSeg ((SE-corner C),(SW-corner C)))
then A4: a in LSeg ((SE-corner C),(SW-corner C)) by RLTOPSP1:68;
 a in LSeg ((NE-corner C),(SE-corner C)) by A3, RLTOPSP1:68;
hence  a in (LSeg ((NE-corner C),(SE-corner C))) /\ (LSeg ((SE-corner C),(SW-corner C))) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (LSeg ((SE-corner C),(NE-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) = {(SE-corner C)} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th30: :: SPRECT_1:30
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) = {(SW-corner C)}
 for a being set holds
( a in (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) iff a = SW-corner C )
proof
let a be set ; ::_thesis: ( a in (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) iff a = SW-corner C )
thus  ( a in (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) implies a = SW-corner C ) ::_thesis: ( a = SW-corner C implies a in (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) )
proof
assume A1: a in (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) ; ::_thesis: a = SW-corner C
then  a in LSeg ((SW-corner C),(SE-corner C)) by XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C )  }  by Th24;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = S-bound C ) ;
 a in LSeg ((NW-corner C),(SW-corner C)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C )  }  by Th26;
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
hence  a = SW-corner C by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = SW-corner C ; ::_thesis: a in (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C)))
then A4: a in LSeg ((SW-corner C),(SE-corner C)) by RLTOPSP1:68;
 a in LSeg ((NW-corner C),(SW-corner C)) by A3, RLTOPSP1:68;
hence  a in (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) = {(SW-corner C)} by TARSKI:def_1; ::_thesis: verum
end;

begin


theorem Th31: :: SPRECT_1:31
for D1 being non empty compact non vertical Subset of (TOP-REAL 2) holds W-bound D1 < E-bound D1
proof
let D1 be non empty compact non vertical Subset of (TOP-REAL 2); ::_thesis: W-bound D1 < E-bound D1
A1: W-bound D1 <> E-bound D1 by Th15;
 W-bound D1 <= E-bound D1 by Th21;
hence  W-bound D1 < E-bound D1 by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th32: :: SPRECT_1:32
for D2 being non empty compact non horizontal Subset of (TOP-REAL 2) holds S-bound D2 < N-bound D2
proof
let D2 be non empty compact non horizontal Subset of (TOP-REAL 2); ::_thesis: S-bound D2 < N-bound D2
A1: S-bound D2 <> N-bound D2 by Th16;
 S-bound D2 <= N-bound D2 by Th22;
hence  S-bound D2 < N-bound D2 by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th33: :: SPRECT_1:33
for D1 being non empty compact non vertical Subset of (TOP-REAL 2) holds LSeg ((SW-corner D1),(NW-corner D1)) misses LSeg ((SE-corner D1),(NE-corner D1))
proof
let D1 be non empty compact non vertical Subset of (TOP-REAL 2); ::_thesis: LSeg ((SW-corner D1),(NW-corner D1)) misses LSeg ((SE-corner D1),(NE-corner D1))
assume  (LSeg ((SW-corner D1),(NW-corner D1))) /\ (LSeg ((SE-corner D1),(NE-corner D1))) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider a being set  such that
A1: a in (LSeg ((SW-corner D1),(NW-corner D1))) /\ (LSeg ((SE-corner D1),(NE-corner D1))) by XBOOLE_0:def_1;
 a in LSeg ((NE-corner D1),(SE-corner D1)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 )  }  by Th23;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = E-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 ) ;
 a in LSeg ((NW-corner D1),(SW-corner D1)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 )  }  by Th26;
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = W-bound D1 & p `2 <= N-bound D1 & p `2 >= S-bound D1 ) ;
hence  contradiction by A2, Th15; ::_thesis: verum
end;

theorem Th34: :: SPRECT_1:34
for D2 being non empty compact non horizontal Subset of (TOP-REAL 2) holds LSeg ((SW-corner D2),(SE-corner D2)) misses LSeg ((NW-corner D2),(NE-corner D2))
proof
let D2 be non empty compact non horizontal Subset of (TOP-REAL 2); ::_thesis: LSeg ((SW-corner D2),(SE-corner D2)) misses LSeg ((NW-corner D2),(NE-corner D2))
assume  (LSeg ((SW-corner D2),(SE-corner D2))) /\ (LSeg ((NW-corner D2),(NE-corner D2))) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider a being set  such that
A1: a in (LSeg ((SW-corner D2),(SE-corner D2))) /\ (LSeg ((NW-corner D2),(NE-corner D2))) by XBOOLE_0:def_1;
 a in LSeg ((NE-corner D2),(NW-corner D2)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound D2 & p `1 >= W-bound D2 & p `2 = N-bound D2 )  }  by Th25;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound D2 & p `1 >= W-bound D2 & p `2 = N-bound D2 ) ;
 a in LSeg ((SE-corner D2),(SW-corner D2)) by A1, XBOOLE_0:def_4;
then  a in  {  p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound D2 & p `1 >= W-bound D2 & p `2 = S-bound D2 )  }  by Th24;
then  ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound D2 & p `1 >= W-bound D2 & p `2 = S-bound D2 ) ;
hence  contradiction by A2, Th16; ::_thesis: verum
end;

begin

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 Th35: :: SPRECT_1:35
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 1 = NW-corner S
proof
let S be Subset of (TOP-REAL 2); ::_thesis: (SpStSeq S) /. 1 = NW-corner S
 1 in dom <*(NW-corner S),(NE-corner S),(SE-corner S)*> by TOPREAL3:1;
hence (SpStSeq S) /. 1 = <*(NW-corner S),(NE-corner S),(SE-corner S)*> /. 1 by FINSEQ_4:68
.= NW-corner S by FINSEQ_4:18 ;
::_thesis: verum
end;

theorem Th36: :: SPRECT_1:36
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 2 = NE-corner S
proof
let S be Subset of (TOP-REAL 2); ::_thesis: (SpStSeq S) /. 2 = NE-corner S
 2 in dom <*(NW-corner S),(NE-corner S),(SE-corner S)*> by TOPREAL3:1;
hence (SpStSeq S) /. 2 = <*(NW-corner S),(NE-corner S),(SE-corner S)*> /. 2 by FINSEQ_4:68
.= NE-corner S by FINSEQ_4:18 ;
::_thesis: verum
end;

theorem Th37: :: SPRECT_1:37
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 3 = SE-corner S
proof
let S be Subset of (TOP-REAL 2); ::_thesis: (SpStSeq S) /. 3 = SE-corner S
 3 in dom <*(NW-corner S),(NE-corner S),(SE-corner S)*> by TOPREAL3:1;
hence (SpStSeq S) /. 3 = <*(NW-corner S),(NE-corner S),(SE-corner S)*> /. 3 by FINSEQ_4:68
.= SE-corner S by FINSEQ_4:18 ;
::_thesis: verum
end;

theorem Th38: :: SPRECT_1:38
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 4 = SW-corner S
proof
let S be Subset of (TOP-REAL 2); ::_thesis: (SpStSeq S) /. 4 = SW-corner S
set g = <*(NW-corner S),(NE-corner S),(SE-corner S)*>;
 1 in {1,2} by TARSKI:def_2;
then A1: 1 in dom <*(SW-corner S),(NW-corner S)*> by FINSEQ_1:2, FINSEQ_1:89;
 len <*(NW-corner S),(NE-corner S),(SE-corner S)*> = 3 by FINSEQ_1:45;
hence (SpStSeq S) /. 4 = (SpStSeq S) /. ((len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) + 1)
.= <*(SW-corner S),(NW-corner S)*> /. 1 by A1, FINSEQ_4:69
.= SW-corner S by FINSEQ_4:17 ;
::_thesis: verum
end;

theorem :: SPRECT_1:39
for S being Subset of (TOP-REAL 2) holds (SpStSeq S) /. 5 = NW-corner S
proof
let S be Subset of (TOP-REAL 2); ::_thesis: (SpStSeq S) /. 5 = NW-corner S
set g = <*(NW-corner S),(NE-corner S),(SE-corner S)*>;
 2 in {1,2} by TARSKI:def_2;
then A1: 2 in dom <*(SW-corner S),(NW-corner S)*> by FINSEQ_1:2, FINSEQ_1:89;
 len <*(NW-corner S),(NE-corner S),(SE-corner S)*> = 3 by FINSEQ_1:45;
hence (SpStSeq S) /. 5 = (SpStSeq S) /. ((len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) + 2)
.= <*(SW-corner S),(NW-corner S)*> /. 2 by A1, FINSEQ_4:69
.= NW-corner S by FINSEQ_4:17 ;
::_thesis: verum
end;

theorem Th40: :: SPRECT_1:40
for S being Subset of (TOP-REAL 2) holds len (SpStSeq S) = 5
proof
let S be Subset of (TOP-REAL 2); ::_thesis: len (SpStSeq S) = 5
thus  len (SpStSeq S) = (len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) + (len <*(SW-corner S),(NW-corner S)*>) by FINSEQ_1:22
.= (len <*(SW-corner S),(NW-corner S)*>) + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= 5 ; ::_thesis: verum
end;

theorem Th41: :: SPRECT_1:41
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
let S be Subset of (TOP-REAL 2); ::_thesis: 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))))
 len <*(NW-corner S),(NE-corner S),(SE-corner S)*> = 3 by FINSEQ_1:45;
then A1: <*(NW-corner S),(NE-corner S),(SE-corner S)*> /. (len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) = SE-corner S by FINSEQ_4:18;
 <*(SW-corner S),(NW-corner S)*> /. 1 = SW-corner S by FINSEQ_4:17;
hence  L~ (SpStSeq S) = ((L~ <*(NW-corner S),(NE-corner S),(SE-corner S)*>) \/ (LSeg ((SE-corner S),(SW-corner S)))) \/ (L~ <*(SW-corner S),(NW-corner S)*>) by A1, SPPOL_2:23
.= ((L~ <*(NW-corner S),(NE-corner S),(SE-corner S)*>) \/ (LSeg ((SE-corner S),(SW-corner S)))) \/ (LSeg ((SW-corner S),(NW-corner S))) by SPPOL_2:21
.= (((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))) by Th8
.= ((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)))) by XBOOLE_1:4 ;
::_thesis: verum
end;

registration
let D be non empty compact non vertical Subset of (TOP-REAL 2);
cluster SpStSeq D ->  non constant ;
coherence
 not SpStSeq D is constant
proof
assume  SpStSeq D is constant ; ::_thesis: contradiction
then  <*(NW-corner D),(NE-corner D),(SE-corner D)*> is constant by Th1;
then  |[(W-bound D),(N-bound D)]| = |[(E-bound D),(N-bound D)]| by Th3;
then  W-bound D = E-bound D by SPPOL_2:1;
hence  contradiction by Th15; ::_thesis: verum
end;
end;

registration
let D be non empty compact non horizontal Subset of (TOP-REAL 2);
cluster SpStSeq D ->  non constant ;
coherence
 not SpStSeq D is constant
proof
assume  SpStSeq D is constant ; ::_thesis: contradiction
then  <*(SW-corner D),(NW-corner D)*> is constant by Th1;
then  |[(W-bound D),(N-bound D)]| = |[(W-bound D),(S-bound D)]| by Th2;
then  N-bound D = S-bound D by SPPOL_2:1;
hence  contradiction by Th16; ::_thesis: verum
end;
end;

registration
let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
cluster SpStSeq D ->  circular special unfolded 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
A1: <*(S-bound D),(N-bound D)*> is increasing
proof
let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in K105(<*(S-bound D),(N-bound D)*>) or not m in K105(<*(S-bound D),(N-bound D)*>) or m <= n or not K513(<*(S-bound D),(N-bound D)*>,m) <= K513(<*(S-bound D),(N-bound D)*>,n) )
assume that
A2: n in dom <*(S-bound D),(N-bound D)*> and
A3: m in dom <*(S-bound D),(N-bound D)*> ; ::_thesis: ( m <= n or not K513(<*(S-bound D),(N-bound D)*>,m) <= K513(<*(S-bound D),(N-bound D)*>,n) )
 len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:44;
then A4: dom <*(S-bound D),(N-bound D)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
then A5: ( n = 1 or n = 2 ) by A2, TARSKI:def_2;
assume A6: n < m ; ::_thesis: not K513(<*(S-bound D),(N-bound D)*>,m) <= K513(<*(S-bound D),(N-bound D)*>,n)
A7: ( m = 1 or m = 2 ) by A4, A3, TARSKI:def_2;
then A8: <*(S-bound D),(N-bound D)*> . m = N-bound D by A5, A6, FINSEQ_1:44;
 <*(S-bound D),(N-bound D)*> . n = S-bound D by A5, A7, A6, FINSEQ_1:44;
hence  <*(S-bound D),(N-bound D)*> . n < <*(S-bound D),(N-bound D)*> . m by A8, Th32; ::_thesis: verum
end;
set S = (|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|);
set Yf1 = <*(N-bound D),(N-bound D),(S-bound D)*>;
set Yf2 = <*(S-bound D),(N-bound D)*>;
set Xf1 = <*(W-bound D),(E-bound D),(E-bound D)*>;
set Xf2 = <*(W-bound D),(W-bound D)*>;
set f = SpStSeq D;
set f1 = <*(NW-corner D),(NE-corner D),(SE-corner D)*>;
set f2 = <*(SW-corner D),(NW-corner D)*>;
reconsider Xf = <*(W-bound D),(E-bound D),(E-bound D)*> ^ <*(W-bound D),(W-bound D)*> as FinSequence of REAL ;
A9: rng <*(W-bound D),(W-bound D)*> = {(W-bound D),(W-bound D)} by FINSEQ_2:127
.= {(W-bound D)} by ENUMSET1:29 ;
rng <*(W-bound D),(E-bound D),(E-bound D)*> = {(W-bound D),(E-bound D),(E-bound D)} by FINSEQ_2:128
.= {(E-bound D),(E-bound D),(W-bound D)} by ENUMSET1:60
.= {(W-bound D),(E-bound D)} by ENUMSET1:30 ;
then A10: rng Xf = {(W-bound D),(E-bound D)} \/ {(W-bound D)} by A9, FINSEQ_1:31
.= {(W-bound D),(W-bound D),(E-bound D)} by ENUMSET1:2
.= {(W-bound D),(E-bound D)} by ENUMSET1:30 ;
then A11: rng <*(W-bound D),(E-bound D)*> = rng Xf by FINSEQ_2:127;
A12: <*(W-bound D),(E-bound D)*> is increasing
proof
let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in K105(<*(W-bound D),(E-bound D)*>) or not m in K105(<*(W-bound D),(E-bound D)*>) or m <= n or not K513(<*(W-bound D),(E-bound D)*>,m) <= K513(<*(W-bound D),(E-bound D)*>,n) )
assume that
A13: n in dom <*(W-bound D),(E-bound D)*> and
A14: m in dom <*(W-bound D),(E-bound D)*> ; ::_thesis: ( m <= n or not K513(<*(W-bound D),(E-bound D)*>,m) <= K513(<*(W-bound D),(E-bound D)*>,n) )
 len <*(W-bound D),(E-bound D)*> = 2 by FINSEQ_1:44;
then A15: dom <*(W-bound D),(E-bound D)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
then A16: ( n = 1 or n = 2 ) by A13, TARSKI:def_2;
assume A17: n < m ; ::_thesis: not K513(<*(W-bound D),(E-bound D)*>,m) <= K513(<*(W-bound D),(E-bound D)*>,n)
A18: ( m = 1 or m = 2 ) by A15, A14, TARSKI:def_2;
then A19: <*(W-bound D),(E-bound D)*> . m = E-bound D by A16, A17, FINSEQ_1:44;
 <*(W-bound D),(E-bound D)*> . n = W-bound D by A16, A18, A17, FINSEQ_1:44;
hence  <*(W-bound D),(E-bound D)*> . n < <*(W-bound D),(E-bound D)*> . m by A19, Th31; ::_thesis: verum
end;
A20: S-bound D < N-bound D by Th32;
reconsider Yf = <*(N-bound D),(N-bound D),(S-bound D)*> ^ <*(S-bound D),(N-bound D)*> as FinSequence of REAL ;
A21: rng <*(S-bound D),(N-bound D)*> = {(S-bound D),(N-bound D)} by FINSEQ_2:127;
rng <*(N-bound D),(N-bound D),(S-bound D)*> = {(N-bound D),(N-bound D),(S-bound D)} by FINSEQ_2:128
.= {(S-bound D),(N-bound D)} by ENUMSET1:30 ;
then A22: rng Yf = {(S-bound D),(N-bound D)} \/ {(S-bound D),(N-bound D)} by A21, FINSEQ_1:31
.= {(S-bound D),(N-bound D)} ;
then A23: rng <*(S-bound D),(N-bound D)*> = rng Yf by FINSEQ_2:127;
A24: len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:44
.= card (rng Yf) by A20, A22, CARD_2:57 ;
A25: len <*(N-bound D),(N-bound D),(S-bound D)*> = 3 by FINSEQ_1:45;
then  1 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by FINSEQ_3:25;
then A26: Yf . 1 = <*(N-bound D),(N-bound D),(S-bound D)*> . 1 by FINSEQ_1:def_7
.= N-bound D by FINSEQ_1:45 ;
A27: len <*(S-bound D),(N-bound D)*> = 2 by FINSEQ_1:44;
then A28: len Yf = 3 + 2 by A25, FINSEQ_1:22;
 2 in dom <*(S-bound D),(N-bound D)*> by A27, FINSEQ_3:25;
then A29: Yf . (3 + 2) = <*(S-bound D),(N-bound D)*> . 2 by A25, FINSEQ_1:def_7
.= N-bound D by FINSEQ_1:44 ;
 3 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by A25, FINSEQ_3:25;
then A30: Yf . 3 = <*(N-bound D),(N-bound D),(S-bound D)*> . 3 by FINSEQ_1:def_7
.= S-bound D by FINSEQ_1:45 ;
 2 in dom <*(N-bound D),(N-bound D),(S-bound D)*> by A25, FINSEQ_3:25;
then A31: Yf . 2 = <*(N-bound D),(N-bound D),(S-bound D)*> . 2 by FINSEQ_1:def_7
.= N-bound D by FINSEQ_1:45 ;
A32: len <*(NW-corner D),(NE-corner D),(SE-corner D)*> = 3 by FINSEQ_1:45;
then  1 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by FINSEQ_3:25;
then A33: (SpStSeq D) /. 1 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 1 by FINSEQ_4:68
.= NW-corner D by FINSEQ_4:18 ;
 3 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by A32, FINSEQ_3:25;
then A34: (SpStSeq D) /. 3 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 3 by FINSEQ_4:68
.= SE-corner D by FINSEQ_4:18 ;
 2 in dom <*(NW-corner D),(NE-corner D),(SE-corner D)*> by A32, FINSEQ_3:25;
then A35: (SpStSeq D) /. 2 = <*(NW-corner D),(NE-corner D),(SE-corner D)*> /. 2 by FINSEQ_4:68
.= NE-corner D by FINSEQ_4:18 ;
A36: len <*(SW-corner D),(NW-corner D)*> = 2 by FINSEQ_1:44;
then A37: len (<*(NW-corner D),(NE-corner D),(SE-corner D)*> ^ <*(SW-corner D),(NW-corner D)*>) = 3 + 2 by A32, FINSEQ_1:22;
 1 in dom <*(SW-corner D),(NW-corner D)*> by A36, FINSEQ_3:25;
then A38: (SpStSeq D) /. (3 + 1) = <*(SW-corner D),(NW-corner D)*> /. 1 by A32, FINSEQ_4:69
.= SW-corner D by FINSEQ_4:17 ;
then A39: LSeg ((SpStSeq D),3) = LSeg ((SE-corner D),(SW-corner D)) by A37, A34, TOPREAL1:def_3;
 2 in dom <*(SW-corner D),(NW-corner D)*> by A36, FINSEQ_3:25;
then A40: (SpStSeq D) /. (3 + 2) = <*(SW-corner D),(NW-corner D)*> /. 2 by A32, FINSEQ_4:69
.= NW-corner D by FINSEQ_4:17 ;
thus  SpStSeq D is special ::_thesis: ( SpStSeq D is unfolded & SpStSeq D is circular & SpStSeq D is s.c.c. & SpStSeq D is standard )
proof
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (SpStSeq D) or ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
assume  1 <= i ; ::_thesis: ( not i + 1 <= len (SpStSeq D) or ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
then  1 + 1 <= i + 1 by XREAL_1:6;
then A41: 1 < i + 1 by XXREAL_0:2;
assume  i + 1 <= len (SpStSeq D) ; ::_thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
then A42: ( i + 1 = 1 + 1 or i + 1 = 2 + 1 or i + 1 = 3 + 1 or i + 1 = 4 + 1 ) by A37, A41, NAT_1:29;
percases ( i = 1 or i = 2 or i = 3 or i = 4 ) by A42;
supposeA43: i = 1 ; ::_thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
((SpStSeq D) /. 1) `2 = N-bound D by A33, EUCLID:52
.= ((SpStSeq D) /. (1 + 1)) `2 by A35, EUCLID:52 ;
hence  ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A43; ::_thesis: verum
end;
supposeA44: i = 2 ; ::_thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
((SpStSeq D) /. 2) `1 = E-bound D by A35, EUCLID:52
.= ((SpStSeq D) /. (2 + 1)) `1 by A34, EUCLID:52 ;
hence  ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A44; ::_thesis: verum
end;
supposeA45: i = 3 ; ::_thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
((SpStSeq D) /. 3) `2 = S-bound D by A34, EUCLID:52
.= ((SpStSeq D) /. (3 + 1)) `2 by A38, EUCLID:52 ;
hence  ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A45; ::_thesis: verum
end;
supposeA46: i = 4 ; ::_thesis: ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 )
((SpStSeq D) /. 4) `1 = W-bound D by A38, EUCLID:52
.= ((SpStSeq D) /. (4 + 1)) `1 by A40, EUCLID:52 ;
hence  ( ((SpStSeq D) /. i) `1 = ((SpStSeq D) /. (i + 1)) `1 or ((SpStSeq D) /. i) `2 = ((SpStSeq D) /. (i + 1)) `2 ) by A46; ::_thesis: verum
end;
end;
end;
 4 + 1 = 5 ;
then A47: LSeg ((SpStSeq D),4) = LSeg ((SW-corner D),(NW-corner D)) by A37, A38, A40, TOPREAL1:def_3;
 2 + 1 = 3 ;
then A48: LSeg ((SpStSeq D),2) = LSeg ((NE-corner D),(SE-corner D)) by A37, A35, A34, TOPREAL1:def_3;
 1 in dom <*(S-bound D),(N-bound D)*> by A27, FINSEQ_3:25;
then A49: Yf . (3 + 1) = <*(S-bound D),(N-bound D)*> . 1 by A25, FINSEQ_1:def_7
.= S-bound D by FINSEQ_1:44 ;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_Yf_holds_
Yf_._n_=_((SpStSeq_D)_/._n)_`2
let n be Element of NAT ; ::_thesis: ( n in dom Yf implies Yf . b1 = ((SpStSeq D) /. b1) `2 )
assume A50: n in dom Yf ; ::_thesis: Yf . b1 = ((SpStSeq D) /. b1) `2
then A51: n <> 0 by FINSEQ_3:25;
A52: n <= 5 by A28, A50, FINSEQ_3:25;
percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A51, A52, NAT_1:29;
suppose n = 1 ; ::_thesis: Yf . b1 = ((SpStSeq D) /. b1) `2
hence  Yf . n = ((SpStSeq D) /. n) `2 by A33, A26, EUCLID:52; ::_thesis: verum
end;
suppose n = 2 ; ::_thesis: Yf . b1 = ((SpStSeq D) /. b1) `2
hence  Yf . n = ((SpStSeq D) /. n) `2 by A35, A31, EUCLID:52; ::_thesis: verum
end;
suppose n = 3 ; ::_thesis: Yf . b1 = ((SpStSeq D) /. b1) `2
hence  Yf . n = ((SpStSeq D) /. n) `2 by A34, A30, EUCLID:52; ::_thesis: verum
end;
suppose n = 4 ; ::_thesis: Yf . b1 = ((SpStSeq D) /. b1) `2
hence  Yf . n = ((SpStSeq D) /. n) `2 by A38, A49, EUCLID:52; ::_thesis: verum
end;
suppose n = 5 ; ::_thesis: Yf . b1 = ((SpStSeq D) /. b1) `2
hence  Yf . n = ((SpStSeq D) /. n) `2 by A40, A29, EUCLID:52; ::_thesis: verum
end;
end;
end;
then  Yf = Y_axis (SpStSeq D) by A37, A28, GOBOARD1:def_2;
then A53: <*(S-bound D),(N-bound D)*> = Incr (Y_axis (SpStSeq D)) by A23, A24, A1, SEQ_4:def_21;
 1 + 1 = 2 ;
then A54: LSeg ((SpStSeq D),1) = LSeg ((NW-corner D),(NE-corner D)) by A37, A33, A35, TOPREAL1:def_3;
thus  SpStSeq D is unfolded ::_thesis: ( SpStSeq D is circular & SpStSeq D is s.c.c. & SpStSeq D is standard )
proof
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (SpStSeq D) or (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} )
assume  1 <= i ; ::_thesis: ( not i + 2 <= len (SpStSeq D) or (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} )
then A55: 1 + 2 <= i + 2 by XREAL_1:6;
then A56: 1 < i + 2 by XXREAL_0:2;
assume A57: i + 2 <= len (SpStSeq D) ; ::_thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}
 2 < i + 2 by A55, XXREAL_0:2;
then A58: ( i + 2 = 1 + 2 or i + 2 = 2 + 2 or i + 2 = 3 + 2 ) by A37, A56, A57, NAT_1:29;
percases ( i = 1 or i = 2 or i = 3 ) by A58;
suppose i = 1 ; ::_thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}
hence  (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} by A35, A54, A48, Th28; ::_thesis: verum
end;
suppose i = 2 ; ::_thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}
hence  (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} by A34, A48, A39, Th29; ::_thesis: verum
end;
suppose i = 3 ; ::_thesis: (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))}
hence  (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),(i + 1))) = {((SpStSeq D) /. (i + 1))} by A38, A39, A47, Th30; ::_thesis: verum
end;
end;
end;
thus  SpStSeq D is circular by A37, A33, A40, FINSEQ_6:def_1; ::_thesis: ( SpStSeq D is s.c.c. & SpStSeq D is standard )
thus  SpStSeq D is s.c.c. ::_thesis: SpStSeq D is standard
proof
let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for b1 being Element of NAT holds
( b1 <= i + 1 or ( ( i <= 1 or len (SpStSeq D) <= b1 ) & len (SpStSeq D) <= b1 + 1 ) or LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),b1) )
let j be Element of NAT ; ::_thesis: ( j <= i + 1 or ( ( i <= 1 or len (SpStSeq D) <= j ) & len (SpStSeq D) <= j + 1 ) or LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j) )
assume that
A59: i + 1 < j and
A60: ( ( i > 1 & j < len (SpStSeq D) ) or j + 1 < len (SpStSeq D) ) ; ::_thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)
A61: ( j + 1 = 0 + 1 or j + 1 = 1 + 1 or j + 1 = 2 + 1 or j + 1 = 3 + 1 or j + 1 = 4 + 1 ) by A37, A60, NAT_1:29;
A62: ( i + 2 = 2 + 2 implies i = 2 ) ;
A63: ( i + 2 = 1 + 2 implies i = 1 ) ;
A64: (i + 1) + 1 = i + (1 + 1) ;
then A65: i + 2 <> 0 + 1 ;
A66: ( i + 2 = 0 + 2 implies i = 0 ) ;
A67: i + 2 <= j by A59, A64, NAT_1:13;
A68: now__::_thesis:_(_(_j_=_2_&_i_=_0_)_or_(_j_=_3_&_(_i_=_0_or_i_=_1_)_)_or_(_j_=_4_&_(_i_=_0_or_i_=_2_)_)_)
percases ( j = 2 or j = 3 or j = 4 ) by A59, A61, NAT_1:11;
case j = 2 ; ::_thesis: i = 0
hence  i = 0 by A59, A64, A66, NAT_1:26; ::_thesis: verum
end;
case j = 3 ; ::_thesis: ( i = 0 or i = 1 )
hence  ( i = 0 or i = 1 ) by A59, A64, A63, A66, NAT_1:27; ::_thesis: verum
end;
case j = 4 ; ::_thesis: ( i = 0 or i = 2 )
hence  ( i = 0 or i = 2 ) by A37, A60, A67, A62, A63, A66, A65, NAT_1:28; ::_thesis: verum
end;
end;
end;
percases ( i = 0 or ( i = 1 & j = 3 ) or ( i = 2 & j = 4 ) ) by A68;
suppose i = 0 ; ::_thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)
then  LSeg ((SpStSeq D),i) = {} by TOPREAL1:def_3;
hence  (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
suppose ( i = 1 & j = 3 ) ; ::_thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)
then  LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j) by A54, A39, Th34;
hence  (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),j)) = {} by XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
suppose ( i = 2 & j = 4 ) ; ::_thesis: LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j)
then  LSeg ((SpStSeq D),i) misses LSeg ((SpStSeq D),j) by A48, A47, Th33;
hence  (LSeg ((SpStSeq D),i)) /\ (LSeg ((SpStSeq D),j)) = {} by XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
end;
end;
A69: W-bound D < E-bound D by Th31;
A70: len <*(W-bound D),(E-bound D)*> = 2 by FINSEQ_1:44
.= card (rng Xf) by A69, A10, CARD_2:57 ;
A71: len <*(W-bound D),(E-bound D),(E-bound D)*> = 3 by FINSEQ_1:45;
then  1 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by FINSEQ_3:25;
then A72: Xf . 1 = <*(W-bound D),(E-bound D),(E-bound D)*> . 1 by FINSEQ_1:def_7
.= W-bound D by FINSEQ_1:45 ;
A73: len <*(W-bound D),(W-bound D)*> = 2 by FINSEQ_1:44;
then A74: len Xf = 3 + 2 by A71, FINSEQ_1:22;
 2 in dom <*(W-bound D),(W-bound D)*> by A73, FINSEQ_3:25;
then A75: Xf . (3 + 2) = <*(W-bound D),(W-bound D)*> . 2 by A71, FINSEQ_1:def_7
.= W-bound D by FINSEQ_1:44 ;
 3 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by A71, FINSEQ_3:25;
then A76: Xf . 3 = <*(W-bound D),(E-bound D),(E-bound D)*> . 3 by FINSEQ_1:def_7
.= E-bound D by FINSEQ_1:45 ;
 2 in dom <*(W-bound D),(E-bound D),(E-bound D)*> by A71, FINSEQ_3:25;
then A77: Xf . 2 = <*(W-bound D),(E-bound D),(E-bound D)*> . 2 by FINSEQ_1:def_7
.= E-bound D by FINSEQ_1:45 ;
 1 in dom <*(W-bound D),(W-bound D)*> by A73, FINSEQ_3:25;
then A78: Xf . (3 + 1) = <*(W-bound D),(W-bound D)*> . 1 by A71, FINSEQ_1:def_7
.= W-bound D by FINSEQ_1:44 ;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_Xf_holds_
Xf_._n_=_((SpStSeq_D)_/._n)_`1
let n be Element of NAT ; ::_thesis: ( n in dom Xf implies Xf . b1 = ((SpStSeq D) /. b1) `1 )
assume A79: n in dom Xf ; ::_thesis: Xf . b1 = ((SpStSeq D) /. b1) `1
then A80: n <> 0 by FINSEQ_3:25;
A81: n <= 5 by A74, A79, FINSEQ_3:25;
percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A80, A81, NAT_1:29;
suppose n = 1 ; ::_thesis: Xf . b1 = ((SpStSeq D) /. b1) `1
hence  Xf . n = ((SpStSeq D) /. n) `1 by A33, A72, EUCLID:52; ::_thesis: verum
end;
suppose n = 2 ; ::_thesis: Xf . b1 = ((SpStSeq D) /. b1) `1
hence  Xf . n = ((SpStSeq D) /. n) `1 by A35, A77, EUCLID:52; ::_thesis: verum
end;
suppose n = 3 ; ::_thesis: Xf . b1 = ((SpStSeq D) /. b1) `1
hence  Xf . n = ((SpStSeq D) /. n) `1 by A34, A76, EUCLID:52; ::_thesis: verum
end;
suppose n = 4 ; ::_thesis: Xf . b1 = ((SpStSeq D) /. b1) `1
hence  Xf . n = ((SpStSeq D) /. n) `1 by A38, A78, EUCLID:52; ::_thesis: verum
end;
suppose n = 5 ; ::_thesis: Xf . b1 = ((SpStSeq D) /. b1) `1
hence  Xf . n = ((SpStSeq D) /. n) `1 by A40, A75, EUCLID:52; ::_thesis: verum
end;
end;
end;
then  Xf = X_axis (SpStSeq D) by A37, A74, GOBOARD1:def_1;
then A82: <*(W-bound D),(E-bound D)*> = Incr (X_axis (SpStSeq D)) by A11, A70, A12, SEQ_4:def_21;
A83: for n, m being Element of NAT st [n,m] in Indices ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) holds
((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|
proof
let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) implies ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| )
A84: <*(S-bound D),(N-bound D)*> . 1 = S-bound D by FINSEQ_1:44;
assume  [n,m] in Indices ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) ; ::_thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|
then  [n,m] in [:{1,2},{1,2}:] by FINSEQ_1:2, MATRIX_2:3;
then A85: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
A86: <*(S-bound D),(N-bound D)*> . 2 = N-bound D by FINSEQ_1:44;
percases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A85, ENUMSET1:def_2;
supposeA87: [n,m] = [1,1] ; ::_thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|
then A88: m = 1 by XTUPLE_0:1;
A89: n = 1 by A87, XTUPLE_0:1;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(W-bound D),(S-bound D)]| by A88, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A84, A89, A88, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA90: [n,m] = [1,2] ; ::_thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|
then A91: m = 2 by XTUPLE_0:1;
A92: n = 1 by A90, XTUPLE_0:1;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(W-bound D),(N-bound D)]| by A91, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A86, A92, A91, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA93: [n,m] = [2,1] ; ::_thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|
then A94: m = 1 by XTUPLE_0:1;
A95: n = 2 by A93, XTUPLE_0:1;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(E-bound D),(S-bound D)]| by A94, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A84, A95, A94, FINSEQ_1:44 ;
::_thesis: verum
end;
supposeA96: [n,m] = [2,2] ; ::_thesis: ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]|
then A97: m = 2 by XTUPLE_0:1;
A98: n = 2 by A96, XTUPLE_0:1;
hence ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) * (n,m) = |[(E-bound D),(N-bound D)]| by A97, MATRIX_2:6
.= |[((Incr (X_axis (SpStSeq D))) . n),((Incr (Y_axis (SpStSeq D))) . m)]| by A82, A53, A86, A98, A97, FINSEQ_1:44 ;
::_thesis: verum
end;
end;
end;
A99: width ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) = 2 by MATRIX_2:3
.= len (Incr (Y_axis (SpStSeq D))) by A53, FINSEQ_1:44 ;
len ((|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|)) = 2 by MATRIX_2:3
.= len (Incr (X_axis (SpStSeq D))) by A82, FINSEQ_1:44 ;
then A100: (|[(W-bound D),(S-bound D)]|,|[(W-bound D),(N-bound D)]|) ][ (|[(E-bound D),(S-bound D)]|,|[(E-bound D),(N-bound D)]|) = GoB ((Incr (X_axis (SpStSeq D))),(Incr (Y_axis (SpStSeq D)))) by A99, A83, GOBOARD2:def_1
.= GoB (SpStSeq D) by GOBOARD2:def_2 ;
then A101: (SpStSeq D) /. 2 = (GoB (SpStSeq D)) * (2,2) by A35, MATRIX_2:6;
A102: (SpStSeq D) /. 4 = (GoB (SpStSeq D)) * (1,1) by A38, A100, MATRIX_2:6;
A103: (SpStSeq D) /. 3 = (GoB (SpStSeq D)) * (2,1) by A34, A100, MATRIX_2:6;
A104: (SpStSeq D) /. 1 = (GoB (SpStSeq D)) * (1,2) by A33, A100, MATRIX_2:6;
thus  SpStSeq D is standard ::_thesis: verum
proof
thus  for k being Element of NAT st k in dom (SpStSeq D) holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) ) :: according to GOBOARD1:def_9,GOBOARD5:def_5 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom (SpStSeq D) or not b1 + 1 in dom (SpStSeq D) or for b2, b3, b4, b5 being Element of NAT holds
( not [b2,b3] in Indices (GoB (SpStSeq D)) or not [b4,b5] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. b1 = (GoB (SpStSeq D)) * (b2,b3) or not (SpStSeq D) /. (b1 + 1) = (GoB (SpStSeq D)) * (b4,b5) or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) )
proof
let k be Element of NAT ; ::_thesis: ( k in dom (SpStSeq D) implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) ) )
assume A105: k in dom (SpStSeq D) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )
then A106: k >= 1 by FINSEQ_3:25;
A107: k <= 5 by A37, A105, FINSEQ_3:25;
percases ( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 ) by A106, A107, NAT_1:29;
supposeA108: k = 1 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )
take  1 ; ::_thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,j) )
take  2 ; ::_thesis: ( [1,2] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) )
thus  [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; ::_thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2)
thus  (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) by A33, A100, A108, MATRIX_2:6; ::_thesis: verum
end;
supposeA109: k = 2 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )
take  2 ; ::_thesis: ex j being Element of NAT st
( [2,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,j) )
take  2 ; ::_thesis: ( [2,2] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,2) )
thus  [2,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; ::_thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,2)
thus  (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,2) by A35, A100, A109, MATRIX_2:6; ::_thesis: verum
end;
supposeA110: k = 3 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )
take  2 ; ::_thesis: ex j being Element of NAT st
( [2,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,j) )
take  1 ; ::_thesis: ( [2,1] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,1) )
thus  [2,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; ::_thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,1)
thus  (SpStSeq D) /. k = (GoB (SpStSeq D)) * (2,1) by A34, A100, A110, MATRIX_2:6; ::_thesis: verum
end;
supposeA111: k = 4 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )
take  1 ; ::_thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,j) )
take  1 ; ::_thesis: ( [1,1] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,1) )
thus  [1,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; ::_thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,1)
thus  (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,1) by A38, A100, A111, MATRIX_2:6; ::_thesis: verum
end;
supposeA112: k = 5 ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (i,j) )
take  1 ; ::_thesis: ex j being Element of NAT st
( [1,j] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,j) )
take  2 ; ::_thesis: ( [1,2] in Indices (GoB (SpStSeq D)) & (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) )
thus  [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4; ::_thesis: (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2)
thus  (SpStSeq D) /. k = (GoB (SpStSeq D)) * (1,2) by A40, A100, A112, MATRIX_2:6; ::_thesis: verum
end;
end;
end;
let n be Element of NAT ; ::_thesis: ( not n in dom (SpStSeq D) or not n + 1 in dom (SpStSeq D) or for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB (SpStSeq D)) or not [b3,b4] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. n = (GoB (SpStSeq D)) * (b1,b2) or not (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) )
assume that
A113: n in dom (SpStSeq D) and
A114: n + 1 in dom (SpStSeq D) ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB (SpStSeq D)) or not [b3,b4] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. n = (GoB (SpStSeq D)) * (b1,b2) or not (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 )
A115: n <> 0 by A113, FINSEQ_3:25;
 n + 1 <= 4 + 1 by A37, A114, FINSEQ_3:25;
then A116: n <= 4 by XREAL_1:6;
let m, k, i, j be Element of NAT ; ::_thesis: ( not [m,k] in Indices (GoB (SpStSeq D)) or not [i,j] in Indices (GoB (SpStSeq D)) or not (SpStSeq D) /. n = (GoB (SpStSeq D)) * (m,k) or not (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (i,j) or (abs (m - i)) + (abs (k - j)) = 1 )
assume that
A117: [m,k] in Indices (GoB (SpStSeq D)) and
A118: [i,j] in Indices (GoB (SpStSeq D)) and
A119: (SpStSeq D) /. n = (GoB (SpStSeq D)) * (m,k) and
A120: (SpStSeq D) /. (n + 1) = (GoB (SpStSeq D)) * (i,j) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
percases ( n = 1 or n = 2 or n = 3 or n = 4 ) by A115, A116, NAT_1:28;
supposeA121: n = 1 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A122: [2,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A123: i = 1 + 1 by A101, A118, A120, A121, GOBOARD1:5;
A124: [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then  m = 1 by A104, A117, A119, A121, GOBOARD1:5;
then A125: abs (m - i) = 1 by A123, SEQM_3:41;
A126: j = 2 by A101, A118, A120, A121, A122, GOBOARD1:5;
 k = 2 by A104, A117, A119, A121, A124, GOBOARD1:5;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A126, A125, SEQM_3:42; ::_thesis: verum
end;
supposeA127: n = 2 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A128: [2,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A129: j = 1 by A103, A118, A120, A127, GOBOARD1:5;
A130: [2,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then  k = 1 + 1 by A101, A117, A119, A127, GOBOARD1:5;
then A131: abs (k - j) = 1 by A129, SEQM_3:41;
A132: i = 2 by A103, A118, A120, A127, A128, GOBOARD1:5;
 m = 2 by A101, A117, A119, A127, A130, GOBOARD1:5;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A132, A131, SEQM_3:42; ::_thesis: verum
end;
supposeA133: n = 3 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A134: [1,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A135: i = 1 by A102, A118, A120, A133, GOBOARD1:5;
A136: [2,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then  m = 1 + 1 by A103, A117, A119, A133, GOBOARD1:5;
then A137: abs (m - i) = 1 by A135, SEQM_3:41;
A138: j = 1 by A102, A118, A120, A133, A134, GOBOARD1:5;
 k = 1 by A103, A117, A119, A133, A136, GOBOARD1:5;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A138, A137, SEQM_3:42; ::_thesis: verum
end;
supposeA139: n = 4 ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A140: [1,1] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then A141: k = 1 by A102, A117, A119, A139, GOBOARD1:5;
A142: [1,2] in Indices (GoB (SpStSeq D)) by A100, MATRIX_2:4;
then  j = 1 + 1 by A33, A40, A104, A118, A120, A139, GOBOARD1:5;
then A143: abs (k - j) = 1 by A141, SEQM_3:41;
A144: m = 1 by A102, A117, A119, A139, A140, GOBOARD1:5;
 i = 1 by A33, A40, A104, A118, A120, A139, A142, GOBOARD1:5;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A144, A143, SEQM_3:42; ::_thesis: verum
end;
end;
end;
end;
end;

theorem Th42: :: SPRECT_1:42
for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds L~ (SpStSeq D) = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).]
proof
let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: L~ (SpStSeq D) = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).]
L~ (SpStSeq D) = ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ ((LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D)))) by Th41
.= ((LSeg ((SW-corner D),(NW-corner D))) \/ ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))))) \/ (LSeg ((SE-corner D),(SW-corner D))) by XBOOLE_1:4
.= (((LSeg ((SW-corner D),(NW-corner D))) \/ (LSeg ((NW-corner D),(NE-corner D)))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ (LSeg ((SE-corner D),(SW-corner D))) by XBOOLE_1:4
.= ((LSeg ((SW-corner D),(NW-corner D))) \/ (LSeg ((NW-corner D),(NE-corner D)))) \/ ((LSeg ((NE-corner D),(SE-corner D))) \/ (LSeg ((SE-corner D),(SW-corner D)))) by XBOOLE_1:4 ;
hence  L~ (SpStSeq D) = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).] by SPPOL_2:def_3; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let X be non empty compact Subset of T;
let f be continuous RealMap of T;
clusterf .: X ->  bounded_below ;
coherence
 f .: X is bounded_below
proof
A1: (f | X) .: the carrier of (T | X) is bounded_below by MEASURE6:def_10;
 (f | X) .: X = f .: X by RELAT_1:129;
hence  f .: X is bounded_below by A1, PRE_TOPC:8; ::_thesis: verum
end;
clusterf .: X ->  bounded_above ;
coherence
 f .: X is bounded_above
proof
A2: (f | X) .: the carrier of (T | X) is bounded_above by MEASURE6:def_11;
 (f | X) .: X = f .: X by RELAT_1:129;
hence  f .: X is bounded_above by A2, PRE_TOPC:8; ::_thesis: verum
end;
end;

theorem Th43: :: SPRECT_1:43
for S being Subset of (TOP-REAL 2) holds W-bound S = lower_bound (proj1 .: S)
proof
let S be Subset of (TOP-REAL 2); ::_thesis: W-bound S = lower_bound (proj1 .: S)
thus  W-bound S = lower_bound (rng (proj1 | S)) by RELSET_1:22
.= lower_bound (proj1 .: S) by RELAT_1:115 ; ::_thesis: verum
end;

theorem Th44: :: SPRECT_1:44
for S being Subset of (TOP-REAL 2) holds S-bound S = lower_bound (proj2 .: S)
proof
let S be Subset of (TOP-REAL 2); ::_thesis: S-bound S = lower_bound (proj2 .: S)
thus  S-bound S = lower_bound (rng (proj2 | S)) by RELSET_1:22
.= lower_bound (proj2 .: S) by RELAT_1:115 ; ::_thesis: verum
end;

theorem Th45: :: SPRECT_1:45
for S being Subset of (TOP-REAL 2) holds N-bound S = upper_bound (proj2 .: S)
proof
let S be Subset of (TOP-REAL 2); ::_thesis: N-bound S = upper_bound (proj2 .: S)
thus  N-bound S = upper_bound (rng (proj2 | S)) by RELSET_1:22
.= upper_bound (proj2 .: S) by RELAT_1:115 ; ::_thesis: verum
end;

theorem Th46: :: SPRECT_1:46
for S being Subset of (TOP-REAL 2) holds E-bound S = upper_bound (proj1 .: S)
proof
let S be Subset of (TOP-REAL 2); ::_thesis: E-bound S = upper_bound (proj1 .: S)
thus  E-bound S = upper_bound (rng (proj1 | S)) by RELSET_1:22
.= upper_bound (proj1 .: S) by RELAT_1:115 ; ::_thesis: verum
end;

theorem Th47: :: SPRECT_1:47
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
let S be Subset of (TOP-REAL 2); ::_thesis: 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))
let C1, C2 be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( S = C1 \/ C2 implies W-bound S = min ((W-bound C1),(W-bound C2)) )
assume A1: S = C1 \/ C2 ; ::_thesis: W-bound S = min ((W-bound C1),(W-bound C2))
A2: W-bound C1 = lower_bound (proj1 .: C1) by Th43;
A3: W-bound C2 = lower_bound (proj1 .: C2) by Th43;
thus  W-bound S = lower_bound (proj1 .: S) by Th43
.= lower_bound ((proj1 .: C1) \/ (proj1 .: C2)) by A1, RELAT_1:120
.= min ((W-bound C1),(W-bound C2)) by A2, A3, SEQ_4:142 ; ::_thesis: verum
end;

theorem Th48: :: SPRECT_1:48
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
let S be Subset of (TOP-REAL 2); ::_thesis: 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))
let C1, C2 be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( S = C1 \/ C2 implies S-bound S = min ((S-bound C1),(S-bound C2)) )
assume A1: S = C1 \/ C2 ; ::_thesis: S-bound S = min ((S-bound C1),(S-bound C2))
A2: S-bound C1 = lower_bound (proj2 .: C1) by Th44;
A3: S-bound C2 = lower_bound (proj2 .: C2) by Th44;
thus  S-bound S = lower_bound (proj2 .: S) by Th44
.= lower_bound ((proj2 .: C1) \/ (proj2 .: C2)) by A1, RELAT_1:120
.= min ((S-bound C1),(S-bound C2)) by A2, A3, SEQ_4:142 ; ::_thesis: verum
end;

theorem Th49: :: SPRECT_1:49
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
let S be Subset of (TOP-REAL 2); ::_thesis: 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))
let C1, C2 be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( S = C1 \/ C2 implies N-bound S = max ((N-bound C1),(N-bound C2)) )
assume A1: S = C1 \/ C2 ; ::_thesis: N-bound S = max ((N-bound C1),(N-bound C2))
A2: N-bound C1 = upper_bound (proj2 .: C1) by Th45;
A3: N-bound C2 = upper_bound (proj2 .: C2) by Th45;
thus  N-bound S = upper_bound (proj2 .: S) by Th45
.= upper_bound ((proj2 .: C1) \/ (proj2 .: C2)) by A1, RELAT_1:120
.= max ((N-bound C1),(N-bound C2)) by A2, A3, SEQ_4:143 ; ::_thesis: verum
end;

theorem Th50: :: SPRECT_1:50
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
let S be Subset of (TOP-REAL 2); ::_thesis: 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))
let C1, C2 be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( S = C1 \/ C2 implies E-bound S = max ((E-bound C1),(E-bound C2)) )
assume A1: S = C1 \/ C2 ; ::_thesis: E-bound S = max ((E-bound C1),(E-bound C2))
A2: E-bound C1 = upper_bound (proj1 .: C1) by Th46;
A3: E-bound C2 = upper_bound (proj1 .: C2) by Th46;
thus  E-bound S = upper_bound (proj1 .: S) by Th46
.= upper_bound ((proj1 .: C1) \/ (proj1 .: C2)) by A1, RELAT_1:120
.= max ((E-bound C1),(E-bound C2)) by A2, A3, SEQ_4:143 ; ::_thesis: verum
end;

registration
let r1, r2 be real number ;
clusterK76(r1,r2) ->  real-bounded for Subset of REAL;
coherence
 for b1 being Subset of REAL st b1 = [.r1,r2.] holds
b1 is real-bounded
proof
A1: [.r1,r2.] is bounded_above
proof
take  r2 ; :: according to XXREAL_2:def_10 ::_thesis: r2 is UpperBound of [.r1,r2.]
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not x in [.r1,r2.] or x <= r2 )
thus  ( not x in [.r1,r2.] or x <= r2 ) by XXREAL_1:1; ::_thesis: verum
end;
 [.r1,r2.] is bounded_below
proof
take  r1 ; :: according to XXREAL_2:def_9 ::_thesis: r1 is LowerBound of [.r1,r2.]
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not x in [.r1,r2.] or r1 <= x )
thus  ( not x in [.r1,r2.] or r1 <= x ) by XXREAL_1:1; ::_thesis: verum
end;
hence  for b1 being Subset of REAL st b1 = [.r1,r2.] holds
b1 is real-bounded by A1; ::_thesis: verum
end;
end;

theorem Th51: :: SPRECT_1:51
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
let r1, r2, t be Real; ::_thesis: ( r1 <= r2 implies ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) ) )
assume A1: r1 <= r2 ; ::_thesis: ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )
percases ( r1 = r2 or r1 < r2 ) by A1, XXREAL_0:1;
supposeA2: r1 = r2 ; ::_thesis: ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )
then A3: [.r1,r2.] = {r1} by XXREAL_1:17;
hereby  ::_thesis: ( ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) implies t in [.r1,r2.] )
reconsider a19 = 1 as Real ;
assume A4: t in [.r1,r2.] ; ::_thesis: ex s being Real st
( 0 <= s & s <= 1 & t = (s * r1) + ((1 - s) * r2) )
take s = a19; ::_thesis: ( 0 <= s & s <= 1 & t = (s * r1) + ((1 - s) * r2) )
thus  ( 0 <= s & s <= 1 ) ; ::_thesis: t = (s * r1) + ((1 - s) * r2)
thus  t = (s * r1) + ((1 - s) * r2) by A3, A4, TARSKI:def_1; ::_thesis: verum
end;
given s1 being Real such that  0 <= s1 and
 s1 <= 1 and
A5: t = (s1 * r1) + ((1 - s1) * r2) ; ::_thesis: t in [.r1,r2.]
thus  t in [.r1,r2.] by A2, A3, A5, TARSKI:def_1; ::_thesis: verum
end;
supposeA6: r1 < r2 ; ::_thesis: ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )
hereby  ::_thesis: ( ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) implies t in [.r1,r2.] )
assume A7: t in [.r1,r2.] ; ::_thesis: ex s1 being Element of REAL st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) )
take s1 = (r2 - t) / (r2 - r1); ::_thesis: ( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) )
A8: r2 - r1 > 0 by A6, XREAL_1:50;
 t <= r2 by A7, XXREAL_1:1;
then  0 <= r2 - t by XREAL_1:48;
hence  0 <= s1 by A8; ::_thesis: ( s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) )
 r1 <= t by A7, XXREAL_1:1;
then  r2 - t <= r2 - r1 by XREAL_1:10;
hence  s1 <= 1 by A8, XREAL_1:185; ::_thesis: t = (s1 * r1) + ((1 - s1) * r2)
thus t = (t * (r2 - r1)) / (r2 - r1) by A8, XCMPLX_1:89
.= (((r2 - t) * r1) + ((t - r1) * r2)) / (r2 - r1)
.= (((r2 - t) * r1) / (r2 - r1)) + (((t - r1) * r2) / (r2 - r1)) by XCMPLX_1:62
.= (((r2 - t) * r1) / (r2 - r1)) + (((t - r1) / (r2 - r1)) * r2) by XCMPLX_1:74
.= (((r2 - t) / (r2 - r1)) * r1) + ((((1 * (r2 - r1)) - (r2 - t)) / (r2 - r1)) * r2) by XCMPLX_1:74
.= (s1 * r1) + ((1 - s1) * r2) by A8, XCMPLX_1:127 ; ::_thesis: verum
end;
given s1 being Real such that A9: 0 <= s1 and
A10: s1 <= 1 and
A11: t = (s1 * r1) + ((1 - s1) * r2) ; ::_thesis: t in [.r1,r2.]
A12: (s1 * r2) + ((1 - s1) * r2) = 1 * r2 ;
 1 - s1 >= 0 by A10, XREAL_1:48;
then A13: (1 - s1) * r1 <= (1 - s1) * r2 by A6, XREAL_1:64;
 s1 * r1 <= s1 * r2 by A6, A9, XREAL_1:64;
then A14: t <= r2 by A11, A12, XREAL_1:6;
 (s1 * r1) + ((1 - s1) * r1) = 1 * r1 ;
then  r1 <= t by A11, A13, XREAL_1:6;
hence  t in [.r1,r2.] by A14, XXREAL_1:1; ::_thesis: verum
end;
end;
end;

theorem Th52: :: SPRECT_1:52
for p, q being Point of (TOP-REAL 2) st p `1 <= q `1 holds
proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).]
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 <= q `1 implies proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).] )
assume A1: p `1 <= q `1 ; ::_thesis: proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).]
 for y being set holds
( y in [.(p `1),(q `1).] iff ex x being set st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x ) )
proof
let y be set ; ::_thesis: ( y in [.(p `1),(q `1).] iff ex x being set st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x ) )
hereby  ::_thesis: ( ex x being set st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x ) implies y in [.(p `1),(q `1).] )
assume A2: y in [.(p `1),(q `1).] ; ::_thesis: ex x being set st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x )
then reconsider r = y as Real ;
consider t being Real such that
A3: 0 <= t and
A4: t <= 1 and
A5: r = (t * (p `1)) + ((1 - t) * (q `1)) by A1, A2, Th51;
set o = (t * p) + ((1 - t) * q);
reconsider x = (t * p) + ((1 - t) * q) as set ;
take x = x; ::_thesis: ( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x )
 (t * p) + ((1 - t) * q) in the carrier of (TOP-REAL 2) ;
hence  x in dom proj1 by FUNCT_2:def_1; ::_thesis: ( x in LSeg (p,q) & y = proj1 . x )
 (t * p) + ((1 - t) * q) in LSeg (q,p) by A3, A4;
hence  x in LSeg (p,q) ; ::_thesis: y = proj1 . x
thus y = ((t * p) `1) + ((1 - t) * (q `1)) by A5, TOPREAL3:4
.= ((t * p) `1) + (((1 - t) * q) `1) by TOPREAL3:4
.= ((t * p) + ((1 - t) * q)) `1 by TOPREAL3:2
.= proj1 . x by PSCOMP_1:def_5 ; ::_thesis: verum
end;
given x being set  such that  x in dom proj1 and
A6: x in LSeg (p,q) and
A7: y = proj1 . x ; ::_thesis: y in [.(p `1),(q `1).]
reconsider s = x as Point of (TOP-REAL 2) by A6;
 x in LSeg (q,p) by A6;
then consider r being Real such that
A8: s = ((1 - r) * q) + (r * p) and
A9: 0 <= r and
A10: r <= 1 ;
y = s `1 by A7, PSCOMP_1:def_5
.= (((1 - r) * q) `1) + ((r * p) `1) by A8, TOPREAL3:2
.= ((1 - r) * (q `1)) + ((r * p) `1) by TOPREAL3:4
.= ((1 - r) * (q `1)) + (r * (p `1)) by TOPREAL3:4 ;
hence  y in [.(p `1),(q `1).] by A1, A9, A10, Th51; ::_thesis: verum
end;
hence  proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).] by FUNCT_1:def_6; ::_thesis: verum
end;

theorem Th53: :: SPRECT_1:53
for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds
proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).]
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `2 <= q `2 implies proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).] )
assume A1: p `2 <= q `2 ; ::_thesis: proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).]
 for y being set holds
( y in [.(p `2),(q `2).] iff ex x being set st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x ) )
proof
let y be set ; ::_thesis: ( y in [.(p `2),(q `2).] iff ex x being set st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x ) )
hereby  ::_thesis: ( ex x being set st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x ) implies y in [.(p `2),(q `2).] )
assume A2: y in [.(p `2),(q `2).] ; ::_thesis: ex x being set st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x )
then reconsider r = y as Real ;
consider t being Real such that
A3: 0 <= t and
A4: t <= 1 and
A5: r = (t * (p `2)) + ((1 - t) * (q `2)) by A1, A2, Th51;
set o = (t * p) + ((1 - t) * q);
reconsider x = (t * p) + ((1 - t) * q) as set ;
take x = x; ::_thesis: ( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x )
 (t * p) + ((1 - t) * q) in the carrier of (TOP-REAL 2) ;
hence  x in dom proj2 by FUNCT_2:def_1; ::_thesis: ( x in LSeg (p,q) & y = proj2 . x )
 (t * p) + ((1 - t) * q) in LSeg (q,p) by A3, A4;
hence  x in LSeg (p,q) ; ::_thesis: y = proj2 . x
thus y = ((t * p) `2) + ((1 - t) * (q `2)) by A5, TOPREAL3:4
.= ((t * p) `2) + (((1 - t) * q) `2) by TOPREAL3:4
.= ((t * p) + ((1 - t) * q)) `2 by TOPREAL3:2
.= proj2 . x by PSCOMP_1:def_6 ; ::_thesis: verum
end;
given x being set  such that  x in dom proj2 and
A6: x in LSeg (p,q) and
A7: y = proj2 . x ; ::_thesis: y in [.(p `2),(q `2).]
reconsider s = x as Point of (TOP-REAL 2) by A6;
 x in LSeg (q,p) by A6;
then consider r being Real such that
A8: s = ((1 - r) * q) + (r * p) and
A9: 0 <= r and
A10: r <= 1 ;
y = s `2 by A7, PSCOMP_1:def_6
.= (((1 - r) * q) `2) + ((r * p) `2) by A8, TOPREAL3:2
.= ((1 - r) * (q `2)) + ((r * p) `2) by TOPREAL3:4
.= ((1 - r) * (q `2)) + (r * (p `2)) by TOPREAL3:4 ;
hence  y in [.(p `2),(q `2).] by A1, A9, A10, Th51; ::_thesis: verum
end;
hence  proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).] by FUNCT_1:def_6; ::_thesis: verum
end;

theorem Th54: :: SPRECT_1:54
for p, q being Point of (TOP-REAL 2) st p `1 <= q `1 holds
W-bound (LSeg (p,q)) = p `1
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 <= q `1 implies W-bound (LSeg (p,q)) = p `1 )
assume A1: p `1 <= q `1 ; ::_thesis: W-bound (LSeg (p,q)) = p `1
then A2: proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).] by Th52;
thus  W-bound (LSeg (p,q)) = lower_bound (proj1 .: (LSeg (p,q))) by Th43
.= p `1 by A1, A2, JORDAN5A:19 ; ::_thesis: verum
end;

theorem Th55: :: SPRECT_1:55
for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds
S-bound (LSeg (p,q)) = p `2
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `2 <= q `2 implies S-bound (LSeg (p,q)) = p `2 )
assume A1: p `2 <= q `2 ; ::_thesis: S-bound (LSeg (p,q)) = p `2
then A2: proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).] by Th53;
thus  S-bound (LSeg (p,q)) = lower_bound (proj2 .: (LSeg (p,q))) by Th44
.= p `2 by A1, A2, JORDAN5A:19 ; ::_thesis: verum
end;

theorem Th56: :: SPRECT_1:56
for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds
N-bound (LSeg (p,q)) = q `2
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `2 <= q `2 implies N-bound (LSeg (p,q)) = q `2 )
assume A1: p `2 <= q `2 ; ::_thesis: N-bound (LSeg (p,q)) = q `2
then A2: proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).] by Th53;
thus  N-bound (LSeg (p,q)) = upper_bound (proj2 .: (LSeg (p,q))) by Th45
.= q `2 by A1, A2, JORDAN5A:19 ; ::_thesis: verum
end;

theorem Th57: :: SPRECT_1:57
for p, q being Point of (TOP-REAL 2) st p `1 <= q `1 holds
E-bound (LSeg (p,q)) = q `1
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 <= q `1 implies E-bound (LSeg (p,q)) = q `1 )
assume A1: p `1 <= q `1 ; ::_thesis: E-bound (LSeg (p,q)) = q `1
then A2: proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).] by Th52;
thus  E-bound (LSeg (p,q)) = upper_bound (proj1 .: (LSeg (p,q))) by Th46
.= q `1 by A1, A2, JORDAN5A:19 ; ::_thesis: verum
end;

theorem Th58: :: SPRECT_1:58
for C being non empty compact Subset of (TOP-REAL 2) holds W-bound (L~ (SpStSeq C)) = W-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: W-bound (L~ (SpStSeq C)) = W-bound C
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
set S3 = LSeg ((SE-corner C),(SW-corner C));
set S4 = LSeg ((SW-corner C),(NW-corner C));
A1: (SE-corner C) `1 = E-bound C by EUCLID:52;
A2: W-bound C <= E-bound C by Th21;
A3: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) is compact by COMPTS_1:10;
A4: (NE-corner C) `1 = E-bound C by EUCLID:52;
then A5: W-bound (LSeg ((NE-corner C),(SE-corner C))) = E-bound C by A1, Th54;
A6: (SW-corner C) `1 = W-bound C by EUCLID:52;
A7: (NW-corner C) `1 = W-bound C by EUCLID:52;
then A8: W-bound (LSeg ((SW-corner C),(NW-corner C))) = W-bound C by A6, Th54;
A9: W-bound ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) = min ((W-bound (LSeg ((SE-corner C),(SW-corner C)))),(W-bound (LSeg ((SW-corner C),(NW-corner C))))) by Th47
.= min ((W-bound C),(W-bound C)) by A1, A6, A8, Th21, Th54
.= W-bound C ;
A10: L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
A11: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) is compact by COMPTS_1:10;
W-bound ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) = min ((W-bound (LSeg ((NW-corner C),(NE-corner C)))),(W-bound (LSeg ((NE-corner C),(SE-corner C))))) by Th47
.= min ((E-bound C),(W-bound C)) by A7, A4, A5, Th21, Th54
.= W-bound C by A2, XXREAL_0:def_9 ;
hence  W-bound (L~ (SpStSeq C)) = min ((W-bound C),(W-bound C)) by A10, A11, A3, A9, Th47
.= W-bound C ;
::_thesis: verum
end;

theorem Th59: :: SPRECT_1:59
for C being non empty compact Subset of (TOP-REAL 2) holds S-bound (L~ (SpStSeq C)) = S-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: S-bound (L~ (SpStSeq C)) = S-bound C
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
set S3 = LSeg ((SE-corner C),(SW-corner C));
set S4 = LSeg ((SW-corner C),(NW-corner C));
A1: (SE-corner C) `2 = S-bound C by EUCLID:52;
A2: S-bound C <= N-bound C by Th22;
A3: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) is compact by COMPTS_1:10;
A4: (NE-corner C) `2 = N-bound C by EUCLID:52;
then A5: S-bound (LSeg ((NE-corner C),(SE-corner C))) = S-bound C by A1, Th22, Th55;
A6: (SW-corner C) `2 = S-bound C by EUCLID:52;
A7: (NW-corner C) `2 = N-bound C by EUCLID:52;
then A8: S-bound (LSeg ((SW-corner C),(NW-corner C))) = S-bound C by A6, Th22, Th55;
A9: S-bound ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) = min ((S-bound (LSeg ((SE-corner C),(SW-corner C)))),(S-bound (LSeg ((SW-corner C),(NW-corner C))))) by Th48
.= min ((S-bound C),(S-bound C)) by A1, A6, A8, Th55
.= S-bound C ;
A10: L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
A11: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) is compact by COMPTS_1:10;
S-bound ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) = min ((S-bound (LSeg ((NW-corner C),(NE-corner C)))),(S-bound (LSeg ((NE-corner C),(SE-corner C))))) by Th48
.= min ((N-bound C),(S-bound C)) by A7, A4, A5, Th55
.= S-bound C by A2, XXREAL_0:def_9 ;
hence  S-bound (L~ (SpStSeq C)) = min ((S-bound C),(S-bound C)) by A10, A11, A3, A9, Th48
.= S-bound C ;
::_thesis: verum
end;

theorem Th60: :: SPRECT_1:60
for C being non empty compact Subset of (TOP-REAL 2) holds N-bound (L~ (SpStSeq C)) = N-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: N-bound (L~ (SpStSeq C)) = N-bound C
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
set S3 = LSeg ((SE-corner C),(SW-corner C));
set S4 = LSeg ((SW-corner C),(NW-corner C));
A1: (NW-corner C) `2 = N-bound C by EUCLID:52;
A2: S-bound C <= N-bound C by Th22;
A3: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) is compact by COMPTS_1:10;
A4: (SW-corner C) `2 = S-bound C by EUCLID:52;
then A5: N-bound (LSeg ((SW-corner C),(NW-corner C))) = N-bound C by A1, Th22, Th56;
A6: (SE-corner C) `2 = S-bound C by EUCLID:52;
A7: (NE-corner C) `2 = N-bound C by EUCLID:52;
then A8: N-bound (LSeg ((NE-corner C),(SE-corner C))) = N-bound C by A6, Th22, Th56;
A9: N-bound ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) = max ((N-bound (LSeg ((NW-corner C),(NE-corner C)))),(N-bound (LSeg ((NE-corner C),(SE-corner C))))) by Th49
.= max ((N-bound C),(N-bound C)) by A1, A7, A8, Th56
.= N-bound C ;
A10: L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
A11: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) is compact by COMPTS_1:10;
N-bound ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) = max ((N-bound (LSeg ((SE-corner C),(SW-corner C)))),(N-bound (LSeg ((SW-corner C),(NW-corner C))))) by Th49
.= max ((S-bound C),(N-bound C)) by A6, A4, A5, Th56
.= N-bound C by A2, XXREAL_0:def_10 ;
hence  N-bound (L~ (SpStSeq C)) = max ((N-bound C),(N-bound C)) by A10, A11, A9, A3, Th49
.= N-bound C ;
::_thesis: verum
end;

theorem Th61: :: SPRECT_1:61
for C being non empty compact Subset of (TOP-REAL 2) holds E-bound (L~ (SpStSeq C)) = E-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: E-bound (L~ (SpStSeq C)) = E-bound C
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
set S3 = LSeg ((SE-corner C),(SW-corner C));
set S4 = LSeg ((SW-corner C),(NW-corner C));
A1: (NW-corner C) `1 = W-bound C by EUCLID:52;
A2: W-bound C <= E-bound C by Th21;
A3: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) is compact by COMPTS_1:10;
A4: (SW-corner C) `1 = W-bound C by EUCLID:52;
then A5: E-bound (LSeg ((SW-corner C),(NW-corner C))) = W-bound C by A1, Th57;
A6: (SE-corner C) `1 = E-bound C by EUCLID:52;
A7: (NE-corner C) `1 = E-bound C by EUCLID:52;
then A8: E-bound (LSeg ((NE-corner C),(SE-corner C))) = E-bound C by A6, Th57;
A9: E-bound ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) = max ((E-bound (LSeg ((NW-corner C),(NE-corner C)))),(E-bound (LSeg ((NE-corner C),(SE-corner C))))) by Th50
.= max ((E-bound C),(E-bound C)) by A1, A7, A8, Th21, Th57
.= E-bound C ;
A10: L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
A11: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) is compact by COMPTS_1:10;
E-bound ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) = max ((E-bound (LSeg ((SE-corner C),(SW-corner C)))),(E-bound (LSeg ((SW-corner C),(NW-corner C))))) by Th50
.= max ((W-bound C),(E-bound C)) by A6, A4, A5, Th21, Th57
.= E-bound C by A2, XXREAL_0:def_10 ;
hence  E-bound (L~ (SpStSeq C)) = max ((E-bound C),(E-bound C)) by A10, A11, A9, A3, Th50
.= E-bound C ;
::_thesis: verum
end;

theorem Th62: :: SPRECT_1:62
for C being non empty compact Subset of (TOP-REAL 2) holds NW-corner (L~ (SpStSeq C)) = NW-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: NW-corner (L~ (SpStSeq C)) = NW-corner C
thus  NW-corner (L~ (SpStSeq C)) = |[(W-bound C),(N-bound (L~ (SpStSeq C)))]| by Th58
.= NW-corner C by Th60 ; ::_thesis: verum
end;

theorem Th63: :: SPRECT_1:63
for C being non empty compact Subset of (TOP-REAL 2) holds NE-corner (L~ (SpStSeq C)) = NE-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: NE-corner (L~ (SpStSeq C)) = NE-corner C
thus  NE-corner (L~ (SpStSeq C)) = |[(E-bound C),(N-bound (L~ (SpStSeq C)))]| by Th61
.= NE-corner C by Th60 ; ::_thesis: verum
end;

theorem Th64: :: SPRECT_1:64
for C being non empty compact Subset of (TOP-REAL 2) holds SW-corner (L~ (SpStSeq C)) = SW-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: SW-corner (L~ (SpStSeq C)) = SW-corner C
thus  SW-corner (L~ (SpStSeq C)) = |[(W-bound C),(S-bound (L~ (SpStSeq C)))]| by Th58
.= SW-corner C by Th59 ; ::_thesis: verum
end;

theorem Th65: :: SPRECT_1:65
for C being non empty compact Subset of (TOP-REAL 2) holds SE-corner (L~ (SpStSeq C)) = SE-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: SE-corner (L~ (SpStSeq C)) = SE-corner C
thus  SE-corner (L~ (SpStSeq C)) = |[(E-bound C),(S-bound (L~ (SpStSeq C)))]| by Th61
.= SE-corner C by Th59 ; ::_thesis: verum
end;

theorem Th66: :: SPRECT_1:66
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: W-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(NW-corner C))
set X = L~ (SpStSeq C);
set S3 = LSeg ((SE-corner C),(SW-corner C));
set S4 = LSeg ((SW-corner C),(NW-corner C));
A1: LSeg ((SW-corner C),(NW-corner C)) c= (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) by XBOOLE_1:7;
 L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
then A2: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) c= L~ (SpStSeq C) by XBOOLE_1:7;
LSeg ((SW-corner (L~ (SpStSeq C))),(NW-corner (L~ (SpStSeq C)))) = LSeg ((SW-corner (L~ (SpStSeq C))),(NW-corner C)) by Th62
.= LSeg ((SW-corner C),(NW-corner C)) by Th64 ;
hence  W-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(NW-corner C)) by A1, A2, XBOOLE_1:1, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th67: :: SPRECT_1:67
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: N-most (L~ (SpStSeq C)) = LSeg ((NW-corner C),(NE-corner C))
set X = L~ (SpStSeq C);
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
A1: LSeg ((NW-corner C),(NE-corner C)) c= (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) by XBOOLE_1:7;
 L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
then A2: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) c= L~ (SpStSeq C) by XBOOLE_1:7;
LSeg ((NW-corner (L~ (SpStSeq C))),(NE-corner (L~ (SpStSeq C)))) = LSeg ((NW-corner (L~ (SpStSeq C))),(NE-corner C)) by Th63
.= LSeg ((NW-corner C),(NE-corner C)) by Th62 ;
hence  N-most (L~ (SpStSeq C)) = LSeg ((NW-corner C),(NE-corner C)) by A1, A2, XBOOLE_1:1, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th68: :: SPRECT_1:68
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: S-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(SE-corner C))
set X = L~ (SpStSeq C);
set S3 = LSeg ((SE-corner C),(SW-corner C));
set S4 = LSeg ((SW-corner C),(NW-corner C));
A1: LSeg ((SE-corner C),(SW-corner C)) c= (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) by XBOOLE_1:7;
 L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
then A2: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) c= L~ (SpStSeq C) by XBOOLE_1:7;
LSeg ((SW-corner (L~ (SpStSeq C))),(SE-corner (L~ (SpStSeq C)))) = LSeg ((SW-corner (L~ (SpStSeq C))),(SE-corner C)) by Th65
.= LSeg ((SW-corner C),(SE-corner C)) by Th64 ;
hence  S-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(SE-corner C)) by A1, A2, XBOOLE_1:1, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th69: :: SPRECT_1:69
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: E-most (L~ (SpStSeq C)) = LSeg ((SE-corner C),(NE-corner C))
set X = L~ (SpStSeq C);
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
A1: LSeg ((NE-corner C),(SE-corner C)) c= (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) by XBOOLE_1:7;
 L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by Th41;
then A2: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) c= L~ (SpStSeq C) by XBOOLE_1:7;
LSeg ((SE-corner (L~ (SpStSeq C))),(NE-corner (L~ (SpStSeq C)))) = LSeg ((SE-corner (L~ (SpStSeq C))),(NE-corner C)) by Th63
.= LSeg ((SE-corner C),(NE-corner C)) by Th65 ;
hence  E-most (L~ (SpStSeq C)) = LSeg ((SE-corner C),(NE-corner C)) by A1, A2, XBOOLE_1:1, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th70: :: SPRECT_1:70
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: proj2 .: (LSeg ((SW-corner C),(NW-corner C))) = [.(S-bound C),(N-bound C).]
A1: (NW-corner C) `2 = N-bound C by EUCLID:52;
 (SW-corner C) `2 = S-bound C by EUCLID:52;
hence  proj2 .: (LSeg ((SW-corner C),(NW-corner C))) = [.(S-bound C),(N-bound C).] by A1, Th22, Th53; ::_thesis: verum
end;

theorem Th71: :: SPRECT_1:71
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: proj1 .: (LSeg ((NW-corner C),(NE-corner C))) = [.(W-bound C),(E-bound C).]
A1: (NE-corner C) `1 = E-bound C by EUCLID:52;
 (NW-corner C) `1 = W-bound C by EUCLID:52;
hence  proj1 .: (LSeg ((NW-corner C),(NE-corner C))) = [.(W-bound C),(E-bound C).] by A1, Th21, Th52; ::_thesis: verum
end;

theorem Th72: :: SPRECT_1:72
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: proj2 .: (LSeg ((NE-corner C),(SE-corner C))) = [.(S-bound C),(N-bound C).]
A1: (SE-corner C) `2 = S-bound C by EUCLID:52;
 (NE-corner C) `2 = N-bound C by EUCLID:52;
hence  proj2 .: (LSeg ((NE-corner C),(SE-corner C))) = [.(S-bound C),(N-bound C).] by A1, Th22, Th53; ::_thesis: verum
end;

theorem Th73: :: SPRECT_1:73
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
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: proj1 .: (LSeg ((SE-corner C),(SW-corner C))) = [.(W-bound C),(E-bound C).]
A1: (SW-corner C) `1 = W-bound C by EUCLID:52;
 (SE-corner C) `1 = E-bound C by EUCLID:52;
hence  proj1 .: (LSeg ((SE-corner C),(SW-corner C))) = [.(W-bound C),(E-bound C).] by A1, Th21, Th52; ::_thesis: verum
end;

theorem Th74: :: SPRECT_1:74
for C being non empty compact Subset of (TOP-REAL 2) holds W-min (L~ (SpStSeq C)) = SW-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: W-min (L~ (SpStSeq C)) = SW-corner C
set X = L~ (SpStSeq C);
set S = W-most (L~ (SpStSeq C));
A1: W-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(NW-corner C)) by Th66;
A2: S-bound C <= N-bound C by Th22;
lower_bound (proj2 | (W-most (L~ (SpStSeq C)))) = lower_bound (rng (proj2 | (W-most (L~ (SpStSeq C))))) by RELSET_1:22
.= lower_bound (proj2 .: (W-most (L~ (SpStSeq C)))) by RELAT_1:115
.= lower_bound [.(S-bound C),(N-bound C).] by A1, Th70
.= S-bound C by A2, JORDAN5A:19 ;
hence  W-min (L~ (SpStSeq C)) = SW-corner C by Th58; ::_thesis: verum
end;

theorem Th75: :: SPRECT_1:75
for C being non empty compact Subset of (TOP-REAL 2) holds W-max (L~ (SpStSeq C)) = NW-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: W-max (L~ (SpStSeq C)) = NW-corner C
set X = L~ (SpStSeq C);
set S = W-most (L~ (SpStSeq C));
A1: W-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(NW-corner C)) by Th66;
A2: S-bound C <= N-bound C by Th22;
upper_bound (proj2 | (W-most (L~ (SpStSeq C)))) = upper_bound (rng (proj2 | (W-most (L~ (SpStSeq C))))) by RELSET_1:22
.= upper_bound (proj2 .: (W-most (L~ (SpStSeq C)))) by RELAT_1:115
.= upper_bound [.(S-bound C),(N-bound C).] by A1, Th70
.= N-bound C by A2, JORDAN5A:19 ;
hence  W-max (L~ (SpStSeq C)) = NW-corner C by Th58; ::_thesis: verum
end;

theorem Th76: :: SPRECT_1:76
for C being non empty compact Subset of (TOP-REAL 2) holds N-min (L~ (SpStSeq C)) = NW-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: N-min (L~ (SpStSeq C)) = NW-corner C
set X = L~ (SpStSeq C);
set S = N-most (L~ (SpStSeq C));
A1: N-most (L~ (SpStSeq C)) = LSeg ((NW-corner C),(NE-corner C)) by Th67;
A2: W-bound C <= E-bound C by Th21;
lower_bound (proj1 | (N-most (L~ (SpStSeq C)))) = lower_bound (rng (proj1 | (N-most (L~ (SpStSeq C))))) by RELSET_1:22
.= lower_bound (proj1 .: (N-most (L~ (SpStSeq C)))) by RELAT_1:115
.= lower_bound [.(W-bound C),(E-bound C).] by A1, Th71
.= W-bound C by A2, JORDAN5A:19 ;
hence  N-min (L~ (SpStSeq C)) = NW-corner C by Th60; ::_thesis: verum
end;

theorem Th77: :: SPRECT_1:77
for C being non empty compact Subset of (TOP-REAL 2) holds N-max (L~ (SpStSeq C)) = NE-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: N-max (L~ (SpStSeq C)) = NE-corner C
set X = L~ (SpStSeq C);
set S = N-most (L~ (SpStSeq C));
A1: N-most (L~ (SpStSeq C)) = LSeg ((NW-corner C),(NE-corner C)) by Th67;
A2: W-bound C <= E-bound C by Th21;
upper_bound (proj1 | (N-most (L~ (SpStSeq C)))) = upper_bound (rng (proj1 | (N-most (L~ (SpStSeq C))))) by RELSET_1:22
.= upper_bound (proj1 .: (N-most (L~ (SpStSeq C)))) by RELAT_1:115
.= upper_bound [.(W-bound C),(E-bound C).] by A1, Th71
.= E-bound C by A2, JORDAN5A:19 ;
hence  N-max (L~ (SpStSeq C)) = NE-corner C by Th60; ::_thesis: verum
end;

theorem Th78: :: SPRECT_1:78
for C being non empty compact Subset of (TOP-REAL 2) holds E-min (L~ (SpStSeq C)) = SE-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: E-min (L~ (SpStSeq C)) = SE-corner C
set X = L~ (SpStSeq C);
set S = E-most (L~ (SpStSeq C));
A1: E-most (L~ (SpStSeq C)) = LSeg ((SE-corner C),(NE-corner C)) by Th69;
A2: S-bound C <= N-bound C by Th22;
lower_bound (proj2 | (E-most (L~ (SpStSeq C)))) = lower_bound (rng (proj2 | (E-most (L~ (SpStSeq C))))) by RELSET_1:22
.= lower_bound (proj2 .: (E-most (L~ (SpStSeq C)))) by RELAT_1:115
.= lower_bound [.(S-bound C),(N-bound C).] by A1, Th72
.= S-bound C by A2, JORDAN5A:19 ;
hence  E-min (L~ (SpStSeq C)) = SE-corner C by Th61; ::_thesis: verum
end;

theorem Th79: :: SPRECT_1:79
for C being non empty compact Subset of (TOP-REAL 2) holds E-max (L~ (SpStSeq C)) = NE-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: E-max (L~ (SpStSeq C)) = NE-corner C
set X = L~ (SpStSeq C);
set S = E-most (L~ (SpStSeq C));
A1: E-most (L~ (SpStSeq C)) = LSeg ((SE-corner C),(NE-corner C)) by Th69;
A2: S-bound C <= N-bound C by Th22;
upper_bound (proj2 | (E-most (L~ (SpStSeq C)))) = upper_bound (rng (proj2 | (E-most (L~ (SpStSeq C))))) by RELSET_1:22
.= upper_bound (proj2 .: (E-most (L~ (SpStSeq C)))) by RELAT_1:115
.= upper_bound [.(S-bound C),(N-bound C).] by A1, Th72
.= N-bound C by A2, JORDAN5A:19 ;
hence  E-max (L~ (SpStSeq C)) = NE-corner C by Th61; ::_thesis: verum
end;

theorem Th80: :: SPRECT_1:80
for C being non empty compact Subset of (TOP-REAL 2) holds S-min (L~ (SpStSeq C)) = SW-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: S-min (L~ (SpStSeq C)) = SW-corner C
set X = L~ (SpStSeq C);
set S = S-most (L~ (SpStSeq C));
A1: S-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(SE-corner C)) by Th68;
A2: W-bound C <= E-bound C by Th21;
lower_bound (proj1 | (S-most (L~ (SpStSeq C)))) = lower_bound (rng (proj1 | (S-most (L~ (SpStSeq C))))) by RELSET_1:22
.= lower_bound (proj1 .: (S-most (L~ (SpStSeq C)))) by RELAT_1:115
.= lower_bound [.(W-bound C),(E-bound C).] by A1, Th73
.= W-bound C by A2, JORDAN5A:19 ;
hence  S-min (L~ (SpStSeq C)) = SW-corner C by Th59; ::_thesis: verum
end;

theorem Th81: :: SPRECT_1:81
for C being non empty compact Subset of (TOP-REAL 2) holds S-max (L~ (SpStSeq C)) = SE-corner C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: S-max (L~ (SpStSeq C)) = SE-corner C
set X = L~ (SpStSeq C);
set S = S-most (L~ (SpStSeq C));
A1: S-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(SE-corner C)) by Th68;
A2: W-bound C <= E-bound C by Th21;
upper_bound (proj1 | (S-most (L~ (SpStSeq C)))) = upper_bound (rng (proj1 | (S-most (L~ (SpStSeq C))))) by RELSET_1:22
.= upper_bound (proj1 .: (S-most (L~ (SpStSeq C)))) by RELAT_1:115
.= upper_bound [.(W-bound C),(E-bound C).] by A1, Th73
.= E-bound C by A2, JORDAN5A:19 ;
hence  S-max (L~ (SpStSeq C)) = SE-corner C by Th59; ::_thesis: verum
end;

begin

definition
let f be FinSequence of (TOP-REAL 2);
attrf is rectangular  means :Def2: :: SPRECT_1:def 2
 ex D being non empty compact non horizontal non vertical 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 compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D );

registration
let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
cluster SpStSeq D ->  rectangular ;
coherence
 SpStSeq D is rectangular by Def2;
end;

registration
clusterV19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like rectangular for FinSequence of the carrier of (TOP-REAL 2);
existence
 ex b1 being FinSequence of (TOP-REAL 2) st b1 is rectangular
proof
set D = the non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
take  SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ; ::_thesis: SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) is rectangular
take  the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ; :: according to SPRECT_1:def_2 ::_thesis: SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) = SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
thus  SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) = SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
end;

theorem :: SPRECT_1:82
for s being rectangular FinSequence of (TOP-REAL 2) holds len s = 5
proof
let s be rectangular FinSequence of (TOP-REAL 2); ::_thesis: len s = 5
 ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st s = SpStSeq D by Def2;
hence  len s = 5 by Th40; ::_thesis: verum
end;

registration
cluster rectangular  ->  non constant for 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
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is rectangular implies not f is constant )
assume  ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D ; :: according to SPRECT_1:def_2 ::_thesis: not f is constant
hence  not f is constant ; ::_thesis: verum
end;
end;

registration
cluster non empty rectangular  ->  non empty circular special unfolded s.c.c. standard for 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
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( f is rectangular implies ( f is standard & f is special & f is unfolded & f is circular & f is s.c.c. ) )
assume  ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D ; :: according to SPRECT_1:def_2 ::_thesis: ( f is standard & f is special & f is unfolded & f is circular & f is s.c.c. )
hence  ( f is standard & f is special & f is unfolded & f is circular & f is s.c.c. ) ; ::_thesis: verum
end;
end;

theorem :: SPRECT_1:83
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )
proof
let s be rectangular FinSequence of (TOP-REAL 2); ::_thesis: ( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: s = SpStSeq D by Def2;
A2: s /. 1 = NW-corner D by A1, Th35;
hence  s /. 1 = N-min (L~ s) by A1, Th76; ::_thesis: s /. 1 = W-max (L~ s)
thus  s /. 1 = W-max (L~ s) by A1, A2, Th75; ::_thesis: verum
end;

theorem :: SPRECT_1:84
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 2 = N-max (L~ s) & s /. 2 = E-max (L~ s) )
proof
let s be rectangular FinSequence of (TOP-REAL 2); ::_thesis: ( s /. 2 = N-max (L~ s) & s /. 2 = E-max (L~ s) )
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: s = SpStSeq D by Def2;
A2: s /. 2 = NE-corner D by A1, Th36;
hence  s /. 2 = N-max (L~ s) by A1, Th77; ::_thesis: s /. 2 = E-max (L~ s)
thus  s /. 2 = E-max (L~ s) by A1, A2, Th79; ::_thesis: verum
end;

theorem :: SPRECT_1:85
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 3 = S-max (L~ s) & s /. 3 = E-min (L~ s) )
proof
let s be rectangular FinSequence of (TOP-REAL 2); ::_thesis: ( s /. 3 = S-max (L~ s) & s /. 3 = E-min (L~ s) )
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: s = SpStSeq D by Def2;
A2: s /. 3 = SE-corner D by A1, Th37;
hence  s /. 3 = S-max (L~ s) by A1, Th81; ::_thesis: s /. 3 = E-min (L~ s)
thus  s /. 3 = E-min (L~ s) by A1, A2, Th78; ::_thesis: verum
end;

theorem :: SPRECT_1:86
for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 4 = S-min (L~ s) & s /. 4 = W-min (L~ s) )
proof
let s be rectangular FinSequence of (TOP-REAL 2); ::_thesis: ( s /. 4 = S-min (L~ s) & s /. 4 = W-min (L~ s) )
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: s = SpStSeq D by Def2;
A2: s /. 4 = SW-corner D by A1, Th38;
hence  s /. 4 = S-min (L~ s) by A1, Th80; ::_thesis: s /. 4 = W-min (L~ s)
thus  s /. 4 = W-min (L~ s) by A1, A2, Th74; ::_thesis: verum
end;

begin

theorem Th87: :: SPRECT_1:87
for r1, r2, s1, s2 being Real st r1 < r2 & s1 < s2 holds
[.r1,r2,s1,s2.] is Jordan
proof
let r1, r2, s1, s2 be Real; ::_thesis: ( r1 < r2 & s1 < s2 implies [.r1,r2,s1,s2.] is Jordan )
assume that
A1: r1 < r2 and
A2: s1 < s2 ; ::_thesis: [.r1,r2,s1,s2.] is Jordan
 [.r1,r2,s1,s2.] =  {  p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= s2 & p `2 >= s1 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = s2 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = s1 ) or ( p `1 = r2 & p `2 <= s2 & p `2 >= s1 ) )  }  by A1, A2, SPPOL_2:54;
hence  [.r1,r2,s1,s2.] is Jordan by A1, A2, JORDAN1:43; ::_thesis: verum
end;

registration
let f be rectangular FinSequence of (TOP-REAL 2);
cluster L~ f ->  Jordan ;
coherence
 L~ f is Jordan
proof
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: f = SpStSeq D by Def2;
A2: W-bound D < E-bound D by Th31;
A3: S-bound D < N-bound D by Th32;
 L~ f = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).] by A1, Th42;
hence  L~ f is Jordan by A2, A3, Th87; ::_thesis: verum
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
hereby  ::_thesis: ( 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 ` ) implies S is Jordan )
assume A1: S is Jordan ; ::_thesis: ( 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 ` ) )
hence  S ` <> {} by JORDAN1:def_2; ::_thesis: 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 ` )
consider A1, A2 being Subset of (TOP-REAL 2) such that
A2: S ` = A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1) \ A1 = (Cl A2) \ A2 and
A5: for C1, C2 being Subset of ((TOP-REAL 2) | (S `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) by A1, JORDAN1:def_2;
A6: A2 /\ (S `) = A2 by A2, XBOOLE_1:21;
 A1 /\ (S `) = A1 by A2, XBOOLE_1:21;
then reconsider C1 = A1, C2 = A2 as Subset of ((TOP-REAL 2) | (S `)) by A6, TOPS_2:29;
 C2 = A2 ;
then A7: C1 is a_component by A5;
take A1 = A1; ::_thesis: ex 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 ` )
take A2 = A2; ::_thesis: ( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
thus  S ` = A1 \/ A2 by A2; ::_thesis: ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
thus  A1 misses A2 by A3; ::_thesis: ( (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
thus  (Cl A1) \ A1 = (Cl A2) \ A2 by A4; ::_thesis: ( A1 is_a_component_of S ` & A2 is_a_component_of S ` )
 C1 = A1 ;
then  C2 is a_component by A5;
hence  ( A1 is_a_component_of S ` & A2 is_a_component_of S ` ) by A7, CONNSP_1:def_6; ::_thesis: verum
end;
assume A8: S ` <> {} ; ::_thesis: ( for A1, A2 being Subset of (TOP-REAL 2) holds
( not S ` = A1 \/ A2 or not A1 misses A2 or not (Cl A1) \ A1 = (Cl A2) \ A2 or not A1 is_a_component_of S ` or not A2 is_a_component_of S ` ) or S is Jordan )
given A1, A2 being Subset of (TOP-REAL 2) such that A9: S ` = A1 \/ A2 and
A10: A1 misses A2 and
A11: (Cl A1) \ A1 = (Cl A2) \ A2 and
A12: A1 is_a_component_of S ` and
A13: A2 is_a_component_of S ` ; ::_thesis: S is Jordan
reconsider a1 = A1, a2 = A2 as Subset of (TOP-REAL 2) ;
A14: ex B being Subset of ((TOP-REAL 2) | (S `)) st
( B = a2 & B is a_component ) by A13, CONNSP_1:def_6;
thus  S ` <> {} by A8; :: according to JORDAN1:def_2 ::_thesis: ex b1, b2 being Element of bool the carrier of (TOP-REAL 2) st
( S ` = b1 \/ b2 & b1 misses b2 & (Cl b1) \ b1 = (Cl b2) \ b2 & ( for b3, b4 being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b3 = b1 or not b4 = b2 or ( b3 is a_component & b4 is a_component ) ) ) )
take  a1 ; ::_thesis: ex b1 being Element of bool the carrier of (TOP-REAL 2) st
( S ` = a1 \/ b1 & a1 misses b1 & (Cl a1) \ a1 = (Cl b1) \ b1 & ( for b2, b3 being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b2 = a1 or not b3 = b1 or ( b2 is a_component & b3 is a_component ) ) ) )
take  a2 ; ::_thesis: ( S ` = a1 \/ a2 & a1 misses a2 & (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b1, b2 being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b1 = a1 or not b2 = a2 or ( b1 is a_component & b2 is a_component ) ) ) )
thus  S ` = a1 \/ a2 by A9; ::_thesis: ( a1 misses a2 & (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b1, b2 being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b1 = a1 or not b2 = a2 or ( b1 is a_component & b2 is a_component ) ) ) )
thus  a1 /\ a2 = {} by A10, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: ( (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b1, b2 being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b1 = a1 or not b2 = a2 or ( b1 is a_component & b2 is a_component ) ) ) )
thus  (Cl a1) \ a1 = (Cl a2) \ a2 by A11; ::_thesis: for b1, b2 being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b1 = a1 or not b2 = a2 or ( b1 is a_component & b2 is a_component ) )
 ex B being Subset of ((TOP-REAL 2) | (S `)) st
( B = a1 & B is a_component ) by A12, CONNSP_1:def_6;
hence  for b1, b2 being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b1 = a1 or not b2 = a2 or ( b1 is a_component & b2 is a_component ) ) by A14; ::_thesis: verum
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 Th88: :: SPRECT_1:88
for f being rectangular FinSequence of (TOP-REAL 2) holds LeftComp f misses RightComp f
proof
let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: LeftComp f misses RightComp f
A1: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
A2: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
A3: (L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:10;
consider A1, A2 being Subset of (TOP-REAL 2) such that
A4: (L~ f) ` = A1 \/ A2 and
A5: A1 misses A2 and
 (Cl A1) \ A1 = (Cl A2) \ A2 and
A6: A1 is_a_component_of (L~ f) ` and
A7: A2 is_a_component_of (L~ f) ` by Def3;
 (L~ f) ` <> {} by Def3;
then  {(LeftComp f),(RightComp f)} = {A1,A2} by A4, A6, A7, A1, A2, A3, Th7;
then  ( ( LeftComp f = A1 & RightComp f = A2 ) or ( LeftComp f = A2 & RightComp f = A1 ) ) by ZFMISC_1:6;
hence  LeftComp f misses RightComp f by A5; ::_thesis: verum
end;

registration
let f be non constant standard special_circular_sequence;
cluster LeftComp f ->  non empty ;
coherence
 not LeftComp f is empty
proof
A1: Int (left_cell (f,1)) c= LeftComp f by GOBOARD9:def_1;
 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
hence  not LeftComp f is empty by A1, GOBOARD9:15, XBOOLE_1:3; ::_thesis: verum
end;
cluster RightComp f ->  non empty ;
coherence
 not RightComp f is empty
proof
A2: Int (right_cell (f,1)) c= RightComp f by GOBOARD9:def_2;
 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
hence  not RightComp f is empty by A2, GOBOARD9:16, XBOOLE_1:3; ::_thesis: verum
end;
end;

theorem :: SPRECT_1:89
for f being rectangular FinSequence of (TOP-REAL 2) holds LeftComp f <> RightComp f
proof
let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: LeftComp f <> RightComp f
 LeftComp f misses RightComp f by Th88;
hence  LeftComp f <> RightComp f ; ::_thesis: verum
end;