:: 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;