sprect_1.miz



    begin

    registration

      cluster non empty constant for FinSequence;

      existence

      proof

        take <* 0 *>;

        thus thesis;

      end;

    end

    theorem :: SPRECT_1:1

    

     Th1: for f,g be FinSequence st (f ^ g) is constant holds f is constant & g is constant

    proof

      let f,g be FinSequence;

      assume (f ^ g) is constant;

      then

      reconsider h = (f ^ g) as constant FinSequence;

      ( rng f) c= ( rng h) by FINSEQ_1: 29;

      hence f is constant;

      ( rng g) c= ( rng h) by FINSEQ_1: 30;

      hence thesis;

    end;

    theorem :: SPRECT_1:2

    

     Th2: for x,y be set st <*x, y*> is constant holds x = y

    proof

      let x,y be set;

      

       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;

      then

      reconsider s = <*x, y*> as constant Function;

      

       A3: x in {x, y} by TARSKI:def 2;

      ( rng s) is trivial;

      hence thesis by A1, A3, A2, ZFMISC_1:def 10;

    end;

    theorem :: SPRECT_1:3

    

     Th3: for x,y,z be set st <*x, y, z*> is constant holds x = y & y = z & z = x

    proof

      let x,y,z be set;

      

       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;

      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 thesis by A1, A3, A2, A4, ZFMISC_1:def 10;

    end;

    begin

    theorem :: SPRECT_1:4

    

     Th4: for GX be non empty TopSpace, A be Subset of GX, B be non empty Subset of GX holds A is_a_component_of B implies A <> {}

    proof

      let GX be non empty TopSpace, A be Subset of GX, B be non empty Subset of GX;

      assume A is_a_component_of B;

      then

      consider B1 be 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 thesis by A1;

    end;

    theorem :: SPRECT_1:5

    

     Th5: for GX be TopStruct, A,B be Subset of GX holds A is_a_component_of B implies A c= B

    proof

      let GX be TopStruct, A,B be Subset of GX;

      assume A is_a_component_of B;

      then

       A1: ex B1 be 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 thesis by A1;

    end;

    theorem :: SPRECT_1:6

    

     Th6: for T be non empty TopSpace, A be non empty Subset of T, B1,B2,S be 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 holds S = B1 or S = B2

    proof

      let T be non empty TopSpace, A be non empty Subset of T, B1,B2,S be Subset of T such 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;

      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 thesis by A1, A2, A3, GOBOARD9: 1;

    end;

    theorem :: SPRECT_1:7

    

     Th7: for T be non empty TopSpace, A be non empty Subset of T, B1,B2,C1,C2 be 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, A be non empty Subset of T, B1,B2,C1,C2 be Subset of T such 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;

      now

        let x be object;

        x = B1 or x = B2 iff x = C1 or x = C2 by A1, A2, A3, A4, A5, A6, Th6;

        hence x in {B1, B2} iff x = C1 or x = C2 by TARSKI:def 2;

      end;

      hence thesis by TARSKI:def 2;

    end;

    begin

    reserve S for Subset of ( TOP-REAL 2),

C,C1,C2 for non empty compact Subset of ( TOP-REAL 2),

p,q for Point of ( TOP-REAL 2);

    theorem :: SPRECT_1:8

    

     Th8: for p,q,r be 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);

      

       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;

    end;

    registration

      let n be Nat;

      let f be non trivial FinSequence of ( TOP-REAL n);

      cluster ( L~ f) -> non empty;

      coherence

      proof

        

         A1: ( len f) <> 1 by NAT_D: 60;

        ( len f) <> 0 by NAT_D: 60;

        hence thesis by A1, TOPREAL1: 22;

      end;

    end

    registration

      let f be FinSequence of ( TOP-REAL 2);

      cluster ( L~ f) -> compact;

      coherence

      proof

        defpred X[ Nat] means for f be FinSequence of ( TOP-REAL 2) st ( len f) = $1 holds ( L~ f) is compact;

        

         A1: for m be Nat st X[m] holds X[(m + 1)]

        proof

          let m be Nat;

          assume

           A2: for f be FinSequence of ( TOP-REAL 2) st ( len f) = m holds ( L~ f) is compact;

          let f be FinSequence of ( TOP-REAL 2);

          assume

           A3: ( len f) = (m + 1);

          then

          consider q be FinSequence of ( TOP-REAL 2), x be 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;

          per cases ;

            suppose q is empty;

            

            then ( L~ f) = ( L~ <*x*>) by A4, FINSEQ_1: 34

            .= ( {} ( TOP-REAL 2)) by SPPOL_2: 12;

            hence thesis;

          end;

            suppose q is non empty;

            

            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 thesis by A5, COMPTS_1: 10;

          end;

        end;

        

         A6: X[ 0 ]

        proof

          let f be FinSequence of ( TOP-REAL 2);

          assume ( len f) = 0 ;

          then ( L~ f) = ( {} ( TOP-REAL 2)) by TOPREAL1: 22;

          hence thesis;

        end;

        for m be Nat holds X[m] from NAT_1:sch 2( A6, A1);

        hence thesis;

      end;

    end

    theorem :: SPRECT_1:9

    

     Th9: for A,B be Subset of ( TOP-REAL 2) st A c= B & B is horizontal holds A is horizontal;

    theorem :: SPRECT_1:10

    

     Th10: for A,B be Subset of ( TOP-REAL 2) st A c= B & B is vertical holds A is vertical;

    registration

      cluster R^2-unit_square -> special_polygonal non horizontal non vertical;

      coherence

      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 Sq is special_polygonal;

        

         A3: (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) \/ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) c= Sq 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 Sq is horizontal by A3, A2, Th9, XBOOLE_1: 1;

        

         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 thesis by A3, A5, Th10, XBOOLE_1: 1;

      end;

    end

    registration

      cluster non vertical non horizontal non empty compact for Subset of ( TOP-REAL 2);

      existence

      proof

        take R^2-unit_square ;

        thus thesis;

      end;

    end

    begin

    theorem :: SPRECT_1:11

    

     Th11: ( N-min C) in C & ( N-max C) in C

    proof

      

       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 thesis by A1, A2;

    end;

    theorem :: SPRECT_1:12

    

     Th12: ( S-min C) in C & ( S-max C) in C

    proof

      

       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 thesis by A1, A2;

    end;

    theorem :: SPRECT_1:13

    

     Th13: ( W-min C) in C & ( W-max C) in C

    proof

      

       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 thesis by A1, A2;

    end;

    theorem :: SPRECT_1:14

    

     Th14: ( E-min C) in C & ( E-max C) in C

    proof

      

       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 thesis by A1, A2;

    end;

    theorem :: SPRECT_1:15

    

     Th15: C is vertical iff ( W-bound C) = ( E-bound C)

    proof

      thus C is vertical implies ( W-bound C) = ( E-bound C)

      proof

        

         A1: ( E-min C) in C by Th14;

        

         A2: ( W-min C) in C by Th13;

        assume

         A3: C is vertical;

        

        thus ( W-bound C) = (( W-min C) `1 ) by EUCLID: 52

        .= (( E-min C) `1 ) by A3, A2, A1

        .= ( E-bound C) by EUCLID: 52;

      end;

      assume

       A4: ( W-bound C) = ( E-bound C);

      let p, q;

      assume that

       A5: p in C and

       A6: q in C;

      

       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 thesis by A4, A9, A8, XXREAL_0: 1;

    end;

    theorem :: SPRECT_1:16

    

     Th16: C is horizontal iff ( S-bound C) = ( N-bound C)

    proof

      thus C is horizontal implies ( S-bound C) = ( N-bound C)

      proof

        

         A1: ( N-min C) in C by Th11;

        

         A2: ( S-min C) in C by Th12;

        assume

         A3: C is horizontal;

        

        thus ( S-bound C) = (( S-min C) `2 ) by EUCLID: 52

        .= (( N-min C) `2 ) by A3, A2, A1

        .= ( N-bound C) by EUCLID: 52;

      end;

      assume

       A4: ( S-bound C) = ( N-bound C);

      let p, q;

      assume that

       A5: p in C and

       A6: q in C;

      

       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 thesis by A4, A9, A8, XXREAL_0: 1;

    end;

    theorem :: SPRECT_1:17

    ( NW-corner C) = ( NE-corner C) implies C is vertical

    proof

      assume ( NW-corner C) = ( NE-corner C);

      then ( W-bound C) = ( E-bound C) by SPPOL_2: 1;

      hence thesis by Th15;

    end;

    theorem :: SPRECT_1:18

    ( SW-corner C) = ( SE-corner C) implies C is vertical

    proof

      assume ( SW-corner C) = ( SE-corner C);

      then ( W-bound C) = ( E-bound C) by SPPOL_2: 1;

      hence thesis by Th15;

    end;

    theorem :: SPRECT_1:19

    ( NW-corner C) = ( SW-corner C) implies C is horizontal

    proof

      assume ( NW-corner C) = ( SW-corner C);

      then ( S-bound C) = ( N-bound C) by SPPOL_2: 1;

      hence thesis by Th16;

    end;

    theorem :: SPRECT_1:20

    ( NE-corner C) = ( SE-corner C) implies C is horizontal

    proof

      assume ( NE-corner C) = ( SE-corner C);

      then ( S-bound C) = ( N-bound C) by SPPOL_2: 1;

      hence thesis by Th16;

    end;

    reserve i,j,k for Nat,

t,r1,r2,s1,s2 for Real;

    theorem :: SPRECT_1:21

    

     Th21: ( W-bound C) <= ( E-bound C)

    proof

      

       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 thesis by A2, XXREAL_0: 2;

    end;

    theorem :: SPRECT_1:22

    

     Th22: ( S-bound C) <= ( N-bound C)

    proof

      

       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 thesis by A2, XXREAL_0: 2;

    end;

    theorem :: SPRECT_1:23

    

     Th23: ( LSeg (( SE-corner C),( NE-corner C))) = { p : (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) }

    proof

      set L = { p : (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) };

      set q1 = ( SE-corner C), q2 = ( NE-corner C);

      

       A1: (q1 `1 ) = ( E-bound C) by EUCLID: 52;

      

       A2: (q1 `2 ) = ( S-bound C) by EUCLID: 52;

      

       A3: (q2 `1 ) = ( E-bound C) by EUCLID: 52;

      

       A4: (q2 `2 ) = ( N-bound C) by EUCLID: 52;

      

       A5: ( S-bound C) <= ( N-bound C) by Th22;

      thus ( LSeg (q1,q2)) c= L

      proof

        let a be object;

        assume

         A6: a in ( LSeg (q1,q2));

        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 thesis by A7, A8;

      end;

      let a be object;

      assume a in L;

      then ex p st p = a & (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C);

      hence thesis by A1, A2, A3, A4, GOBOARD7: 7;

    end;

    theorem :: SPRECT_1:24

    

     Th24: ( LSeg (( SW-corner C),( SE-corner C))) = { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) }

    proof

      set L = { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) };

      set q1 = ( SW-corner C), q2 = ( SE-corner C);

      

       A1: (q1 `1 ) = ( W-bound C) by EUCLID: 52;

      

       A2: (q2 `2 ) = ( S-bound C) by EUCLID: 52;

      

       A3: (q1 `2 ) = ( S-bound C) by EUCLID: 52;

      

       A4: (q2 `1 ) = ( E-bound C) by EUCLID: 52;

      

       A5: ( W-bound C) <= ( E-bound C) by Th21;

      thus ( LSeg (q1,q2)) c= L

      proof

        let a be object;

        assume

         A6: a in ( LSeg (q1,q2));

        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 thesis by A7, A8;

      end;

      let a be object;

      assume a in L;

      then ex p st p = a & (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C);

      hence thesis by A1, A3, A4, A2, GOBOARD7: 8;

    end;

    theorem :: SPRECT_1:25

    

     Th25: ( LSeg (( NW-corner C),( NE-corner C))) = { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) }

    proof

      set L = { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) };

      set q1 = ( NW-corner C), q2 = ( NE-corner C);

      

       A1: (q1 `1 ) = ( W-bound C) by EUCLID: 52;

      

       A2: (q2 `2 ) = ( N-bound C) by EUCLID: 52;

      

       A3: (q1 `2 ) = ( N-bound C) by EUCLID: 52;

      

       A4: (q2 `1 ) = ( E-bound C) by EUCLID: 52;

      

       A5: ( W-bound C) <= ( E-bound C) by Th21;

      thus ( LSeg (q1,q2)) c= L

      proof

        let a be object;

        assume

         A6: a in ( LSeg (q1,q2));

        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 thesis by A7, A8;

      end;

      let a be object;

      assume a in L;

      then ex p st p = a & (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C);

      hence thesis by A1, A3, A4, A2, GOBOARD7: 8;

    end;

    theorem :: SPRECT_1:26

    

     Th26: ( LSeg (( SW-corner C),( NW-corner C))) = { p : (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) }

    proof

      set L = { p : (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) };

      set q1 = ( SW-corner C), q2 = ( NW-corner C);

      

       A1: (q1 `1 ) = ( W-bound C) by EUCLID: 52;

      

       A2: (q1 `2 ) = ( S-bound C) by EUCLID: 52;

      

       A3: (q2 `1 ) = ( W-bound C) by EUCLID: 52;

      

       A4: (q2 `2 ) = ( N-bound C) by EUCLID: 52;

      

       A5: ( S-bound C) <= ( N-bound C) by Th22;

      thus ( LSeg (q1,q2)) c= L

      proof

        let a be object;

        assume

         A6: a in ( LSeg (q1,q2));

        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 thesis by A7, A8;

      end;

      let a be object;

      assume a in L;

      then ex p st p = a & (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C);

      hence thesis by A1, A2, A3, A4, GOBOARD7: 7;

    end;

    theorem :: SPRECT_1:27

    (( LSeg (( SW-corner C),( NW-corner C))) /\ ( LSeg (( NW-corner C),( NE-corner C)))) = {( NW-corner C)}

    proof

      for a be object 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 object;

        thus a in (( LSeg (( SW-corner C),( NW-corner C))) /\ ( LSeg (( NW-corner C),( NE-corner C)))) implies a = ( NW-corner C)

        proof

          assume

           A1: a in (( LSeg (( SW-corner C),( NW-corner C))) /\ ( LSeg (( NW-corner C),( NE-corner C))));

          then a in ( LSeg (( NW-corner C),( NE-corner C))) by XBOOLE_0:def 4;

          then a in { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) } by Th25;

          then

           A2: ex p 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 : (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) } by Th26;

          then ex p st p = a & (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C);

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = ( NW-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 thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: SPRECT_1:28

    

     Th28: (( LSeg (( NW-corner C),( NE-corner C))) /\ ( LSeg (( NE-corner C),( SE-corner C)))) = {( NE-corner C)}

    proof

      for a be object 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 object;

        thus a in (( LSeg (( NW-corner C),( NE-corner C))) /\ ( LSeg (( NE-corner C),( SE-corner C)))) implies a = ( NE-corner C)

        proof

          assume

           A1: a in (( LSeg (( NW-corner C),( NE-corner C))) /\ ( LSeg (( NE-corner C),( SE-corner C))));

          then a in ( LSeg (( NE-corner C),( SE-corner C))) by XBOOLE_0:def 4;

          then a in { p : (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) } by Th23;

          then

           A2: ex p 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 : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) } by Th25;

          then ex p st p = a & (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C);

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = ( NE-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 thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: SPRECT_1:29

    

     Th29: (( LSeg (( SE-corner C),( NE-corner C))) /\ ( LSeg (( SW-corner C),( SE-corner C)))) = {( SE-corner C)}

    proof

      for a be object 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 object;

        thus a in (( LSeg (( NE-corner C),( SE-corner C))) /\ ( LSeg (( SE-corner C),( SW-corner C)))) implies a = ( SE-corner C)

        proof

          assume

           A1: a in (( LSeg (( NE-corner C),( SE-corner C))) /\ ( LSeg (( SE-corner C),( SW-corner C))));

          then a in ( LSeg (( SE-corner C),( SW-corner C))) by XBOOLE_0:def 4;

          then a in { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) } by Th24;

          then

           A2: ex p 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 : (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) } by Th23;

          then ex p st p = a & (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C);

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = ( SE-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 thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: SPRECT_1:30

    

     Th30: (( LSeg (( NW-corner C),( SW-corner C))) /\ ( LSeg (( SW-corner C),( SE-corner C)))) = {( SW-corner C)}

    proof

      for a be object 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 object;

        thus a in (( LSeg (( NW-corner C),( SW-corner C))) /\ ( LSeg (( SW-corner C),( SE-corner C)))) implies a = ( SW-corner C)

        proof

          assume

           A1: a in (( LSeg (( NW-corner C),( SW-corner C))) /\ ( LSeg (( SW-corner C),( SE-corner C))));

          then a in ( LSeg (( SW-corner C),( SE-corner C))) by XBOOLE_0:def 4;

          then a in { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) } by Th24;

          then

           A2: ex p 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 : (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) } by Th26;

          then ex p st p = a & (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C);

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = ( SW-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 thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    begin

    reserve D1 for non vertical non empty compact Subset of ( TOP-REAL 2),

D2 for non horizontal non empty compact Subset of ( TOP-REAL 2),

D for non vertical non horizontal non empty compact Subset of ( TOP-REAL 2);

    theorem :: SPRECT_1:31

    

     Th31: ( W-bound D1) < ( E-bound D1)

    proof

      

       A1: ( W-bound D1) <> ( E-bound D1) by Th15;

      ( W-bound D1) <= ( E-bound D1) by Th21;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: SPRECT_1:32

    

     Th32: ( S-bound D2) < ( N-bound D2)

    proof

      

       A1: ( S-bound D2) <> ( N-bound D2) by Th16;

      ( S-bound D2) <= ( N-bound D2) by Th22;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: SPRECT_1:33

    

     Th33: ( LSeg (( SW-corner D1),( NW-corner D1))) misses ( LSeg (( SE-corner D1),( NE-corner D1)))

    proof

      assume (( LSeg (( SW-corner D1),( NW-corner D1))) /\ ( LSeg (( SE-corner D1),( NE-corner D1)))) <> {} ;

      then

      consider a be object 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 : (p `1 ) = ( E-bound D1) & (p `2 ) <= ( N-bound D1) & (p `2 ) >= ( S-bound D1) } by Th23;

      then

       A2: ex p 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 : (p `1 ) = ( W-bound D1) & (p `2 ) <= ( N-bound D1) & (p `2 ) >= ( S-bound D1) } by Th26;

      then ex p st p = a & (p `1 ) = ( W-bound D1) & (p `2 ) <= ( N-bound D1) & (p `2 ) >= ( S-bound D1);

      hence contradiction by A2, Th15;

    end;

    theorem :: SPRECT_1:34

    

     Th34: ( LSeg (( SW-corner D2),( SE-corner D2))) misses ( LSeg (( NW-corner D2),( NE-corner D2)))

    proof

      assume (( LSeg (( SW-corner D2),( SE-corner D2))) /\ ( LSeg (( NW-corner D2),( NE-corner D2)))) <> {} ;

      then

      consider a be object 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 : (p `1 ) <= ( E-bound D2) & (p `1 ) >= ( W-bound D2) & (p `2 ) = ( N-bound D2) } by Th25;

      then

       A2: ex p 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 : (p `1 ) <= ( E-bound D2) & (p `1 ) >= ( W-bound D2) & (p `2 ) = ( S-bound D2) } by Th24;

      then ex p st p = a & (p `1 ) <= ( E-bound D2) & (p `1 ) >= ( W-bound D2) & (p `2 ) = ( S-bound D2);

      hence contradiction by A2, Th16;

    end;

    begin

    definition

      let C be Subset of ( TOP-REAL 2);

      :: SPRECT_1:def1

      func SpStSeq C -> FinSequence of ( TOP-REAL 2) equals ( <*( NW-corner C), ( NE-corner C), ( SE-corner C)*> ^ <*( SW-corner C), ( NW-corner C)*>);

      coherence ;

    end

    theorem :: SPRECT_1:35

    

     Th35: (( SpStSeq S) /. 1) = ( NW-corner S)

    proof

      1 in ( dom <*( NW-corner S), ( NE-corner S), ( SE-corner S)*>) by FINSEQ_1: 81;

      

      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;

    end;

    theorem :: SPRECT_1:36

    

     Th36: (( SpStSeq S) /. 2) = ( NE-corner S)

    proof

      2 in ( dom <*( NW-corner S), ( NE-corner S), ( SE-corner S)*>) by FINSEQ_1: 81;

      

      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;

    end;

    theorem :: SPRECT_1:37

    

     Th37: (( SpStSeq S) /. 3) = ( SE-corner S)

    proof

      3 in ( dom <*( NW-corner S), ( NE-corner S), ( SE-corner S)*>) by FINSEQ_1: 81;

      

      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;

    end;

    theorem :: SPRECT_1:38

    

     Th38: (( SpStSeq S) /. 4) = ( SW-corner S)

    proof

      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 g) = 3 by FINSEQ_1: 45;

      

      hence (( SpStSeq S) /. 4) = (( SpStSeq S) /. (( len g) + 1))

      .= ( <*( SW-corner S), ( NW-corner S)*> /. 1) by A1, FINSEQ_4: 69

      .= ( SW-corner S) by FINSEQ_4: 17;

    end;

    theorem :: SPRECT_1:39

    (( SpStSeq S) /. 5) = ( NW-corner S)

    proof

      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 g) = 3 by FINSEQ_1: 45;

      

      hence (( SpStSeq S) /. 5) = (( SpStSeq S) /. (( len g) + 2))

      .= ( <*( SW-corner S), ( NW-corner S)*> /. 2) by A1, FINSEQ_4: 69

      .= ( NW-corner S) by FINSEQ_4: 17;

    end;

    theorem :: SPRECT_1:40

    

     Th40: ( len ( SpStSeq S)) = 5

    proof

      

      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;

    end;

    theorem :: SPRECT_1:41

    

     Th41: ( 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

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

    end;

    registration

      let D be non vertical non empty compact Subset of ( TOP-REAL 2);

      cluster ( SpStSeq D) -> non constant;

      coherence

      proof

        assume ( SpStSeq D) is constant;

        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;

      end;

    end

    registration

      let D be non horizontal non empty compact Subset of ( TOP-REAL 2);

      cluster ( SpStSeq D) -> non constant;

      coherence

      proof

        assume ( SpStSeq D) is constant;

        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;

      end;

    end

    registration

      let D be non vertical non horizontal non empty compact Subset of ( TOP-REAL 2);

      cluster ( SpStSeq D) -> special unfolded circular s.c.c. standard;

      coherence

      proof

        reconsider Sb = ( S-bound D), Nb = ( N-bound D), Wb = ( W-bound D), Eb = ( E-bound D) as Element of REAL by XREAL_0:def 1;

        

         A1: <*Sb, Nb*> is increasing

        proof

          let n,m be Nat;

          assume that

           A2: n in ( dom <*Sb, Nb*>) and

           A3: m in ( dom <*Sb, Nb*>);

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

          

           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 ( <*Sb, Nb*> . n) < ( <*Sb, Nb*> . m) by A8, Th32;

        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 = <*Nb, Nb, Sb*>, Yf2 = <*Sb, Nb*>;

        set Xf1 = <*Wb, Eb, Eb*>, Xf2 = <*Wb, Wb*>;

        set f = ( SpStSeq D);

        set f1 = <*( NW-corner D), ( NE-corner D), ( SE-corner D)*>, f2 = <*( SW-corner D), ( NW-corner D)*>;

        reconsider Xf = (Xf1 ^ Xf2) as FinSequence of REAL ;

        

         A9: ( rng Xf2) = {( W-bound D), ( W-bound D)} by FINSEQ_2: 127

        .= {( W-bound D)} by ENUMSET1: 29;

        ( rng Xf1) = {( 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: <*Wb, Eb*> is increasing

        proof

          let n,m be Nat;

          assume that

           A13: n in ( dom <*Wb, Eb*>) and

           A14: m in ( dom <*Wb, Eb*>);

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

          

           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 ( <*Wb, Eb*> . n) < ( <*Wb, Eb*> . m) by A19, Th31;

        end;

        

         A20: ( S-bound D) < ( N-bound D) by Th32;

        reconsider Yf = (Yf1 ^ Yf2) as FinSequence of REAL ;

        

         A21: ( rng Yf2) = {( S-bound D), ( N-bound D)} by FINSEQ_2: 127;

        ( rng Yf1) = {( 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 Yf1) = 3 by FINSEQ_1: 45;

        then 1 in ( dom Yf1) by FINSEQ_3: 25;

        

        then

         A26: (Yf . 1) = (Yf1 . 1) by FINSEQ_1:def 7

        .= ( N-bound D) by FINSEQ_1: 45;

        

         A27: ( len Yf2) = 2 by FINSEQ_1: 44;

        then

         A28: ( len Yf) = (3 + 2) by A25, FINSEQ_1: 22;

        2 in ( dom Yf2) by A27, FINSEQ_3: 25;

        

        then

         A29: (Yf . (3 + 2)) = (Yf2 . 2) by A25, FINSEQ_1:def 7

        .= ( N-bound D) by FINSEQ_1: 44;

        3 in ( dom Yf1) by A25, FINSEQ_3: 25;

        

        then

         A30: (Yf . 3) = (Yf1 . 3) by FINSEQ_1:def 7

        .= ( S-bound D) by FINSEQ_1: 45;

        2 in ( dom Yf1) by A25, FINSEQ_3: 25;

        

        then

         A31: (Yf . 2) = (Yf1 . 2) by FINSEQ_1:def 7

        .= ( N-bound D) by FINSEQ_1: 45;

        

         A32: ( len f1) = 3 by FINSEQ_1: 45;

        then 1 in ( dom f1) by FINSEQ_3: 25;

        

        then

         A33: (f /. 1) = (f1 /. 1) by FINSEQ_4: 68

        .= ( NW-corner D) by FINSEQ_4: 18;

        3 in ( dom f1) by A32, FINSEQ_3: 25;

        

        then

         A34: (f /. 3) = (f1 /. 3) by FINSEQ_4: 68

        .= ( SE-corner D) by FINSEQ_4: 18;

        2 in ( dom f1) by A32, FINSEQ_3: 25;

        

        then

         A35: (f /. 2) = (f1 /. 2) by FINSEQ_4: 68

        .= ( NE-corner D) by FINSEQ_4: 18;

        

         A36: ( len f2) = 2 by FINSEQ_1: 44;

        then

         A37: ( len (f1 ^ f2)) = (3 + 2) by A32, FINSEQ_1: 22;

        1 in ( dom f2) by A36, FINSEQ_3: 25;

        

        then

         A38: (f /. (3 + 1)) = (f2 /. 1) by A32, FINSEQ_4: 69

        .= ( SW-corner D) by FINSEQ_4: 17;

        then

         A39: ( LSeg (f,3)) = ( LSeg (( SE-corner D),( SW-corner D))) by A37, A34, TOPREAL1:def 3;

        2 in ( dom f2) by A36, FINSEQ_3: 25;

        

        then

         A40: (f /. (3 + 2)) = (f2 /. 2) by A32, FINSEQ_4: 69

        .= ( NW-corner D) by FINSEQ_4: 17;

        thus f is special

        proof

          let i be Nat;

          assume 1 <= i;

          then (1 + 1) <= (i + 1) by XREAL_1: 6;

          then

           A41: 1 < (i + 1) by XXREAL_0: 2;

          assume (i + 1) <= ( len f);

          then

           A42: (i + 1) = 0 or ... or (i + 1) = 5 by A37;

          per cases by A41, A42;

            suppose

             A43: i = 1;

            ((f /. 1) `2 ) = ( N-bound D) by A33, EUCLID: 52

            .= ((f /. (1 + 1)) `2 ) by A35, EUCLID: 52;

            hence thesis by A43;

          end;

            suppose

             A44: i = 2;

            ((f /. 2) `1 ) = ( E-bound D) by A35, EUCLID: 52

            .= ((f /. (2 + 1)) `1 ) by A34, EUCLID: 52;

            hence thesis by A44;

          end;

            suppose

             A45: i = 3;

            ((f /. 3) `2 ) = ( S-bound D) by A34, EUCLID: 52

            .= ((f /. (3 + 1)) `2 ) by A38, EUCLID: 52;

            hence thesis by A45;

          end;

            suppose

             A46: i = 4;

            ((f /. 4) `1 ) = ( W-bound D) by A38, EUCLID: 52

            .= ((f /. (4 + 1)) `1 ) by A40, EUCLID: 52;

            hence thesis by A46;

          end;

        end;

        (4 + 1) = 5;

        then

         A47: ( LSeg (f,4)) = ( LSeg (( SW-corner D),( NW-corner D))) by A37, A38, A40, TOPREAL1:def 3;

        (2 + 1) = 3;

        then

         A48: ( LSeg (f,2)) = ( LSeg (( NE-corner D),( SE-corner D))) by A37, A35, A34, TOPREAL1:def 3;

        1 in ( dom Yf2) by A27, FINSEQ_3: 25;

        

        then

         A49: (Yf . (3 + 1)) = (Yf2 . 1) by A25, FINSEQ_1:def 7

        .= ( S-bound D) by FINSEQ_1: 44;

        now

          let n be Nat;

          assume

           A50: n in ( dom Yf);

          then

           A51: n <> 0 by FINSEQ_3: 25;

          n <= 5 by A28, A50, FINSEQ_3: 25;

          then n = 0 or ... or n = 5;

          per cases by A51;

            suppose n = 1;

            hence (Yf . n) = ((f /. n) `2 ) by A33, A26, EUCLID: 52;

          end;

            suppose n = 2;

            hence (Yf . n) = ((f /. n) `2 ) by A35, A31, EUCLID: 52;

          end;

            suppose n = 3;

            hence (Yf . n) = ((f /. n) `2 ) by A34, A30, EUCLID: 52;

          end;

            suppose n = 4;

            hence (Yf . n) = ((f /. n) `2 ) by A38, A49, EUCLID: 52;

          end;

            suppose n = 5;

            hence (Yf . n) = ((f /. n) `2 ) by A40, A29, EUCLID: 52;

          end;

        end;

        then Yf = ( Y_axis f) by A37, A28, GOBOARD1:def 2;

        then

         A52: <*( S-bound D), ( N-bound D)*> = ( Incr ( Y_axis f)) by A23, A24, A1, SEQ_4:def 21;

        (1 + 1) = 2;

        then

         A53: ( LSeg (f,1)) = ( LSeg (( NW-corner D),( NE-corner D))) by A37, A33, A35, TOPREAL1:def 3;

        thus f is unfolded

        proof

          let i be Nat;

          assume 1 <= i;

          then

           A54: (1 + 2) <= (i + 2) by XREAL_1: 6;

          assume

           A55: (i + 2) <= ( len f);

          

           A56: 2 < (i + 2) by A54, XXREAL_0: 2;

          (i + 2) = 0 or ... or (i + 2) = 5 by A37, A55;

          per cases by A56;

            suppose i = 1;

            hence thesis by A35, A53, A48, Th28;

          end;

            suppose i = 2;

            hence thesis by A34, A48, A39, Th29;

          end;

            suppose i = 3;

            hence thesis by A38, A39, A47, Th30;

          end;

        end;

        thus f is circular by A37, A33, A40, FINSEQ_6:def 1;

        thus f is s.c.c.

        proof

          let i, j;

          assume that

           A57: (i + 1) < j and

           A58: i > 1 & j < ( len f) or (j + 1) < ( len f);

          (j + 1) <= 5 by A37, A58, NAT_1: 13;

          then

           A59: (j + 1) = 0 or ... or (j + 1) = 5;

          

           A60: ((i + 1) + 1) = (i + (1 + 1));

          then

           A61: (i + 2) <> ( 0 + 1);

          

           A62: (i + 2) <= j by A57, A60, NAT_1: 13;

           A63:

          now

            per cases by A57, A59, NAT_1: 11;

              case j = 2;

              then (i + 2) <= 2 by A62;

              then (i + 2) = 0 or ... or (i + 2) = 2;

              hence i = 0 by A57;

            end;

              case j = 3;

              then (i + 2) <= 3 by A62;

              then (i + 2) = 0 or ... or (i + 2) = 3;

              hence i = 0 or i = 1 by A57;

            end;

              case

               A64: j = 4;

              then (i + 2) <= 4 by A62;

              then (i + 2) = 0 or ... or (i + 2) = 4;

              hence i = 0 or i = 2 by A37, A58, A61, A64;

            end;

          end;

          per cases by A63;

            suppose i = 0 ;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

            hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

          end;

            suppose i = 1 & j = 3;

            then ( LSeg (f,i)) misses ( LSeg (f,j)) by A53, A39, Th34;

            hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

          end;

            suppose i = 2 & j = 4;

            then ( LSeg (f,i)) misses ( LSeg (f,j)) by A48, A47, Th33;

            hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

          end;

        end;

        

         A65: ( W-bound D) < ( E-bound D) by Th31;

        

         A66: ( len <*( W-bound D), ( E-bound D)*>) = 2 by FINSEQ_1: 44

        .= ( card ( rng Xf)) by A65, A10, CARD_2: 57;

        

         A67: ( len Xf1) = 3 by FINSEQ_1: 45;

        then 1 in ( dom Xf1) by FINSEQ_3: 25;

        

        then

         A68: (Xf . 1) = (Xf1 . 1) by FINSEQ_1:def 7

        .= ( W-bound D) by FINSEQ_1: 45;

        

         A69: ( len Xf2) = 2 by FINSEQ_1: 44;

        then

         A70: ( len Xf) = (3 + 2) by A67, FINSEQ_1: 22;

        2 in ( dom Xf2) by A69, FINSEQ_3: 25;

        

        then

         A71: (Xf . (3 + 2)) = (Xf2 . 2) by A67, FINSEQ_1:def 7

        .= ( W-bound D) by FINSEQ_1: 44;

        3 in ( dom Xf1) by A67, FINSEQ_3: 25;

        

        then

         A72: (Xf . 3) = (Xf1 . 3) by FINSEQ_1:def 7

        .= ( E-bound D) by FINSEQ_1: 45;

        2 in ( dom Xf1) by A67, FINSEQ_3: 25;

        

        then

         A73: (Xf . 2) = (Xf1 . 2) by FINSEQ_1:def 7

        .= ( E-bound D) by FINSEQ_1: 45;

        1 in ( dom Xf2) by A69, FINSEQ_3: 25;

        

        then

         A74: (Xf . (3 + 1)) = (Xf2 . 1) by A67, FINSEQ_1:def 7

        .= ( W-bound D) by FINSEQ_1: 44;

        now

          let n be Nat;

          assume

           A75: n in ( dom Xf);

          then

           A76: n <> 0 by FINSEQ_3: 25;

          n <= 5 by A70, A75, FINSEQ_3: 25;

          then n = 0 or ... or n = 5;

          per cases by A76;

            suppose n = 1;

            hence (Xf . n) = ((f /. n) `1 ) by A33, A68, EUCLID: 52;

          end;

            suppose n = 2;

            hence (Xf . n) = ((f /. n) `1 ) by A35, A73, EUCLID: 52;

          end;

            suppose n = 3;

            hence (Xf . n) = ((f /. n) `1 ) by A34, A72, EUCLID: 52;

          end;

            suppose n = 4;

            hence (Xf . n) = ((f /. n) `1 ) by A38, A74, EUCLID: 52;

          end;

            suppose n = 5;

            hence (Xf . n) = ((f /. n) `1 ) by A40, A71, EUCLID: 52;

          end;

        end;

        then Xf = ( X_axis f) by A37, A70, GOBOARD1:def 1;

        then

         A77: <*( W-bound D), ( E-bound D)*> = ( Incr ( X_axis f)) by A11, A66, A12, SEQ_4:def 21;

        

         A78: for n,m be Nat st [n, m] in ( Indices S) holds (S * (n,m)) = |[(( Incr ( X_axis f)) . n), (( Incr ( Y_axis f)) . m)]|

        proof

          let n,m be Nat;

          

           A79: ( <*( S-bound D), ( N-bound D)*> . 1) = ( S-bound D) by FINSEQ_1: 44;

          assume [n, m] in ( Indices S);

          then [n, m] in [: {1, 2}, {1, 2}:] by FINSEQ_1: 2, MATRIX_0: 47;

          then

           A80: [n, m] in { [1, 1], [1, 2], [2, 1], [2, 2]} by MCART_1: 23;

          

           A81: ( <*( S-bound D), ( N-bound D)*> . 2) = ( N-bound D) by FINSEQ_1: 44;

          per cases by A80, ENUMSET1:def 2;

            suppose

             A82: [n, m] = [1, 1];

            then

             A83: m = 1 by XTUPLE_0: 1;

            

             A84: n = 1 by A82, XTUPLE_0: 1;

            

            hence (S * (n,m)) = |[( W-bound D), ( S-bound D)]| by A83, MATRIX_0: 50

            .= |[(( Incr ( X_axis f)) . n), (( Incr ( Y_axis f)) . m)]| by A77, A52, A79, A84, A83, FINSEQ_1: 44;

          end;

            suppose

             A85: [n, m] = [1, 2];

            then

             A86: m = 2 by XTUPLE_0: 1;

            

             A87: n = 1 by A85, XTUPLE_0: 1;

            

            hence (S * (n,m)) = |[( W-bound D), ( N-bound D)]| by A86, MATRIX_0: 50

            .= |[(( Incr ( X_axis f)) . n), (( Incr ( Y_axis f)) . m)]| by A77, A52, A81, A87, A86, FINSEQ_1: 44;

          end;

            suppose

             A88: [n, m] = [2, 1];

            then

             A89: m = 1 by XTUPLE_0: 1;

            

             A90: n = 2 by A88, XTUPLE_0: 1;

            

            hence (S * (n,m)) = |[( E-bound D), ( S-bound D)]| by A89, MATRIX_0: 50

            .= |[(( Incr ( X_axis f)) . n), (( Incr ( Y_axis f)) . m)]| by A77, A52, A79, A90, A89, FINSEQ_1: 44;

          end;

            suppose

             A91: [n, m] = [2, 2];

            then

             A92: m = 2 by XTUPLE_0: 1;

            

             A93: n = 2 by A91, XTUPLE_0: 1;

            

            hence (S * (n,m)) = |[( E-bound D), ( N-bound D)]| by A92, MATRIX_0: 50

            .= |[(( Incr ( X_axis f)) . n), (( Incr ( Y_axis f)) . m)]| by A77, A52, A81, A93, A92, FINSEQ_1: 44;

          end;

        end;

        

         A94: ( width S) = 2 by MATRIX_0: 47

        .= ( len ( Incr ( Y_axis f))) by A52, FINSEQ_1: 44;

        ( len S) = 2 by MATRIX_0: 47

        .= ( len ( Incr ( X_axis f))) by A77, FINSEQ_1: 44;

        

        then

         A95: S = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by A94, A78, GOBOARD2:def 1

        .= ( GoB f) by GOBOARD2:def 2;

        then

         A96: (f /. 2) = (( GoB f) * (2,2)) by A35, MATRIX_0: 50;

        

         A97: (f /. 4) = (( GoB f) * (1,1)) by A38, A95, MATRIX_0: 50;

        

         A98: (f /. 3) = (( GoB f) * (2,1)) by A34, A95, MATRIX_0: 50;

        

         A99: (f /. 1) = (( GoB f) * (1,2)) by A33, A95, MATRIX_0: 50;

        thus ( SpStSeq D) is standard

        proof

          thus for k st k in ( dom f) holds ex i, j st [i, j] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i,j))

          proof

            let k;

            assume

             A100: k in ( dom f);

            then

             A101: k >= 1 by FINSEQ_3: 25;

            k <= 5 by A37, A100, FINSEQ_3: 25;

            then k = 0 or ... or k = 5;

            per cases by A101;

              suppose

               A102: k = 1;

              take 1, 2;

              thus [1, 2] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

              thus thesis by A33, A95, A102, MATRIX_0: 50;

            end;

              suppose

               A103: k = 2;

              take 2, 2;

              thus [2, 2] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

              thus thesis by A35, A95, A103, MATRIX_0: 50;

            end;

              suppose

               A104: k = 3;

              take 2, 1;

              thus [2, 1] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

              thus thesis by A34, A95, A104, MATRIX_0: 50;

            end;

              suppose

               A105: k = 4;

              take 1, 1;

              thus [1, 1] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

              thus thesis by A38, A95, A105, MATRIX_0: 50;

            end;

              suppose

               A106: k = 5;

              take 1, 2;

              thus [1, 2] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

              thus thesis by A40, A95, A106, MATRIX_0: 50;

            end;

          end;

          let n be Nat such that

           A107: n in ( dom f) and

           A108: (n + 1) in ( dom f);

          

           A109: n <> 0 by A107, FINSEQ_3: 25;

          (n + 1) <= (4 + 1) by A37, A108, FINSEQ_3: 25;

          then

           A110: n <= 4 by XREAL_1: 6;

          let m,k,i,j be Nat such that

           A111: [m, k] in ( Indices ( GoB f)) and

           A112: [i, j] in ( Indices ( GoB f)) and

           A113: (f /. n) = (( GoB f) * (m,k)) and

           A114: (f /. (n + 1)) = (( GoB f) * (i,j));

          n = 0 or ... or n = 4 by A110;

          per cases by A109;

            suppose

             A115: n = 1;

            

             A116: [2, 2] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then

             A117: i = (1 + 1) by A96, A112, A114, A115, GOBOARD1: 5;

            

             A118: [1, 2] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then m = 1 by A99, A111, A113, A115, GOBOARD1: 5;

            then

             A119: |.(m - i).| = 1 by A117, SEQM_3: 41;

            

             A120: j = 2 by A96, A112, A114, A115, A116, GOBOARD1: 5;

            k = 2 by A99, A111, A113, A115, A118, GOBOARD1: 5;

            hence ( |.(m - i).| + |.(k - j).|) = 1 by A120, A119, SEQM_3: 42;

          end;

            suppose

             A121: n = 2;

            

             A122: [2, 1] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then

             A123: j = 1 by A98, A112, A114, A121, GOBOARD1: 5;

            

             A124: [2, 2] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then k = (1 + 1) by A96, A111, A113, A121, GOBOARD1: 5;

            then

             A125: |.(k - j).| = 1 by A123, SEQM_3: 41;

            

             A126: i = 2 by A98, A112, A114, A121, A122, GOBOARD1: 5;

            m = 2 by A96, A111, A113, A121, A124, GOBOARD1: 5;

            hence ( |.(m - i).| + |.(k - j).|) = 1 by A126, A125, SEQM_3: 42;

          end;

            suppose

             A127: n = 3;

            

             A128: [1, 1] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then

             A129: i = 1 by A97, A112, A114, A127, GOBOARD1: 5;

            

             A130: [2, 1] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then m = (1 + 1) by A98, A111, A113, A127, GOBOARD1: 5;

            then

             A131: |.(m - i).| = 1 by A129, SEQM_3: 41;

            

             A132: j = 1 by A97, A112, A114, A127, A128, GOBOARD1: 5;

            k = 1 by A98, A111, A113, A127, A130, GOBOARD1: 5;

            hence ( |.(m - i).| + |.(k - j).|) = 1 by A132, A131, SEQM_3: 42;

          end;

            suppose

             A133: n = 4;

            

             A134: [1, 1] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then

             A135: k = 1 by A97, A111, A113, A133, GOBOARD1: 5;

            

             A136: [1, 2] in ( Indices ( GoB f)) by A95, MATRIX_0: 48;

            then j = (1 + 1) by A33, A40, A99, A112, A114, A133, GOBOARD1: 5;

            then

             A137: |.(k - j).| = 1 by A135, SEQM_3: 41;

            

             A138: m = 1 by A97, A111, A113, A133, A134, GOBOARD1: 5;

            i = 1 by A33, A40, A99, A112, A114, A133, A136, GOBOARD1: 5;

            hence ( |.(m - i).| + |.(k - j).|) = 1 by A138, A137, SEQM_3: 42;

          end;

        end;

      end;

    end

    theorem :: SPRECT_1:42

    

     Th42: ( L~ ( SpStSeq D)) = [.( W-bound D), ( E-bound D), ( S-bound D), ( N-bound D).]

    proof

      ( 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 thesis by SPPOL_2:def 3;

    end;

    registration

      let T be non empty TopSpace, X be non empty compact Subset of T, f be continuous RealMap of T;

      cluster (f .: X) -> bounded_below;

      coherence

      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 thesis by A1, PRE_TOPC: 8;

      end;

      cluster (f .: X) -> bounded_above;

      coherence

      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 thesis by A2, PRE_TOPC: 8;

      end;

    end

    theorem :: SPRECT_1:43

    

     Th43: ( W-bound S) = ( lower_bound ( proj1 .: S))

    proof

      

      thus ( W-bound S) = ( lower_bound ( rng ( proj1 | S))) by RELSET_1: 22

      .= ( lower_bound ( proj1 .: S)) by RELAT_1: 115;

    end;

    theorem :: SPRECT_1:44

    

     Th44: ( S-bound S) = ( lower_bound ( proj2 .: S))

    proof

      

      thus ( S-bound S) = ( lower_bound ( rng ( proj2 | S))) by RELSET_1: 22

      .= ( lower_bound ( proj2 .: S)) by RELAT_1: 115;

    end;

    theorem :: SPRECT_1:45

    

     Th45: ( N-bound S) = ( upper_bound ( proj2 .: S))

    proof

      

      thus ( N-bound S) = ( upper_bound ( rng ( proj2 | S))) by RELSET_1: 22

      .= ( upper_bound ( proj2 .: S)) by RELAT_1: 115;

    end;

    theorem :: SPRECT_1:46

    

     Th46: ( E-bound S) = ( upper_bound ( proj1 .: S))

    proof

      

      thus ( E-bound S) = ( upper_bound ( rng ( proj1 | S))) by RELSET_1: 22

      .= ( upper_bound ( proj1 .: S)) by RELAT_1: 115;

    end;

    theorem :: SPRECT_1:47

    

     Th47: S = (C1 \/ C2) implies ( W-bound S) = ( min (( W-bound C1),( W-bound C2)))

    proof

      assume

       A1: S = (C1 \/ 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;

    end;

    theorem :: SPRECT_1:48

    

     Th48: S = (C1 \/ C2) implies ( S-bound S) = ( min (( S-bound C1),( S-bound C2)))

    proof

      assume

       A1: S = (C1 \/ 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;

    end;

    theorem :: SPRECT_1:49

    

     Th49: S = (C1 \/ C2) implies ( N-bound S) = ( max (( N-bound C1),( N-bound C2)))

    proof

      assume

       A1: S = (C1 \/ 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;

    end;

    theorem :: SPRECT_1:50

    

     Th50: S = (C1 \/ C2) implies ( E-bound S) = ( max (( E-bound C1),( E-bound C2)))

    proof

      assume

       A1: S = (C1 \/ 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;

    end;

    registration

      let r1,r2 be Real;

      cluster [.r1, r2.] -> real-bounded;

      coherence

      proof

        

         A1: [.r1, r2.] is bounded_above

        proof

          take r2;

          let x be ExtReal;

          thus thesis by XXREAL_1: 1;

        end;

         [.r1, r2.] is bounded_below

        proof

          take r1;

          let x be ExtReal;

          thus thesis by XXREAL_1: 1;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: SPRECT_1:51

    

     Th51: r1 <= r2 implies (t in [.r1, r2.] iff ex s1 st 0 <= s1 & s1 <= 1 & t = ((s1 * r1) + ((1 - s1) * r2)))

    proof

      assume

       A1: r1 <= r2;

      per cases by A1, XXREAL_0: 1;

        suppose

         A2: r1 = r2;

        then

         A3: [.r1, r2.] = {r1} by XXREAL_1: 17;

        hereby

          reconsider a19 = 1 as Real;

          assume

           A4: t in [.r1, r2.];

          take s = a19;

          thus 0 <= s & s <= 1;

          thus t = ((s * r1) + ((1 - s) * r2)) by A3, A4, TARSKI:def 1;

        end;

        given s1 such that 0 <= s1 and s1 <= 1 and

         A5: t = ((s1 * r1) + ((1 - s1) * r2));

        thus thesis by A2, A3, A5, TARSKI:def 1;

      end;

        suppose

         A6: r1 < r2;

        hereby

          assume

           A7: t in [.r1, r2.];

          reconsider s1 = ((r2 - t) / (r2 - r1)) as Real;

          take s1;

          

           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;

          r1 <= t by A7, XXREAL_1: 1;

          then (r2 - t) <= (r2 - r1) by XREAL_1: 10;

          hence s1 <= 1 by A8, XREAL_1: 185;

          

          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;

        end;

        given s1 such that

         A9: 0 <= s1 and

         A10: s1 <= 1 and

         A11: t = ((s1 * r1) + ((1 - s1) * 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 thesis by A14, XXREAL_1: 1;

      end;

    end;

    theorem :: SPRECT_1:52

    

     Th52: (p `1 ) <= (q `1 ) implies ( proj1 .: ( LSeg (p,q))) = [.(p `1 ), (q `1 ).]

    proof

      assume

       A1: (p `1 ) <= (q `1 );

      for y be object holds y in [.(p `1 ), (q `1 ).] iff ex x be object st x in ( dom proj1 ) & x in ( LSeg (p,q)) & y = ( proj1 . x)

      proof

        let y be object;

        hereby

          assume

           A2: y in [.(p `1 ), (q `1 ).];

          then

          reconsider r = y as Real;

          consider t 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 = o as object;

          take x;

          o in the carrier of ( TOP-REAL 2);

          hence x in ( dom proj1 ) by FUNCT_2:def 1;

          o in ( LSeg (q,p)) by A3, A4;

          hence x in ( LSeg (p,q));

          

          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;

        end;

        given x be object such that x in ( dom proj1 ) and

         A6: x in ( LSeg (p,q)) and

         A7: y = ( proj1 . x);

        reconsider s = x as Point of ( TOP-REAL 2) by A6;

        x in ( LSeg (q,p)) by A6;

        then

        consider r be 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 thesis by A1, A9, A10, Th51;

      end;

      hence thesis by FUNCT_1:def 6;

    end;

    theorem :: SPRECT_1:53

    

     Th53: (p `2 ) <= (q `2 ) implies ( proj2 .: ( LSeg (p,q))) = [.(p `2 ), (q `2 ).]

    proof

      assume

       A1: (p `2 ) <= (q `2 );

      for y be object holds y in [.(p `2 ), (q `2 ).] iff ex x be object st x in ( dom proj2 ) & x in ( LSeg (p,q)) & y = ( proj2 . x)

      proof

        let y be object;

        hereby

          assume

           A2: y in [.(p `2 ), (q `2 ).];

          then

          reconsider r = y as Real;

          consider t 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 = o as object;

          take x;

          o in the carrier of ( TOP-REAL 2);

          hence x in ( dom proj2 ) by FUNCT_2:def 1;

          o in ( LSeg (q,p)) by A3, A4;

          hence x in ( LSeg (p,q));

          

          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;

        end;

        given x be object such that x in ( dom proj2 ) and

         A6: x in ( LSeg (p,q)) and

         A7: y = ( proj2 . x);

        reconsider s = x as Point of ( TOP-REAL 2) by A6;

        x in ( LSeg (q,p)) by A6;

        then

        consider r be 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 thesis by A1, A9, A10, Th51;

      end;

      hence thesis by FUNCT_1:def 6;

    end;

    theorem :: SPRECT_1:54

    

     Th54: (p `1 ) <= (q `1 ) implies ( W-bound ( LSeg (p,q))) = (p `1 )

    proof

      assume

       A1: (p `1 ) <= (q `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;

    end;

    theorem :: SPRECT_1:55

    

     Th55: (p `2 ) <= (q `2 ) implies ( S-bound ( LSeg (p,q))) = (p `2 )

    proof

      assume

       A1: (p `2 ) <= (q `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;

    end;

    theorem :: SPRECT_1:56

    

     Th56: (p `2 ) <= (q `2 ) implies ( N-bound ( LSeg (p,q))) = (q `2 )

    proof

      assume

       A1: (p `2 ) <= (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;

    end;

    theorem :: SPRECT_1:57

    

     Th57: (p `1 ) <= (q `1 ) implies ( E-bound ( LSeg (p,q))) = (q `1 )

    proof

      assume

       A1: (p `1 ) <= (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;

    end;

    theorem :: SPRECT_1:58

    

     Th58: ( W-bound ( L~ ( SpStSeq C))) = ( W-bound C)

    proof

      set S1 = ( LSeg (( NW-corner C),( NE-corner C))), S2 = ( LSeg (( NE-corner C),( SE-corner C))), S3 = ( LSeg (( SE-corner C),( SW-corner C))), 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: (S3 \/ S4) is compact by COMPTS_1: 10;

      

       A4: (( NE-corner C) `1 ) = ( E-bound C) by EUCLID: 52;

      then

       A5: ( W-bound S2) = ( 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 S4) = ( W-bound C) by A6, Th54;

      

       A9: ( W-bound (S3 \/ S4)) = ( min (( W-bound S3),( W-bound S4))) by Th47

      .= ( min (( W-bound C),( W-bound C))) by A1, A6, A8, Th21, Th54

      .= ( W-bound C);

      

       A10: ( L~ ( SpStSeq C)) = ((S1 \/ S2) \/ (S3 \/ S4)) by Th41;

      

       A11: (S1 \/ S2) is compact by COMPTS_1: 10;

      ( W-bound (S1 \/ S2)) = ( min (( W-bound S1),( W-bound S2))) 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);

    end;

    theorem :: SPRECT_1:59

    

     Th59: ( S-bound ( L~ ( SpStSeq C))) = ( S-bound C)

    proof

      set S1 = ( LSeg (( NW-corner C),( NE-corner C))), S2 = ( LSeg (( NE-corner C),( SE-corner C))), S3 = ( LSeg (( SE-corner C),( SW-corner C))), 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: (S3 \/ S4) is compact by COMPTS_1: 10;

      

       A4: (( NE-corner C) `2 ) = ( N-bound C) by EUCLID: 52;

      then

       A5: ( S-bound S2) = ( 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 S4) = ( S-bound C) by A6, Th22, Th55;

      

       A9: ( S-bound (S3 \/ S4)) = ( min (( S-bound S3),( S-bound S4))) by Th48

      .= ( min (( S-bound C),( S-bound C))) by A1, A6, A8, Th55

      .= ( S-bound C);

      

       A10: ( L~ ( SpStSeq C)) = ((S1 \/ S2) \/ (S3 \/ S4)) by Th41;

      

       A11: (S1 \/ S2) is compact by COMPTS_1: 10;

      ( S-bound (S1 \/ S2)) = ( min (( S-bound S1),( S-bound S2))) 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);

    end;

    theorem :: SPRECT_1:60

    

     Th60: ( N-bound ( L~ ( SpStSeq C))) = ( N-bound C)

    proof

      set S1 = ( LSeg (( NW-corner C),( NE-corner C))), S2 = ( LSeg (( NE-corner C),( SE-corner C))), S3 = ( LSeg (( SE-corner C),( SW-corner C))), 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: (S3 \/ S4) is compact by COMPTS_1: 10;

      

       A4: (( SW-corner C) `2 ) = ( S-bound C) by EUCLID: 52;

      then

       A5: ( N-bound S4) = ( 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 S2) = ( N-bound C) by A6, Th22, Th56;

      

       A9: ( N-bound (S1 \/ S2)) = ( max (( N-bound S1),( N-bound S2))) by Th49

      .= ( max (( N-bound C),( N-bound C))) by A1, A7, A8, Th56

      .= ( N-bound C);

      

       A10: ( L~ ( SpStSeq C)) = ((S1 \/ S2) \/ (S3 \/ S4)) by Th41;

      

       A11: (S1 \/ S2) is compact by COMPTS_1: 10;

      ( N-bound (S3 \/ S4)) = ( max (( N-bound S3),( N-bound S4))) 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);

    end;

    theorem :: SPRECT_1:61

    

     Th61: ( E-bound ( L~ ( SpStSeq C))) = ( E-bound C)

    proof

      set S1 = ( LSeg (( NW-corner C),( NE-corner C))), S2 = ( LSeg (( NE-corner C),( SE-corner C))), S3 = ( LSeg (( SE-corner C),( SW-corner C))), 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: (S3 \/ S4) is compact by COMPTS_1: 10;

      

       A4: (( SW-corner C) `1 ) = ( W-bound C) by EUCLID: 52;

      then

       A5: ( E-bound S4) = ( 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 S2) = ( E-bound C) by A6, Th57;

      

       A9: ( E-bound (S1 \/ S2)) = ( max (( E-bound S1),( E-bound S2))) by Th50

      .= ( max (( E-bound C),( E-bound C))) by A1, A7, A8, Th21, Th57

      .= ( E-bound C);

      

       A10: ( L~ ( SpStSeq C)) = ((S1 \/ S2) \/ (S3 \/ S4)) by Th41;

      

       A11: (S1 \/ S2) is compact by COMPTS_1: 10;

      ( E-bound (S3 \/ S4)) = ( max (( E-bound S3),( E-bound S4))) 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);

    end;

    theorem :: SPRECT_1:62

    

     Th62: ( NW-corner ( L~ ( SpStSeq C))) = ( NW-corner C)

    proof

      

      thus ( NW-corner ( L~ ( SpStSeq C))) = |[( W-bound C), ( N-bound ( L~ ( SpStSeq C)))]| by Th58

      .= ( NW-corner C) by Th60;

    end;

    theorem :: SPRECT_1:63

    

     Th63: ( NE-corner ( L~ ( SpStSeq C))) = ( NE-corner C)

    proof

      

      thus ( NE-corner ( L~ ( SpStSeq C))) = |[( E-bound C), ( N-bound ( L~ ( SpStSeq C)))]| by Th61

      .= ( NE-corner C) by Th60;

    end;

    theorem :: SPRECT_1:64

    

     Th64: ( SW-corner ( L~ ( SpStSeq C))) = ( SW-corner C)

    proof

      

      thus ( SW-corner ( L~ ( SpStSeq C))) = |[( W-bound C), ( S-bound ( L~ ( SpStSeq C)))]| by Th58

      .= ( SW-corner C) by Th59;

    end;

    theorem :: SPRECT_1:65

    

     Th65: ( SE-corner ( L~ ( SpStSeq C))) = ( SE-corner C)

    proof

      

      thus ( SE-corner ( L~ ( SpStSeq C))) = |[( E-bound C), ( S-bound ( L~ ( SpStSeq C)))]| by Th61

      .= ( SE-corner C) by Th59;

    end;

    theorem :: SPRECT_1:66

    

     Th66: ( W-most ( L~ ( SpStSeq C))) = ( LSeg (( SW-corner C),( NW-corner C)))

    proof

      set X = ( L~ ( SpStSeq C));

      set S3 = ( LSeg (( SE-corner C),( SW-corner C))), S4 = ( LSeg (( SW-corner C),( NW-corner C)));

      

       A1: S4 c= (S3 \/ S4) by XBOOLE_1: 7;

      X = ((( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) \/ (S3 \/ S4)) by Th41;

      then

       A2: (S3 \/ S4) c= X by XBOOLE_1: 7;

      ( LSeg (( SW-corner X),( NW-corner X))) = ( LSeg (( SW-corner X),( NW-corner C))) by Th62

      .= ( LSeg (( SW-corner C),( NW-corner C))) by Th64;

      hence thesis by A1, A2, XBOOLE_1: 1, XBOOLE_1: 28;

    end;

    theorem :: SPRECT_1:67

    

     Th67: ( N-most ( L~ ( SpStSeq C))) = ( LSeg (( NW-corner C),( NE-corner C)))

    proof

      set X = ( L~ ( SpStSeq C));

      set S1 = ( LSeg (( NW-corner C),( NE-corner C))), S2 = ( LSeg (( NE-corner C),( SE-corner C)));

      

       A1: S1 c= (S1 \/ S2) by XBOOLE_1: 7;

      X = ((S1 \/ S2) \/ (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C))))) by Th41;

      then

       A2: (S1 \/ S2) c= X by XBOOLE_1: 7;

      ( LSeg (( NW-corner X),( NE-corner X))) = ( LSeg (( NW-corner X),( NE-corner C))) by Th63

      .= ( LSeg (( NW-corner C),( NE-corner C))) by Th62;

      hence thesis by A1, A2, XBOOLE_1: 1, XBOOLE_1: 28;

    end;

    theorem :: SPRECT_1:68

    

     Th68: ( S-most ( L~ ( SpStSeq C))) = ( LSeg (( SW-corner C),( SE-corner C)))

    proof

      set X = ( L~ ( SpStSeq C));

      set S3 = ( LSeg (( SE-corner C),( SW-corner C))), S4 = ( LSeg (( SW-corner C),( NW-corner C)));

      

       A1: S3 c= (S3 \/ S4) by XBOOLE_1: 7;

      X = ((( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) \/ (S3 \/ S4)) by Th41;

      then

       A2: (S3 \/ S4) c= X by XBOOLE_1: 7;

      ( LSeg (( SW-corner X),( SE-corner X))) = ( LSeg (( SW-corner X),( SE-corner C))) by Th65

      .= ( LSeg (( SW-corner C),( SE-corner C))) by Th64;

      hence thesis by A1, A2, XBOOLE_1: 1, XBOOLE_1: 28;

    end;

    theorem :: SPRECT_1:69

    

     Th69: ( E-most ( L~ ( SpStSeq C))) = ( LSeg (( SE-corner C),( NE-corner C)))

    proof

      set X = ( L~ ( SpStSeq C));

      set S1 = ( LSeg (( NW-corner C),( NE-corner C))), S2 = ( LSeg (( NE-corner C),( SE-corner C)));

      

       A1: S2 c= (S1 \/ S2) by XBOOLE_1: 7;

      X = ((S1 \/ S2) \/ (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C))))) by Th41;

      then

       A2: (S1 \/ S2) c= X by XBOOLE_1: 7;

      ( LSeg (( SE-corner X),( NE-corner X))) = ( LSeg (( SE-corner X),( NE-corner C))) by Th63

      .= ( LSeg (( SE-corner C),( NE-corner C))) by Th65;

      hence thesis by A1, A2, XBOOLE_1: 1, XBOOLE_1: 28;

    end;

    theorem :: SPRECT_1:70

    

     Th70: ( proj2 .: ( LSeg (( SW-corner C),( NW-corner C)))) = [.( S-bound C), ( N-bound C).]

    proof

      

       A1: (( NW-corner C) `2 ) = ( N-bound C) by EUCLID: 52;

      (( SW-corner C) `2 ) = ( S-bound C) by EUCLID: 52;

      hence thesis by A1, Th22, Th53;

    end;

    theorem :: SPRECT_1:71

    

     Th71: ( proj1 .: ( LSeg (( NW-corner C),( NE-corner C)))) = [.( W-bound C), ( E-bound C).]

    proof

      

       A1: (( NE-corner C) `1 ) = ( E-bound C) by EUCLID: 52;

      (( NW-corner C) `1 ) = ( W-bound C) by EUCLID: 52;

      hence thesis by A1, Th21, Th52;

    end;

    theorem :: SPRECT_1:72

    

     Th72: ( proj2 .: ( LSeg (( NE-corner C),( SE-corner C)))) = [.( S-bound C), ( N-bound C).]

    proof

      

       A1: (( SE-corner C) `2 ) = ( S-bound C) by EUCLID: 52;

      (( NE-corner C) `2 ) = ( N-bound C) by EUCLID: 52;

      hence thesis by A1, Th22, Th53;

    end;

    theorem :: SPRECT_1:73

    

     Th73: ( proj1 .: ( LSeg (( SE-corner C),( SW-corner C)))) = [.( W-bound C), ( E-bound C).]

    proof

      

       A1: (( SW-corner C) `1 ) = ( W-bound C) by EUCLID: 52;

      (( SE-corner C) `1 ) = ( E-bound C) by EUCLID: 52;

      hence thesis by A1, Th21, Th52;

    end;

    theorem :: SPRECT_1:74

    

     Th74: ( W-min ( L~ ( SpStSeq C))) = ( SW-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( W-most X);

      

       A1: S = ( LSeg (( SW-corner C),( NW-corner C))) by Th66;

      

       A2: ( S-bound C) <= ( N-bound C) by Th22;

      ( lower_bound ( proj2 | S)) = ( lower_bound ( rng ( proj2 | S))) by RELSET_1: 22

      .= ( lower_bound ( proj2 .: S)) by RELAT_1: 115

      .= ( lower_bound [.( S-bound C), ( N-bound C).]) by A1, Th70

      .= ( S-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th58;

    end;

    theorem :: SPRECT_1:75

    

     Th75: ( W-max ( L~ ( SpStSeq C))) = ( NW-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( W-most X);

      

       A1: S = ( LSeg (( SW-corner C),( NW-corner C))) by Th66;

      

       A2: ( S-bound C) <= ( N-bound C) by Th22;

      ( upper_bound ( proj2 | S)) = ( upper_bound ( rng ( proj2 | S))) by RELSET_1: 22

      .= ( upper_bound ( proj2 .: S)) by RELAT_1: 115

      .= ( upper_bound [.( S-bound C), ( N-bound C).]) by A1, Th70

      .= ( N-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th58;

    end;

    theorem :: SPRECT_1:76

    

     Th76: ( N-min ( L~ ( SpStSeq C))) = ( NW-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( N-most X);

      

       A1: S = ( LSeg (( NW-corner C),( NE-corner C))) by Th67;

      

       A2: ( W-bound C) <= ( E-bound C) by Th21;

      ( lower_bound ( proj1 | S)) = ( lower_bound ( rng ( proj1 | S))) by RELSET_1: 22

      .= ( lower_bound ( proj1 .: S)) by RELAT_1: 115

      .= ( lower_bound [.( W-bound C), ( E-bound C).]) by A1, Th71

      .= ( W-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th60;

    end;

    theorem :: SPRECT_1:77

    

     Th77: ( N-max ( L~ ( SpStSeq C))) = ( NE-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( N-most X);

      

       A1: S = ( LSeg (( NW-corner C),( NE-corner C))) by Th67;

      

       A2: ( W-bound C) <= ( E-bound C) by Th21;

      ( upper_bound ( proj1 | S)) = ( upper_bound ( rng ( proj1 | S))) by RELSET_1: 22

      .= ( upper_bound ( proj1 .: S)) by RELAT_1: 115

      .= ( upper_bound [.( W-bound C), ( E-bound C).]) by A1, Th71

      .= ( E-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th60;

    end;

    theorem :: SPRECT_1:78

    

     Th78: ( E-min ( L~ ( SpStSeq C))) = ( SE-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( E-most X);

      

       A1: S = ( LSeg (( SE-corner C),( NE-corner C))) by Th69;

      

       A2: ( S-bound C) <= ( N-bound C) by Th22;

      ( lower_bound ( proj2 | S)) = ( lower_bound ( rng ( proj2 | S))) by RELSET_1: 22

      .= ( lower_bound ( proj2 .: S)) by RELAT_1: 115

      .= ( lower_bound [.( S-bound C), ( N-bound C).]) by A1, Th72

      .= ( S-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th61;

    end;

    theorem :: SPRECT_1:79

    

     Th79: ( E-max ( L~ ( SpStSeq C))) = ( NE-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( E-most X);

      

       A1: S = ( LSeg (( SE-corner C),( NE-corner C))) by Th69;

      

       A2: ( S-bound C) <= ( N-bound C) by Th22;

      ( upper_bound ( proj2 | S)) = ( upper_bound ( rng ( proj2 | S))) by RELSET_1: 22

      .= ( upper_bound ( proj2 .: S)) by RELAT_1: 115

      .= ( upper_bound [.( S-bound C), ( N-bound C).]) by A1, Th72

      .= ( N-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th61;

    end;

    theorem :: SPRECT_1:80

    

     Th80: ( S-min ( L~ ( SpStSeq C))) = ( SW-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( S-most X);

      

       A1: S = ( LSeg (( SW-corner C),( SE-corner C))) by Th68;

      

       A2: ( W-bound C) <= ( E-bound C) by Th21;

      ( lower_bound ( proj1 | S)) = ( lower_bound ( rng ( proj1 | S))) by RELSET_1: 22

      .= ( lower_bound ( proj1 .: S)) by RELAT_1: 115

      .= ( lower_bound [.( W-bound C), ( E-bound C).]) by A1, Th73

      .= ( W-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th59;

    end;

    theorem :: SPRECT_1:81

    

     Th81: ( S-max ( L~ ( SpStSeq C))) = ( SE-corner C)

    proof

      set X = ( L~ ( SpStSeq C)), S = ( S-most X);

      

       A1: S = ( LSeg (( SW-corner C),( SE-corner C))) by Th68;

      

       A2: ( W-bound C) <= ( E-bound C) by Th21;

      ( upper_bound ( proj1 | S)) = ( upper_bound ( rng ( proj1 | S))) by RELSET_1: 22

      .= ( upper_bound ( proj1 .: S)) by RELAT_1: 115

      .= ( upper_bound [.( W-bound C), ( E-bound C).]) by A1, Th73

      .= ( E-bound C) by A2, JORDAN5A: 19;

      hence thesis by Th59;

    end;

    begin

    definition

      let f be FinSequence of ( TOP-REAL 2);

      :: SPRECT_1:def2

      attr f is rectangular means

      : Def2: ex D st f = ( SpStSeq D);

    end

    registration

      let D;

      cluster ( SpStSeq D) -> rectangular;

      coherence ;

    end

    registration

      cluster rectangular for FinSequence of ( TOP-REAL 2);

      existence

      proof

        set D = the non vertical non horizontal non empty compact Subset of ( TOP-REAL 2);

        take ( SpStSeq D), D;

        thus thesis;

      end;

    end

    reserve s for rectangular FinSequence of ( TOP-REAL 2);

    theorem :: SPRECT_1:82

    ( len s) = 5

    proof

      ex D st s = ( SpStSeq D) by Def2;

      hence thesis by Th40;

    end;

    registration

      cluster rectangular -> non constant for FinSequence of ( TOP-REAL 2);

      coherence ;

    end

    registration

      cluster rectangular -> standard special unfolded circular s.c.c. for non empty FinSequence of ( TOP-REAL 2);

      coherence ;

    end

    theorem :: SPRECT_1:83

    (s /. 1) = ( N-min ( L~ s)) & (s /. 1) = ( W-max ( L~ s))

    proof

      consider D 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;

      thus thesis by A1, A2, Th75;

    end;

    theorem :: SPRECT_1:84

    (s /. 2) = ( N-max ( L~ s)) & (s /. 2) = ( E-max ( L~ s))

    proof

      consider D 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;

      thus thesis by A1, A2, Th79;

    end;

    theorem :: SPRECT_1:85

    (s /. 3) = ( S-max ( L~ s)) & (s /. 3) = ( E-min ( L~ s))

    proof

      consider D 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;

      thus thesis by A1, A2, Th78;

    end;

    theorem :: SPRECT_1:86

    (s /. 4) = ( S-min ( L~ s)) & (s /. 4) = ( W-min ( L~ s))

    proof

      consider D 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;

      thus thesis by A1, A2, Th74;

    end;

    begin

    theorem :: SPRECT_1:87

    

     Th87: r1 < r2 & s1 < s2 implies [.r1, r2, s1, s2.] is Jordan

    proof

      assume that

       A1: r1 < r2 and

       A2: s1 < s2;

       [.r1, r2, s1, s2.] = { p : (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 thesis by A1, A2, JORDAN1: 43;

    end;

    registration

      let f be rectangular FinSequence of ( TOP-REAL 2);

      cluster ( L~ f) -> Jordan;

      coherence

      proof

        consider D 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 thesis by A2, A3, Th87;

      end;

    end

    definition

      let S be Subset of ( TOP-REAL 2);

      :: original: Jordan

      redefine

      :: SPRECT_1:def3

      attr S is Jordan means

      : Def3: (S ` ) <> {} & ex A1,A2 be 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

      proof

        hereby

          assume

           A1: S is Jordan;

          hence (S ` ) <> {} ;

          consider A1,A2 be 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 be Subset of (( TOP-REAL 2) | (S ` )) st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component by A1;

          

           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, A2;

          thus (S ` ) = (A1 \/ A2) by A2;

          thus A1 misses A2 by A3;

          thus (( Cl A1) \ A1) = (( Cl A2) \ A2) by A4;

          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;

        end;

        assume

         A8: (S ` ) <> {} ;

        given A1,A2 be 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 ` );

        reconsider a1 = A1, a2 = A2 as Subset of ( TOP-REAL 2);

        

         A14: ex B be Subset of (( TOP-REAL 2) | (S ` )) st B = a2 & B is a_component by A13, CONNSP_1:def 6;

        thus (S ` ) <> {} by A8;

        take a1, a2;

        thus (S ` ) = (a1 \/ a2) by A9;

        thus (a1 /\ a2) = {} by A10;

        thus (( Cl a1) \ a1) = (( Cl a2) \ a2) by A11;

        ex B be Subset of (( TOP-REAL 2) | (S ` )) st B = a1 & B is a_component by A12, CONNSP_1:def 6;

        hence thesis by A14;

      end;

    end

    theorem :: SPRECT_1:88

    

     Th88: for f be rectangular FinSequence of ( TOP-REAL 2) holds ( LeftComp f) misses ( RightComp f)

    proof

      let f be rectangular FinSequence of ( TOP-REAL 2);

      

       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 be 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 thesis by A5;

    end;

    registration

      let f be non constant standard special_circular_sequence;

      cluster ( LeftComp f) -> non empty;

      coherence

      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 thesis by A1, GOBOARD9: 15, XBOOLE_1: 3;

      end;

      cluster ( RightComp f) -> non empty;

      coherence

      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 thesis by A2, GOBOARD9: 16, XBOOLE_1: 3;

      end;

    end

    theorem :: SPRECT_1:89

    for f be rectangular FinSequence of ( TOP-REAL 2) holds ( LeftComp f) <> ( RightComp f)

    proof

      let f be rectangular FinSequence of ( TOP-REAL 2);

      ( LeftComp f) misses ( RightComp f) by Th88;

      hence thesis;

    end;