borsuk_1.miz



    begin

    reserve e,u for set;

    theorem :: BORSUK_1:1

    

     Th1: for X be TopStruct, Y be SubSpace of X holds the carrier of Y c= the carrier of X

    proof

      let X be TopStruct, Y be SubSpace of X;

      the carrier of Y = ( [#] Y) & the carrier of X = ( [#] X);

      hence thesis by PRE_TOPC:def 4;

    end;

    definition

      let X,Y be non empty TopSpace, F be Function of X, Y;

      :: original: continuous

      redefine

      :: BORSUK_1:def1

      attr F is continuous means for W be Point of X, G be a_neighborhood of (F . W) holds ex H be a_neighborhood of W st (F .: H) c= G;

      compatibility

      proof

        

         A1: ( [#] Y) <> {} ;

        thus F is continuous implies for W be Point of X, G be a_neighborhood of (F . W) holds ex H be a_neighborhood of W st (F .: H) c= G

        proof

          assume

           A2: F is continuous;

          let W be Point of X, G be a_neighborhood of (F . W);

          (F . W) in ( Int G) by CONNSP_2:def 1;

          then

           A3: W in (F " ( Int G)) by FUNCT_2: 38;

          (F " ( Int G)) is open by A1, A2, TOPS_2: 43;

          then W in ( Int (F " ( Int G))) by A3, TOPS_1: 23;

          then

          reconsider H = (F " ( Int G)) as a_neighborhood of W by CONNSP_2:def 1;

          take H;

          H c= (F " G) by RELAT_1: 143, TOPS_1: 16;

          hence thesis by EQREL_1: 46;

        end;

        assume

         A4: for W be Point of X, G be a_neighborhood of (F . W) holds ex H be a_neighborhood of W st (F .: H) c= G;

        now

          let P1 be Subset of Y such that

           A5: P1 is open;

          now

            let x be set;

            thus x in (F " P1) implies ex P be Subset of X st P is open & P c= (F " P1) & x in P

            proof

              assume

               A6: x in (F " P1);

              then

              reconsider W = x as Point of X;

              

               A7: ( Int P1) = P1 by A5, TOPS_1: 23;

              (F . W) in P1 by A6, FUNCT_2: 38;

              then P1 is a_neighborhood of (F . W) by A7, CONNSP_2:def 1;

              then

              consider H be a_neighborhood of W such that

               A8: (F .: H) c= P1 by A4;

              take ( Int H);

              thus ( Int H) is open;

              

               A9: ( Int H) c= H by TOPS_1: 16;

              ( dom F) = the carrier of X by FUNCT_2:def 1;

              then

               A10: H c= (F " (F .: H)) by FUNCT_1: 76;

              (F " (F .: H)) c= (F " P1) by A8, RELAT_1: 143;

              then H c= (F " P1) by A10;

              hence ( Int H) c= (F " P1) by A9;

              thus thesis by CONNSP_2:def 1;

            end;

            thus (ex P be Subset of X st P is open & P c= (F " P1) & x in P) implies x in (F " P1);

          end;

          hence (F " P1) is open by TOPS_1: 25;

        end;

        hence thesis by A1, TOPS_2: 43;

      end;

    end

    reserve X,Y for non empty TopSpace;

    registration

      let X,Y,Z be non empty TopSpace, F be continuous Function of X, Y, G be continuous Function of Y, Z;

      cluster (G * F) -> continuous;

      coherence by TOPS_2: 46;

    end

    theorem :: BORSUK_1:2

    

     Th2: for A be continuous Function of X, Y, G be Subset of Y holds (A " ( Int G)) c= ( Int (A " G))

    proof

      let A be continuous Function of X, Y, G be Subset of Y;

      let e be object;

      

       A1: (A " ( Int G)) c= (A " G) by RELAT_1: 143, TOPS_1: 16;

      ( [#] Y) <> {} ;

      then

       A2: (A " ( Int G)) is open by TOPS_2: 43;

      assume e in (A " ( Int G));

      hence thesis by A2, A1, TOPS_1: 22;

    end;

    theorem :: BORSUK_1:3

    

     Th3: for W be Point of Y, A be continuous Function of X, Y, G be a_neighborhood of W holds (A " G) is a_neighborhood of (A " {W})

    proof

      let W be Point of Y, A be continuous Function of X, Y, G be a_neighborhood of W;

      W in ( Int G) by CONNSP_2:def 1;

      then {W} c= ( Int G) by ZFMISC_1: 31;

      then

       A1: (A " {W}) c= (A " ( Int G)) by RELAT_1: 143;

      (A " ( Int G)) c= ( Int (A " G)) by Th2;

      hence (A " {W}) c= ( Int (A " G)) by A1;

    end;

    definition

      let X,Y be non empty TopSpace, W be Point of Y, A be continuous Function of X, Y, G be a_neighborhood of W;

      :: original: "

      redefine

      func A " G -> a_neighborhood of (A " {W}) ;

      correctness by Th3;

    end

    theorem :: BORSUK_1:4

    

     Th4: for X be non empty TopSpace, A,B be Subset of X, U be a_neighborhood of B st A c= B holds U is a_neighborhood of A

    proof

      let X be non empty TopSpace;

      let A,B be Subset of X, U be a_neighborhood of B such that

       A1: A c= B;

      B c= ( Int U) by CONNSP_2:def 2;

      hence A c= ( Int U) by A1;

    end;

    registration

      let X be non empty TopSpace, x be Point of X;

      cluster {x} -> compact;

      coherence

      proof

        reconsider B = {x} as Subset of X;

        now

          let F be Subset-Family of X such that

           A1: F is Cover of B and F is open;

          B c= ( union F) by A1, SETFAM_1:def 11;

          then x in ( union F) by ZFMISC_1: 31;

          then

          consider A be set such that

           A2: x in A and

           A3: A in F by TARSKI:def 4;

          reconsider G = {A} as Subset-Family of X by A3, ZFMISC_1: 31;

          take G;

          thus G c= F by A3, ZFMISC_1: 31;

          x in ( union G) by A2;

          then B c= ( union G) by ZFMISC_1: 31;

          hence G is Cover of B by SETFAM_1:def 11;

          thus G is finite;

        end;

        hence thesis by COMPTS_1:def 4;

      end;

    end

    begin

    definition

      let X,Y be TopSpace;

      :: BORSUK_1:def2

      func [:X,Y:] -> strict TopSpace means

      : Def2: the carrier of it = [:the carrier of X, the carrier of Y:] & the topology of it = { ( union A) where A be Subset-Family of it : A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } };

      existence

      proof

        set t = { ( union A) where A be Subset-Family of [:the carrier of X, the carrier of Y:] : A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } };

        t c= ( bool [:the carrier of X, the carrier of Y:])

        proof

          let e be object;

          assume e in t;

          then ex A be Subset-Family of [:the carrier of X, the carrier of Y:] st e = ( union A) & A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y };

          hence thesis;

        end;

        then

        reconsider t as Subset-Family of [:the carrier of X, the carrier of Y:];

        set T = TopStruct (# [:the carrier of X, the carrier of Y:], t #);

        now

          reconsider A = { [:the carrier of X, the carrier of Y:]} as Subset-Family of [:the carrier of X, the carrier of Y:] by ZFMISC_1: 68;

          reconsider A as Subset-Family of [:the carrier of X, the carrier of Y:];

          

           A1: A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y }

          proof

            let e be object;

            assume e in A;

            then

             A2: e = [:the carrier of X, the carrier of Y:] by TARSKI:def 1;

            the carrier of X in the topology of X & the carrier of Y in the topology of Y by PRE_TOPC:def 1;

            hence thesis by A2;

          end;

          the carrier of T = ( union A);

          hence the carrier of T in the topology of T by A1;

          thus for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T

          proof

            let a be Subset-Family of T;

            set A = { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y & ex x be set st x in a & [:X1, Y1:] c= x };

            A c= ( bool [:the carrier of X, the carrier of Y:])

            proof

              let e be object;

              assume e in A;

              then ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x be set st x in a & [:X1, Y1:] c= x;

              hence thesis;

            end;

            then

            reconsider A as Subset-Family of [:the carrier of X, the carrier of Y:];

            assume

             A3: a c= the topology of T;

            

             A4: ( union A) = ( union a)

            proof

              thus ( union A) c= ( union a)

              proof

                let e1,e2 be object;

                assume [e1, e2] in ( union A);

                then

                consider u such that

                 A5: [e1, e2] in u and

                 A6: u in A by TARSKI:def 4;

                ex X1 be Subset of X, Y1 be Subset of Y st u = [:X1, Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x be set st x in a & [:X1, Y1:] c= x by A6;

                hence thesis by A5, TARSKI:def 4;

              end;

              let e be object;

              assume e in ( union a);

              then

              consider u such that

               A7: e in u and

               A8: u in a by TARSKI:def 4;

              u in the topology of T by A3, A8;

              then

              consider B be Subset-Family of [:the carrier of X, the carrier of Y:] such that

               A9: u = ( union B) and

               A10: B c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y };

              consider x be set such that

               A11: e in x and

               A12: x in B by A7, A9, TARSKI:def 4;

              x in { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } by A10, A12;

              then

              consider X1 be Subset of X, Y1 be Subset of Y such that

               A13: x = [:X1, Y1:] and

               A14: X1 in the topology of X & Y1 in the topology of Y;

               [:X1, Y1:] c= u by A9, A12, A13, ZFMISC_1: 74;

              then x in A by A8, A13, A14;

              hence thesis by A11, TARSKI:def 4;

            end;

            A c= { [:X2, Y2:] where X2 be Subset of X, Y2 be Subset of Y : X2 in the topology of X & Y2 in the topology of Y }

            proof

              let e be object;

              assume e in A;

              then ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x be set st x in a & [:X1, Y1:] c= x;

              hence thesis;

            end;

            hence thesis by A4;

          end;

          let a,b be Subset of T;

          set C = { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y & [:X1, Y1:] c= (a /\ b) };

          C c= ( bool [:the carrier of X, the carrier of Y:])

          proof

            let e be object;

            assume e in C;

            then ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1, Y1:] c= (a /\ b);

            hence thesis;

          end;

          then

          reconsider C as Subset-Family of [:the carrier of X, the carrier of Y:];

          assume that

           A15: a in the topology of T and

           A16: b in the topology of T;

          consider A be Subset-Family of [:the carrier of X, the carrier of Y:] such that

           A17: a = ( union A) and

           A18: A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } by A15;

          consider B be Subset-Family of [:the carrier of X, the carrier of Y:] such that

           A19: b = ( union B) and

           A20: B c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } by A16;

          

           A21: (a /\ b) = ( union C)

          proof

            thus (a /\ b) c= ( union C)

            proof

              let e be object;

              assume

               A22: e in (a /\ b);

              then e in a by XBOOLE_0:def 4;

              then

              consider u1 be set such that

               A23: e in u1 and

               A24: u1 in A by A17, TARSKI:def 4;

              

               A25: u1 in { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } by A18, A24;

              e in b by A22, XBOOLE_0:def 4;

              then

              consider u2 be set such that

               A26: e in u2 and

               A27: u2 in B by A19, TARSKI:def 4;

              

               A28: u2 in { [:X2, Y2:] where X2 be Subset of X, Y2 be Subset of Y : X2 in the topology of X & Y2 in the topology of Y } by A20, A27;

              

               A29: u2 c= b by A19, A27, ZFMISC_1: 74;

              consider X1 be Subset of X, Y1 be Subset of Y such that

               A30: u1 = [:X1, Y1:] and

               A31: X1 in the topology of X & Y1 in the topology of Y by A25;

              consider X2 be Subset of X, Y2 be Subset of Y such that

               A32: u2 = [:X2, Y2:] and

               A33: X2 in the topology of X & Y2 in the topology of Y by A28;

              u1 c= a by A17, A24, ZFMISC_1: 74;

              then ( [:X1, Y1:] /\ [:X2, Y2:]) c= (a /\ b) by A30, A32, A29, XBOOLE_1: 27;

              then

               A34: [:(X1 /\ X2), (Y1 /\ Y2):] c= (a /\ b) by ZFMISC_1: 100;

              (X1 /\ X2) in the topology of X & (Y1 /\ Y2) in the topology of Y by A31, A33, PRE_TOPC:def 1;

              then

               A35: [:(X1 /\ X2), (Y1 /\ Y2):] in C by A34;

              e in [:(X1 /\ X2), (Y1 /\ Y2):] by A23, A26, A30, A32, ZFMISC_1: 113;

              hence thesis by A35, TARSKI:def 4;

            end;

            let e1,e2 be object;

            assume [e1, e2] in ( union C);

            then

            consider u such that

             A36: [e1, e2] in u and

             A37: u in C by TARSKI:def 4;

            ex X1 be Subset of X, Y1 be Subset of Y st u = [:X1, Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1, Y1:] c= (a /\ b) by A37;

            hence thesis by A36;

          end;

          C c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y }

          proof

            let e be object;

            assume e in C;

            then ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1, Y1:] c= (a /\ b);

            hence thesis;

          end;

          hence (a /\ b) in the topology of T by A21;

        end;

        then

        reconsider T as strict TopSpace by PRE_TOPC:def 1;

        take T;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let T1 be TopSpace, T2 be empty TopSpace;

      cluster [:T1, T2:] -> empty;

      coherence

      proof

        the carrier of [:T1, T2:] = [:the carrier of T1, the carrier of T2:] by Def2;

        hence thesis;

      end;

      cluster [:T2, T1:] -> empty;

      coherence

      proof

        the carrier of [:T2, T1:] = [:the carrier of T2, the carrier of T1:] by Def2;

        hence thesis;

      end;

    end

    registration

      let X,Y be non empty TopSpace;

      cluster [:X, Y:] -> non empty;

      coherence

      proof

        the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

        hence the carrier of [:X, Y:] is non empty;

      end;

    end

    theorem :: BORSUK_1:5

    

     Th5: for X,Y be TopSpace holds for B be Subset of [:X, Y:] holds B is open iff ex A be Subset-Family of [:X, Y:] st B = ( union A) & for e st e in A holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open

    proof

      let X,Y be TopSpace;

      let B be Subset of [:X, Y:];

      

       A1: the topology of [:X, Y:] = { ( union A) where A be Subset-Family of [:X, Y:] : A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } } by Def2;

      thus B is open implies ex A be Subset-Family of [:X, Y:] st B = ( union A) & for e st e in A holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open

      proof

        assume B in the topology of [:X, Y:];

        then

        consider A be Subset-Family of [:X, Y:] such that

         A2: B = ( union A) and

         A3: A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } by A1;

        take A;

        thus B = ( union A) by A2;

        let e;

        assume e in A;

        then e in { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y } by A3;

        then

        consider X1 be Subset of X, Y1 be Subset of Y such that

         A4: e = [:X1, Y1:] & X1 in the topology of X & Y1 in the topology of Y;

        reconsider Y1 as Subset of Y;

        reconsider X1 as Subset of X;

        take X1, Y1;

        thus thesis by A4;

      end;

      given A be Subset-Family of [:X, Y:] such that

       A5: B = ( union A) and

       A6: for e st e in A holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open;

      A c= { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : X1 in the topology of X & Y1 in the topology of Y }

      proof

        let e be object;

        assume e in A;

        then

        consider X1 be Subset of X, Y1 be Subset of Y such that

         A7: e = [:X1, Y1:] and

         A8: X1 is open & Y1 is open by A6;

        X1 in the topology of X & Y1 in the topology of Y by A8;

        hence thesis by A7;

      end;

      hence B in the topology of [:X, Y:] by A1, A5;

    end;

    definition

      let X,Y be TopSpace, A be Subset of X, B be Subset of Y;

      :: original: [:

      redefine

      func [:A,B:] -> Subset of [:X, Y:] ;

      correctness

      proof

        thus [:A, B:] is Subset of [:X, Y:] by Def2;

      end;

    end

    definition

      let X,Y be non empty TopSpace, x be Point of X, y be Point of Y;

      :: original: [

      redefine

      func [x,y] -> Point of [:X, Y:] ;

      correctness

      proof

        thus [x, y] is Point of [:X, Y:] by Def2;

      end;

    end

    theorem :: BORSUK_1:6

    

     Th6: for X,Y be TopSpace holds for V be Subset of X, W be Subset of Y st V is open & W is open holds [:V, W:] is open

    proof

      let X,Y be TopSpace, V be Subset of X, W be Subset of Y such that

       A1: V is open & W is open;

      reconsider PP = { [:V, W:]} as Subset-Family of [:X, Y:];

      reconsider PP as Subset-Family of [:X, Y:];

       A2:

      now

        let e;

        assume

         A3: e in PP;

        take V, W;

        thus e = [:V, W:] & V is open & W is open by A1, A3, TARSKI:def 1;

      end;

       [:V, W:] = ( union { [:V, W:]});

      hence thesis by A2, Th5;

    end;

    theorem :: BORSUK_1:7

    

     Th7: for X,Y be TopSpace holds for V be Subset of X, W be Subset of Y holds ( Int [:V, W:]) = [:( Int V), ( Int W):]

    proof

      let X,Y be TopSpace, V be Subset of X, W be Subset of Y;

      thus ( Int [:V, W:]) c= [:( Int V), ( Int W):]

      proof

        let e be object;

        assume e in ( Int [:V, W:]);

        then

        consider Q be Subset of [:X, Y:] such that

         A1: Q is open and

         A2: Q c= [:V, W:] and

         A3: e in Q by TOPS_1: 22;

        consider A be Subset-Family of [:X, Y:] such that

         A4: Q = ( union A) and

         A5: for e st e in A holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open by A1, Th5;

        consider a be set such that

         A6: e in a and

         A7: a in A by A3, A4, TARSKI:def 4;

        consider X1 be Subset of X, Y1 be Subset of Y such that

         A8: a = [:X1, Y1:] and

         A9: X1 is open and

         A10: Y1 is open by A5, A7;

         [:X1, Y1:] c= Q by A4, A7, A8, ZFMISC_1: 74;

        then

         A11: [:X1, Y1:] c= [:V, W:] by A2;

        then Y1 c= W by A6, A8, ZFMISC_1: 114;

        then

         A12: Y1 c= ( Int W) by A10, TOPS_1: 24;

        X1 c= V by A6, A8, A11, ZFMISC_1: 114;

        then X1 c= ( Int V) by A9, TOPS_1: 24;

        then [:X1, Y1:] c= [:( Int V), ( Int W):] by A12, ZFMISC_1: 96;

        hence thesis by A6, A8;

      end;

      ( Int V) c= V & ( Int W) c= W by TOPS_1: 16;

      then [:( Int V), ( Int W):] c= [:V, W:] by ZFMISC_1: 96;

      hence thesis by Th6, TOPS_1: 24;

    end;

    theorem :: BORSUK_1:8

    

     Th8: for x be Point of X, y be Point of Y, V be a_neighborhood of x, W be a_neighborhood of y holds [:V, W:] is a_neighborhood of [x, y]

    proof

      let x be Point of X, y be Point of Y, V be a_neighborhood of x, W be a_neighborhood of y;

      x in ( Int V) & y in ( Int W) by CONNSP_2:def 1;

      then [x, y] in [:( Int V), ( Int W):] by ZFMISC_1: 87;

      hence [x, y] in ( Int [:V, W:]) by Th7;

    end;

    theorem :: BORSUK_1:9

    

     Th9: for A be Subset of X, B be Subset of Y, V be a_neighborhood of A, W be a_neighborhood of B holds [:V, W:] is a_neighborhood of [:A, B:]

    proof

      let A be Subset of X, B be Subset of Y, V be a_neighborhood of A, W be a_neighborhood of B;

      A c= ( Int V) & B c= ( Int W) by CONNSP_2:def 2;

      then [:A, B:] c= [:( Int V), ( Int W):] by ZFMISC_1: 96;

      hence [:A, B:] c= ( Int [:V, W:]) by Th7;

    end;

    definition

      let X,Y be non empty TopSpace, x be Point of X, y be Point of Y, V be a_neighborhood of x, W be a_neighborhood of y;

      :: original: [:

      redefine

      func [:V,W:] -> a_neighborhood of [x, y] ;

      correctness by Th8;

    end

    theorem :: BORSUK_1:10

    

     Th10: for XT be Point of [:X, Y:] holds ex W be Point of X, T be Point of Y st XT = [W, T]

    proof

      let XT be Point of [:X, Y:];

      the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

      hence thesis by DOMAIN_1: 1;

    end;

    definition

      let X,Y be non empty TopSpace, A be Subset of X, t be Point of Y, V be a_neighborhood of A, W be a_neighborhood of t;

      :: original: [:

      redefine

      func [:V,W:] -> a_neighborhood of [:A, {t}:] ;

      correctness

      proof

        W is a_neighborhood of {t} by CONNSP_2: 8;

        hence [:V, W:] is a_neighborhood of [:A, {t}:] by Th9;

      end;

    end

    definition

      let X,Y be TopSpace;

      let A be Subset of [:X, Y:];

      :: BORSUK_1:def3

      func Base-Appr A -> Subset-Family of [:X, Y:] equals { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : [:X1, Y1:] c= A & X1 is open & Y1 is open };

      coherence

      proof

        set B = { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : [:X1, Y1:] c= A & X1 is open & Y1 is open };

        B c= ( bool the carrier of [:X, Y:])

        proof

          let e be object;

          assume e in B;

          then ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & [:X1, Y1:] c= A & X1 is open & Y1 is open;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let X,Y be TopSpace, A be Subset of [:X, Y:];

      cluster ( Base-Appr A) -> open;

      coherence

      proof

        let B be Subset of [:X, Y:];

        assume B in ( Base-Appr A);

        then ex X1 be Subset of X, Y1 be Subset of Y st B = [:X1, Y1:] & [:X1, Y1:] c= A & X1 is open & Y1 is open;

        hence thesis by Th6;

      end;

    end

    theorem :: BORSUK_1:11

    

     Th11: for X,Y be TopSpace holds for A,B be Subset of [:X, Y:] st A c= B holds ( Base-Appr A) c= ( Base-Appr B)

    proof

      let X,Y be TopSpace, A,B be Subset of [:X, Y:] such that

       A1: A c= B;

      let e be object;

      assume e in ( Base-Appr A);

      then

      consider X1 be Subset of X, Y1 be Subset of Y such that

       A2: e = [:X1, Y1:] and

       A3: [:X1, Y1:] c= A and

       A4: X1 is open & Y1 is open;

       [:X1, Y1:] c= B by A1, A3;

      hence thesis by A2, A4;

    end;

    theorem :: BORSUK_1:12

    

     Th12: for X,Y be TopSpace, A be Subset of [:X, Y:] holds ( union ( Base-Appr A)) c= A

    proof

      let X,Y be TopSpace, A be Subset of [:X, Y:];

      let e be object;

      assume e in ( union ( Base-Appr A));

      then

      consider B be set such that

       A1: e in B and

       A2: B in ( Base-Appr A) by TARSKI:def 4;

      ex X1 be Subset of X, Y1 be Subset of Y st B = [:X1, Y1:] & [:X1, Y1:] c= A & X1 is open & Y1 is open by A2;

      hence thesis by A1;

    end;

    theorem :: BORSUK_1:13

    

     Th13: for X,Y be TopSpace, A be Subset of [:X, Y:] st A is open holds A = ( union ( Base-Appr A))

    proof

      let X,Y be TopSpace, A be Subset of [:X, Y:];

      assume A is open;

      then

      consider B be Subset-Family of [:X, Y:] such that

       A1: A = ( union B) and

       A2: for e st e in B holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open by Th5;

      thus A c= ( union ( Base-Appr A))

      proof

        let e be object;

        assume e in A;

        then

        consider u such that

         A3: e in u and

         A4: u in B by A1, TARSKI:def 4;

        (ex X1 be Subset of X, Y1 be Subset of Y st u = [:X1, Y1:] & X1 is open & Y1 is open) & u c= A by A1, A2, A4, ZFMISC_1: 74;

        then u in ( Base-Appr A);

        hence thesis by A3, TARSKI:def 4;

      end;

      thus thesis by Th12;

    end;

    theorem :: BORSUK_1:14

    

     Th14: for X,Y be TopSpace, A be Subset of [:X, Y:] holds ( Int A) = ( union ( Base-Appr A))

    proof

      let X,Y be TopSpace, A be Subset of [:X, Y:];

      ( Int A) = ( union ( Base-Appr ( Int A))) & ( Base-Appr ( Int A)) c= ( Base-Appr A) by Th11, Th13, TOPS_1: 16;

      hence ( Int A) c= ( union ( Base-Appr A)) by ZFMISC_1: 77;

      ( union ( Base-Appr A)) is open by TOPS_2: 19;

      hence thesis by Th12, TOPS_1: 24;

    end;

    definition

      let X,Y be non empty TopSpace;

      :: BORSUK_1:def4

      func Pr1 (X,Y) -> Function of ( bool the carrier of [:X, Y:]), ( bool the carrier of X) equals ( .: ( pr1 (the carrier of X,the carrier of Y)));

      coherence

      proof

        the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

        hence thesis;

      end;

      correctness ;

      :: BORSUK_1:def5

      func Pr2 (X,Y) -> Function of ( bool the carrier of [:X, Y:]), ( bool the carrier of Y) equals ( .: ( pr2 (the carrier of X,the carrier of Y)));

      coherence

      proof

        the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: BORSUK_1:15

    

     Th15: for A be Subset of [:X, Y:], H be Subset-Family of [:X, Y:] st for e st e in H holds e c= A & ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] holds [:( union (( Pr1 (X,Y)) .: H)), ( meet (( Pr2 (X,Y)) .: H)):] c= A

    proof

      let A be Subset of [:X, Y:], H be Subset-Family of [:X, Y:];

      assume

       A1: for e st e in H holds e c= A & ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:];

      the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

      hence thesis by A1, EQREL_1: 51;

    end;

    theorem :: BORSUK_1:16

    

     Th16: for H be Subset-Family of [:X, Y:], C be set st C in (( Pr1 (X,Y)) .: H) holds ex D be Subset of [:X, Y:] st D in H & C = (( pr1 (the carrier of X,the carrier of Y)) .: D)

    proof

      let H be Subset-Family of [:X, Y:], C be set;

      assume C in (( Pr1 (X,Y)) .: H);

      then

      consider u be object such that

       A1: u in ( dom ( Pr1 (X,Y))) and

       A2: u in H and

       A3: C = (( Pr1 (X,Y)) . u) by FUNCT_1:def 6;

      reconsider u as Subset of [:X, Y:] by A1;

      take u;

      thus u in H by A2;

      the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

      hence thesis by A3, EQREL_1: 47;

    end;

    theorem :: BORSUK_1:17

    

     Th17: for H be Subset-Family of [:X, Y:], C be set st C in (( Pr2 (X,Y)) .: H) holds ex D be Subset of [:X, Y:] st D in H & C = (( pr2 (the carrier of X,the carrier of Y)) .: D)

    proof

      let H be Subset-Family of [:X, Y:], C be set;

      assume C in (( Pr2 (X,Y)) .: H);

      then

      consider u be object such that

       A1: u in ( dom ( Pr2 (X,Y))) and

       A2: u in H and

       A3: C = (( Pr2 (X,Y)) . u) by FUNCT_1:def 6;

      reconsider u as Subset of [:X, Y:] by A1;

      take u;

      thus u in H by A2;

      the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

      hence thesis by A3, EQREL_1: 48;

    end;

    theorem :: BORSUK_1:18

    

     Th18: for D be Subset of [:X, Y:] st D is open holds for X1 be Subset of X, Y1 be Subset of Y holds (X1 = (( pr1 (the carrier of X,the carrier of Y)) .: D) implies X1 is open) & (Y1 = (( pr2 (the carrier of X,the carrier of Y)) .: D) implies Y1 is open)

    proof

      let D be Subset of [:X, Y:];

      set p = ( pr2 (the carrier of X,the carrier of Y));

      set P = ( .: p);

      assume D is open;

      then

      consider H be Subset-Family of [:X, Y:] such that

       A1: D = ( union H) and

       A2: for e st e in H holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open by Th5;

      reconsider K = H as Subset-Family of [:the carrier of X, the carrier of Y:] by Def2;

      let X1 be Subset of X, Y1 be Subset of Y;

      thus X1 = (( pr1 (the carrier of X,the carrier of Y)) .: D) implies X1 is open

      proof

        set p = ( pr1 (the carrier of X,the carrier of Y));

        set P = ( .: p);

        reconsider PK = (P .: K) as Subset-Family of X;

        reconsider PK as Subset-Family of X;

        

         A3: PK is open

        proof

          let X1 be Subset of X;

          reconsider x1 = X1 as Subset of X;

          assume X1 in PK;

          then

          consider c be Subset of [:the carrier of X, the carrier of Y:] such that

           A4: c in K and

           A5: x1 = (P . c) by FUNCT_2: 65;

          ( dom P) = ( bool [:the carrier of X, the carrier of Y:]) by FUNCT_2:def 1;

          then

           A6: X1 = (p .: c) by A5, FUNCT_3: 7;

          

           A7: c = {} or c <> {} ;

          ex X2 be Subset of X, Y2 be Subset of Y st c = [:X2, Y2:] & X2 is open & Y2 is open by A2, A4;

          hence thesis by A6, A7, EQREL_1: 49;

        end;

        assume X1 = (p .: D);

        then X1 = ( union (P .: K)) by A1, EQREL_1: 53;

        hence thesis by A3, TOPS_2: 19;

      end;

      reconsider PK = (P .: K) as Subset-Family of Y;

      reconsider PK as Subset-Family of Y;

      

       A8: PK is open

      proof

        let Y1 be Subset of Y;

        reconsider y1 = Y1 as Subset of Y;

        assume Y1 in PK;

        then

        consider c be Subset of [:the carrier of X, the carrier of Y:] such that

         A9: c in K and

         A10: y1 = (P . c) by FUNCT_2: 65;

        ( dom P) = ( bool [:the carrier of X, the carrier of Y:]) by FUNCT_2:def 1;

        then

         A11: Y1 = (p .: c) by A10, FUNCT_3: 7;

        

         A12: c = {} or c <> {} ;

        ex X2 be Subset of X, Y2 be Subset of Y st c = [:X2, Y2:] & X2 is open & Y2 is open by A2, A9;

        hence thesis by A11, A12, EQREL_1: 49;

      end;

      assume Y1 = (p .: D);

      then Y1 = ( union (P .: K)) by A1, EQREL_1: 53;

      hence thesis by A8, TOPS_2: 19;

    end;

    theorem :: BORSUK_1:19

    

     Th19: for H be Subset-Family of [:X, Y:] st H is open holds (( Pr1 (X,Y)) .: H) is open & (( Pr2 (X,Y)) .: H) is open

    proof

      let H be Subset-Family of [:X, Y:];

      reconsider P1 = (( Pr1 (X,Y)) .: H) as Subset-Family of X;

      reconsider P2 = (( Pr2 (X,Y)) .: H) as Subset-Family of Y;

      assume

       A1: H is open;

      

       A2: P2 is open

      proof

        let Y1 be Subset of Y;

        assume Y1 in P2;

        then

        consider D be Subset of [:X, Y:] such that

         A3: D in H and

         A4: Y1 = (( pr2 (the carrier of X,the carrier of Y)) .: D) by Th17;

        D is open by A1, A3;

        hence thesis by A4, Th18;

      end;

      P1 is open

      proof

        let X1 be Subset of X;

        assume X1 in P1;

        then

        consider D be Subset of [:X, Y:] such that

         A5: D in H and

         A6: X1 = (( pr1 (the carrier of X,the carrier of Y)) .: D) by Th16;

        D is open by A1, A5;

        hence thesis by A6, Th18;

      end;

      hence thesis by A2;

    end;

    theorem :: BORSUK_1:20

    

     Th20: for H be Subset-Family of [:X, Y:] st (( Pr1 (X,Y)) .: H) = {} or (( Pr2 (X,Y)) .: H) = {} holds H = {}

    proof

      let H be Subset-Family of [:X, Y:];

      ( dom ( Pr1 (X,Y))) = ( bool the carrier of [:X, Y:]) & ( dom ( Pr2 (X,Y))) = ( bool the carrier of [:X, Y:]) by FUNCT_2:def 1;

      hence thesis;

    end;

    theorem :: BORSUK_1:21

    

     Th21: for H be Subset-Family of [:X, Y:], X1 be Subset of X, Y1 be Subset of Y st H is Cover of [:X1, Y1:] holds (Y1 <> {} implies (( Pr1 (X,Y)) .: H) is Cover of X1) & (X1 <> {} implies (( Pr2 (X,Y)) .: H) is Cover of Y1)

    proof

      let H be Subset-Family of [:X, Y:], X1 be Subset of X, Y1 be Subset of Y;

      

       A1: ( dom ( .: ( pr2 (the carrier of X,the carrier of Y)))) = ( bool ( dom ( pr2 (the carrier of X,the carrier of Y)))) by FUNCT_3:def 1

      .= ( bool [:the carrier of X, the carrier of Y:]) by FUNCT_3:def 5;

      

       A2: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

      assume

       A3: [:X1, Y1:] c= ( union H);

      thus Y1 <> {} implies (( Pr1 (X,Y)) .: H) is Cover of X1

      proof

        assume Y1 <> {} ;

        then

        consider y be Point of Y such that

         A4: y in Y1 by SUBSET_1: 4;

        let e be object;

        assume

         A5: e in X1;

        then

        reconsider x = e as Point of X;

         [x, y] in [:X1, Y1:] by A4, A5, ZFMISC_1: 87;

        then

        consider A be set such that

         A6: [x, y] in A and

         A7: A in H by A3, TARSKI:def 4;

         [x, y] in [:the carrier of X, the carrier of Y:] by ZFMISC_1: 87;

        then

         A8: [x, y] in ( dom ( pr1 (the carrier of X,the carrier of Y))) by FUNCT_3:def 4;

        

         A9: ( dom ( .: ( pr1 (the carrier of X,the carrier of Y)))) = ( bool ( dom ( pr1 (the carrier of X,the carrier of Y)))) by FUNCT_3:def 1

        .= ( bool [:the carrier of X, the carrier of Y:]) by FUNCT_3:def 4;

        e = (( pr1 (the carrier of X,the carrier of Y)) . (x,y)) by FUNCT_3:def 4;

        then

         A10: e in (( pr1 (the carrier of X,the carrier of Y)) .: A) by A6, A8, FUNCT_1:def 6;

        (( .: ( pr1 (the carrier of X,the carrier of Y))) . A) = (( pr1 (the carrier of X,the carrier of Y)) .: A) by A2, A7, EQREL_1: 47;

        then (( pr1 (the carrier of X,the carrier of Y)) .: A) in (( Pr1 (X,Y)) .: H) by A2, A7, A9, FUNCT_1:def 6;

        hence e in ( union (( Pr1 (X,Y)) .: H)) by A10, TARSKI:def 4;

      end;

      assume X1 <> {} ;

      then

      consider x be Point of X such that

       A11: x in X1 by SUBSET_1: 4;

      let e be object;

      assume

       A12: e in Y1;

      then

      reconsider y = e as Point of Y;

       [x, y] in [:X1, Y1:] by A11, A12, ZFMISC_1: 87;

      then

      consider A be set such that

       A13: [x, y] in A and

       A14: A in H by A3, TARSKI:def 4;

       [x, y] in [:the carrier of X, the carrier of Y:] by ZFMISC_1: 87;

      then

       A15: [x, y] in ( dom ( pr2 (the carrier of X,the carrier of Y))) by FUNCT_3:def 5;

      e = (( pr2 (the carrier of X,the carrier of Y)) . (x,y)) by FUNCT_3:def 5;

      then

       A16: e in (( pr2 (the carrier of X,the carrier of Y)) .: A) by A13, A15, FUNCT_1:def 6;

      (( .: ( pr2 (the carrier of X,the carrier of Y))) . A) = (( pr2 (the carrier of X,the carrier of Y)) .: A) by A2, A14, EQREL_1: 48;

      then (( pr2 (the carrier of X,the carrier of Y)) .: A) in (( Pr2 (X,Y)) .: H) by A2, A14, A1, FUNCT_1:def 6;

      hence e in ( union (( Pr2 (X,Y)) .: H)) by A16, TARSKI:def 4;

    end;

    theorem :: BORSUK_1:22

    

     Th22: for X,Y be TopSpace, H be Subset-Family of X, Y be Subset of X st H is Cover of Y holds ex F be Subset-Family of X st F c= H & F is Cover of Y & for C be set st C in F holds C meets Y

    proof

      let X,Y be TopSpace, H be Subset-Family of X;

      let Y be Subset of X;

      assume

       A1: H is Cover of Y;

      defpred P[ set] means $1 in H & ($1 /\ Y) <> {} ;

      { Z where Z be Subset of X : P[Z] } is Subset-Family of X from DOMAIN_1:sch 7;

      then

      reconsider F = { Z where Z be Subset of X : Z in H & (Z /\ Y) <> {} } as Subset-Family of X;

      reconsider F as Subset-Family of X;

      take F;

      thus F c= H

      proof

        let e be object;

        assume e in F;

        then ex Z be Subset of X st e = Z & Z in H & (Z /\ Y) <> {} ;

        hence thesis;

      end;

      

       A2: Y c= ( union H) by A1, SETFAM_1:def 11;

      thus F is Cover of Y

      proof

        let e be object;

        assume

         A3: e in Y;

        then

        consider u such that

         A4: e in u and

         A5: u in H by A2, TARSKI:def 4;

        reconsider u as Subset of X by A5;

        (u /\ Y) <> {} by A3, A4, XBOOLE_0:def 4;

        then u in F by A5;

        hence e in ( union F) by A4, TARSKI:def 4;

      end;

      let C be set;

      assume C in F;

      then ex Z be Subset of X st C = Z & Z in H & (Z /\ Y) <> {} ;

      hence (C /\ Y) <> {} ;

    end;

    theorem :: BORSUK_1:23

    

     Th23: for F be Subset-Family of X, H be Subset-Family of [:X, Y:] st F is finite & F c= (( Pr1 (X,Y)) .: H) holds ex G be Subset-Family of [:X, Y:] st G c= H & G is finite & F = (( Pr1 (X,Y)) .: G)

    proof

      let F be Subset-Family of X, H be Subset-Family of [:X, Y:] such that

       A1: F is finite and

       A2: F c= (( Pr1 (X,Y)) .: H);

      defpred P[ object, object] means $2 in ( dom ( Pr1 (X,Y))) & $2 in H & $1 = (( Pr1 (X,Y)) . $2);

      

       A3: for e be object st e in F holds ex u be object st P[e, u] by A2, FUNCT_1:def 6;

      consider f be Function such that

       A4: ( dom f) = F and

       A5: for e be object st e in F holds P[e, (f . e)] from CLASSES1:sch 1( A3);

      

       A6: (f .: F) c= H

      proof

        let e be object;

        assume e in (f .: F);

        then ex u be object st u in ( dom f) & u in F & e = (f . u) by FUNCT_1:def 6;

        hence thesis by A5;

      end;

      then

      reconsider G = (f .: F) as Subset-Family of [:X, Y:] by XBOOLE_1: 1;

      take G;

      thus G c= H by A6;

      thus G is finite by A1;

      now

        let e be object;

        thus e in F iff ex u be object st u in ( dom ( Pr1 (X,Y))) & u in G & e = (( Pr1 (X,Y)) . u)

        proof

          thus e in F implies ex u be object st u in ( dom ( Pr1 (X,Y))) & u in G & e = (( Pr1 (X,Y)) . u)

          proof

            assume

             A7: e in F;

            take (f . e);

            thus (f . e) in ( dom ( Pr1 (X,Y))) by A5, A7;

            thus (f . e) in G by A4, A7, FUNCT_1:def 6;

            thus thesis by A5, A7;

          end;

          given u be object such that u in ( dom ( Pr1 (X,Y))) and

           A8: u in G and

           A9: e = (( Pr1 (X,Y)) . u);

          ex v be object st v in ( dom f) & v in F & u = (f . v) by A8, FUNCT_1:def 6;

          hence thesis by A5, A9;

        end;

      end;

      hence thesis by FUNCT_1:def 6;

    end;

    theorem :: BORSUK_1:24

    for X1 be Subset of X, Y1 be Subset of Y st [:X1, Y1:] <> {} holds (( Pr1 (X,Y)) . [:X1, Y1:]) = X1 & (( Pr2 (X,Y)) . [:X1, Y1:]) = Y1 by EQREL_1: 50;

    theorem :: BORSUK_1:25

    

     Th25: for t be Point of Y, A be Subset of X st A is compact holds for G be a_neighborhood of [:A, {t}:] holds ex V be a_neighborhood of A, W be a_neighborhood of t st [:V, W:] c= G

    proof

      let t be Point of Y, A be Subset of X such that

       A1: A is compact;

      let G be a_neighborhood of [:A, {t}:];

      

       A2: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by Def2;

      now

        per cases ;

          suppose

           A3: A <> ( {} X);

           [:A, {t}:] c= ( Int G) by CONNSP_2:def 2;

          then [:A, {t}:] c= ( union ( Base-Appr G)) by Th14;

          then ( Base-Appr G) is Cover of [:A, {t}:] by SETFAM_1:def 11;

          then

          consider K be Subset-Family of [:X, Y:] such that

           A4: K c= ( Base-Appr G) and

           A5: K is Cover of [:A, {t}:] and

           A6: for c be set st c in K holds c meets [:A, {t}:] by Th22;

          reconsider PK = (( Pr1 (X,Y)) .: K) as Subset-Family of X;

          K is open by A4, TOPS_2: 11;

          then

           A7: (( Pr1 (X,Y)) .: K) is open by Th19;

          PK is Cover of A by A5, Th21;

          then

          consider M be Subset-Family of X such that

           A8: M c= (( Pr1 (X,Y)) .: K) and

           A9: M is Cover of A and

           A10: M is finite by A1, A7, COMPTS_1:def 4;

          consider N be Subset-Family of [:X, Y:] such that

           A11: N c= K and

           A12: N is finite and

           A13: (( Pr1 (X,Y)) .: N) = M by A8, A10, Th23;

          reconsider F = (( Pr1 (X,Y)) .: N) as Subset-Family of X;

          

           A14: N is Cover of [:A, {t}:]

          proof

            let e1,e2 be object;

            

             A15: A c= ( union M) by A9, SETFAM_1:def 11;

            assume

             A16: [e1, e2] in [:A, {t}:];

            then ( [e1, e2] `2 ) in {t} by MCART_1: 10;

            then ( [e1, e2] `2 ) = t by TARSKI:def 1;

            then

             A17: [e1, e2] = [( [e1, e2] `1 ), t];

            ( [e1, e2] `1 ) in A by A16, MCART_1: 10;

            then

            consider X1 be set such that

             A18: ( [e1, e2] `1 ) in X1 and

             A19: X1 in M by A15, TARSKI:def 4;

            consider XY be Subset of [:X, Y:] such that

             A20: XY in N and

             A21: (( Pr1 (X,Y)) . XY) = X1 by A13, A19, FUNCT_2: 65;

            XY in K by A11, A20;

            then XY in ( Base-Appr G) by A4;

            then

            consider X2 be Subset of X, Y2 be Subset of Y such that

             A22: XY = [:X2, Y2:] and [:X2, Y2:] c= G and X2 is open and Y2 is open;

            XY meets [:A, {t}:] by A6, A11, A20;

            then

            consider xy be object such that

             A23: xy in XY and

             A24: xy in [:A, {t}:] by XBOOLE_0: 3;

            (xy `2 ) in {t} by A24, MCART_1: 10;

            then (xy `2 ) = t by TARSKI:def 1;

            then

             A25: t in Y2 by A22, A23, MCART_1: 10;

            XY <> {} by A18, A21, FUNCT_3: 8;

            then ( [e1, e2] `1 ) in X2 by A18, A21, A22, EQREL_1: 50;

            then [e1, e2] in [:X2, Y2:] by A25, A17, ZFMISC_1: 87;

            hence [e1, e2] in ( union N) by A20, A22, TARSKI:def 4;

          end;

          then F is Cover of A by Th21;

          then

           A26: A c= ( union F) by SETFAM_1:def 11;

          reconsider H = (( Pr2 (X,Y)) .: N) as Subset-Family of Y;

           A27:

          now

            let C be set;

            assume C in H;

            then

            consider D be Subset of [:X, Y:] such that

             A28: D in N and

             A29: C = (( pr2 (the carrier of X,the carrier of Y)) .: D) by Th17;

            D meets [:A, {t}:] by A6, A11, A28;

            then (D /\ [:A, {t}:]) <> {} ;

            then

            consider x be Point of [:X, Y:] such that

             A30: x in (D /\ [:A, {t}:]);

            

             A31: x in [:A, {t}:] by A30, XBOOLE_0:def 4;

            then (x `1 ) in A by MCART_1: 10;

            then

             A32: (( pr2 (the carrier of X,the carrier of Y)) . ((x `1 ),t)) = t by FUNCT_3:def 5;

            (x `2 ) in {t} by A31, MCART_1: 10;

            then (x `2 ) = t by TARSKI:def 1;

            then

             A33: x = [(x `1 ), t] by A2, MCART_1: 21;

            x in D by A30, XBOOLE_0:def 4;

            hence t in C by A2, A29, A33, A32, FUNCT_2: 35;

          end;

           [:A, {t}:] c= ( union N) by A14, SETFAM_1:def 11;

          then N <> {} by A3, ZFMISC_1: 2;

          then H <> {} by Th20;

          then

           A34: t in ( meet H) by A27, SETFAM_1:def 1;

          

           A35: N c= ( Base-Appr G) by A4, A11;

          then

           A36: N is open by TOPS_2: 11;

          then ( meet H) is open by A12, Th19, TOPS_2: 20;

          then t in ( Int ( meet H)) by A34, TOPS_1: 23;

          then

          reconsider W = ( meet H) as a_neighborhood of t by CONNSP_2:def 1;

          ( union F) is open by A36, Th19, TOPS_2: 19;

          then A c= ( Int ( union F)) by A26, TOPS_1: 23;

          then

          reconsider V = ( union F) as a_neighborhood of A by CONNSP_2:def 2;

          take V, W;

          now

            let e;

            assume e in N;

            then e in ( Base-Appr G) by A35;

            then ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & [:X1, Y1:] c= G & X1 is open & Y1 is open;

            hence e c= G & ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:];

          end;

          hence [:V, W:] c= G by Th15;

        end;

          suppose A = ( {} X);

          then A c= ( Int ( {} X));

          then

          reconsider V = ( {} X) as a_neighborhood of A by CONNSP_2:def 2;

          set W = the a_neighborhood of t;

          take V, W;

          thus [:V, W:] c= G;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let X be 1-sorted;

      :: BORSUK_1:def6

      func TrivDecomp X -> a_partition of the carrier of X equals ( Class ( id the carrier of X));

      coherence ;

    end

    registration

      let X be non empty 1-sorted;

      cluster ( TrivDecomp X) -> non empty;

      coherence ;

    end

    theorem :: BORSUK_1:26

    

     Th26: for A be Subset of X st A in ( TrivDecomp X) holds ex x be Point of X st A = {x}

    proof

      let A be Subset of X;

      assume A in ( TrivDecomp X);

      then

      consider x be object such that

       A1: x in the carrier of X and

       A2: A = ( Class (( id the carrier of X),x)) by EQREL_1:def 3;

      reconsider x as Point of X by A1;

      take x;

      thus thesis by A2, EQREL_1: 25;

    end;

    

     Lm1: for A be Subset of X holds for V be a_neighborhood of A holds ex W be Subset of X st W is open & A c= W & W c= V & for B be Subset of X st B in ( TrivDecomp X) & B meets W holds B c= W

    proof

      let A be Subset of X;

      let V be a_neighborhood of A;

      take ( Int V);

      thus ( Int V) is open;

      thus A c= ( Int V) by CONNSP_2:def 2;

      thus ( Int V) c= V by TOPS_1: 16;

      let B be Subset of X such that

       A1: B in ( TrivDecomp X) and

       A2: B meets ( Int V);

      consider x be Point of X such that

       A3: B = {x} by A1, Th26;

      x in ( Int V) by A2, A3, ZFMISC_1: 50;

      hence thesis by A3, ZFMISC_1: 31;

    end;

    definition

      let X be TopSpace, D be a_partition of the carrier of X;

      :: BORSUK_1:def7

      func space D -> strict TopSpace means

      : Def7: the carrier of it = D & the topology of it = { A where A be Subset of D : ( union A) in the topology of X };

      existence

      proof

        set t = { A where A be Subset of D : ( union A) in the topology of X };

        t c= ( bool D)

        proof

          let e be object;

          assume e in t;

          then ex A be Subset of D st e = A & ( union A) in the topology of X;

          hence thesis;

        end;

        then

        reconsider t as Subset-Family of D;

        set T = TopStruct (# D, t #);

        T is TopSpace-like

        proof

          ( union D) = the carrier of X by EQREL_1:def 4;

          then D c= D & ( union D) in the topology of X by PRE_TOPC:def 1;

          hence the carrier of T in the topology of T;

          thus for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T

          proof

            let a be Subset-Family of T;

            

             A1: { ( union A) where A be Subset of T : A in a } c= ( bool the carrier of X)

            proof

              let e be object;

              reconsider ee = e as set by TARSKI: 1;

              assume e in { ( union A) where A be Subset of T : A in a };

              then

              consider A be Subset of T such that

               A2: e = ( union A) and A in a;

              ee c= the carrier of X

              proof

                let u be object;

                assume u in ee;

                then

                consider x be set such that

                 A3: u in x and

                 A4: x in A by A2, TARSKI:def 4;

                x in the carrier of T by A4;

                hence thesis by A3;

              end;

              hence thesis;

            end;

            assume

             A5: a c= the topology of T;

            { ( union A) where A be Subset of T : A in a } c= the topology of X

            proof

              let e be object;

              assume e in { ( union A) where A be Subset of T : A in a };

              then

              consider A be Subset of T such that

               A6: e = ( union A) and

               A7: A in a;

              A in the topology of T by A5, A7;

              then ex B be Subset of D st A = B & ( union B) in the topology of X;

              hence thesis by A6;

            end;

            then ( union { ( union A) where A be Subset of T : A in a }) in the topology of X by A1, PRE_TOPC:def 1;

            then ( union ( union a)) in the topology of X by EQREL_1: 54;

            hence thesis;

          end;

          let a,b be Subset of T;

          assume that

           A8: a in the topology of T and

           A9: b in the topology of T;

          consider B be Subset of D such that

           A10: b = B and

           A11: ( union B) in the topology of X by A9;

          consider A be Subset of D such that

           A12: a = A and

           A13: ( union A) in the topology of X by A8;

          ( union (A /\ B)) = (( union A) /\ ( union B)) by EQREL_1: 62;

          then ( union (A /\ B)) in the topology of X by A13, A11, PRE_TOPC:def 1;

          hence thesis by A12, A10;

        end;

        then

        reconsider T as strict TopSpace;

        take T;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let X be non empty TopSpace, D be a_partition of the carrier of X;

      cluster ( space D) -> non empty;

      coherence by Def7;

    end

    theorem :: BORSUK_1:27

    

     Th27: for D be non empty a_partition of the carrier of X, A be Subset of D holds ( union A) in the topology of X iff A in the topology of ( space D)

    proof

      let D be non empty a_partition of the carrier of X, B be Subset of D;

      

       A1: the topology of ( space D) = { A where A be Subset of D : ( union A) in the topology of X } by Def7;

      hence ( union B) in the topology of X implies B in the topology of ( space D);

      assume B in the topology of ( space D);

      then ex A be Subset of D st B = A & ( union A) in the topology of X by A1;

      hence thesis;

    end;

    definition

      let X be non empty TopSpace, D be non empty a_partition of the carrier of X;

      :: BORSUK_1:def8

      func Proj D -> continuous Function of X, ( space D) equals ( proj D);

      coherence

      proof

        reconsider F = ( proj D) as Function of X, ( space D) by Def7;

        

         A1: the carrier of ( space D) = D by Def7;

        F is continuous

        proof

          let W be Point of X, G be a_neighborhood of (F . W);

          reconsider H = ( union ( Int G)) as Subset of X by A1, EQREL_1: 61;

          (F . W) in ( Int G) by CONNSP_2:def 1;

          then W in (F " ( Int G)) by FUNCT_2: 38;

          then

           A2: W in ( union ( Int G)) by A1, EQREL_1: 67;

          ( Int G) in the topology of ( space D) by PRE_TOPC:def 2;

          then ( union ( Int G)) in the topology of X by A1, Th27;

          then H is open;

          then W in ( Int H) by A2, TOPS_1: 23;

          then W in ( Int (F " ( Int G))) by A1, EQREL_1: 67;

          then

          reconsider N = (F " ( Int G)) as a_neighborhood of W by CONNSP_2:def 1;

          take N;

          (F .: N) c= ( Int G) & ( Int G) c= G by FUNCT_1: 75, TOPS_1: 16;

          hence thesis;

        end;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: BORSUK_1:28

    for D be non empty a_partition of the carrier of X, W be Point of X holds W in (( Proj D) . W) by EQREL_1:def 9;

    theorem :: BORSUK_1:29

    

     Th29: for D be non empty a_partition of the carrier of X, W be Point of ( space D) holds ex W9 be Point of X st (( Proj D) . W9) = W

    proof

      let D be non empty a_partition of the carrier of X, W be Point of ( space D);

      reconsider p = W as Element of D by Def7;

      consider W9 be Point of X such that

       A1: (( proj D) . W9) = p by EQREL_1: 68;

      take W9;

      thus thesis by A1;

    end;

    theorem :: BORSUK_1:30

    

     Th30: for D be non empty a_partition of the carrier of X holds ( rng ( Proj D)) = the carrier of ( space D)

    proof

      let D be non empty a_partition of the carrier of X;

      thus ( rng ( Proj D)) c= the carrier of ( space D);

      let e be object;

      assume e in the carrier of ( space D);

      then ex p be Point of X st (( Proj D) . p) = e by Th29;

      hence thesis by FUNCT_2: 4;

    end;

    definition

      let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X;

      :: BORSUK_1:def9

      func TrivExt D -> non empty a_partition of the carrier of XX equals (D \/ { {p} where p be Point of XX : not p in the carrier of X });

      coherence

      proof

        set E = (D \/ { {p} where p be Point of XX : not p in the carrier of X });

        E c= ( bool the carrier of XX)

        proof

          let e be object;

          assume

           A1: e in E;

          now

            per cases by A1, XBOOLE_0:def 3;

              suppose

               A2: e in D;

              ( bool the carrier of X) c= ( bool the carrier of XX) by Th1, ZFMISC_1: 67;

              hence thesis by A2;

            end;

              suppose e in { {p} where p be Point of XX : not p in the carrier of X };

              then ex p be Point of XX st e = {p} & not p in the carrier of X;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

        reconsider E as Subset-Family of XX;

        E is a_partition of the carrier of XX

        proof

          now

            let e be object;

            thus e in (the carrier of XX \ the carrier of X) implies ex Z be set st e in Z & Z in { {p} where p be Point of XX : not p in the carrier of X }

            proof

              assume

               A3: e in (the carrier of XX \ the carrier of X);

              take {e};

              thus e in {e} by TARSKI:def 1;

               not e in the carrier of X by A3, XBOOLE_0:def 5;

              hence thesis by A3;

            end;

            given Z be set such that

             A4: e in Z and

             A5: Z in { {p} where p be Point of XX : not p in the carrier of X };

            consider p be Point of XX such that

             A6: Z = {p} and

             A7: not p in the carrier of X by A5;

            e = p by A4, A6, TARSKI:def 1;

            hence e in (the carrier of XX \ the carrier of X) by A7, XBOOLE_0:def 5;

          end;

          then

           A8: ( union { {p} where p be Point of XX : not p in the carrier of X }) = (the carrier of XX \ the carrier of X) by TARSKI:def 4;

          

          thus ( union E) = (( union D) \/ ( union { {p} where p be Point of XX : not p in the carrier of X })) by ZFMISC_1: 78

          .= (the carrier of X \/ (the carrier of XX \ the carrier of X)) by A8, EQREL_1:def 4

          .= the carrier of XX by Th1, XBOOLE_1: 45;

          let A be Subset of XX;

          assume

           A9: A in E;

          now

            per cases by A9, XBOOLE_0:def 3;

              suppose A in D;

              hence A <> {} by EQREL_1:def 4;

            end;

              suppose A in { {p} where p be Point of XX : not p in the carrier of X };

              then ex p be Point of XX st A = {p} & not p in the carrier of X;

              hence A <> {} ;

            end;

          end;

          hence A <> {} ;

          let B be Subset of XX;

          assume

           A10: B in E;

          now

            per cases by A9, XBOOLE_0:def 3;

              suppose

               A11: A in D;

              now

                per cases by A10, XBOOLE_0:def 3;

                  suppose B in D;

                  hence thesis by A11, EQREL_1:def 4;

                end;

                  suppose B in { {p} where p be Point of XX : not p in the carrier of X };

                  then ex p be Point of XX st B = {p} & not p in the carrier of X;

                  then B misses the carrier of X by ZFMISC_1: 50;

                  hence thesis by A11, XBOOLE_1: 63;

                end;

              end;

              hence thesis;

            end;

              suppose A in { {p} where p be Point of XX : not p in the carrier of X };

              then

               A12: ex p be Point of XX st A = {p} & not p in the carrier of X;

              then

               A13: A misses the carrier of X by ZFMISC_1: 50;

              now

                per cases by A10, XBOOLE_0:def 3;

                  suppose B in D;

                  hence thesis by A13, XBOOLE_1: 63;

                end;

                  suppose B in { {p} where p be Point of XX : not p in the carrier of X };

                  then ex p be Point of XX st B = {p} & not p in the carrier of X;

                  hence thesis by A12, ZFMISC_1: 11;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: BORSUK_1:31

    

     Th31: for XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, A be Subset of XX st A in ( TrivExt D) holds A in D or ex x be Point of XX st not x in ( [#] X) & A = {x}

    proof

      let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, A be Subset of XX;

      assume

       A1: A in ( TrivExt D);

      now

        per cases by A1, XBOOLE_0:def 3;

          case A in D;

          hence A in D;

        end;

          case A in { {p} where p be Point of XX : not p in the carrier of X };

          then

          consider x be Point of XX such that

           A2: A = {x} and

           A3: not x in the carrier of X;

          take x;

          thus not x in ( [#] X) by A3;

          thus A = {x} by A2;

        end;

      end;

      hence thesis;

    end;

    theorem :: BORSUK_1:32

    

     Th32: for XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, x be Point of XX st not x in the carrier of X holds {x} in ( TrivExt D)

    proof

      let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, x be Point of XX;

      ( union ( TrivExt D)) = the carrier of XX by EQREL_1:def 4;

      then

      consider A be set such that

       A1: x in A and

       A2: A in ( TrivExt D) by TARSKI:def 4;

      assume not x in the carrier of X;

      then not A in D by A1;

      then A in { {p} where p be Point of XX : not p in the carrier of X } by A2, XBOOLE_0:def 3;

      then ex p be Point of XX st A = {p} & not p in the carrier of X;

      hence thesis by A1, A2, TARSKI:def 1;

    end;

    theorem :: BORSUK_1:33

    

     Th33: for XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, W be Point of XX st W in the carrier of X holds (( Proj ( TrivExt D)) . W) = (( Proj D) . W)

    proof

      let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, W be Point of XX;

      assume

       A1: W in the carrier of X;

      then

      reconsider p = W as Point of X;

      D c= ( TrivExt D) & (( proj D) . p) in D by XBOOLE_1: 7;

      then

      reconsider A = (( Proj D) . W) as Element of ( TrivExt D);

      W in A by A1, EQREL_1:def 9;

      hence thesis by EQREL_1: 65;

    end;

    theorem :: BORSUK_1:34

    

     Th34: for XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, W be Point of XX st not W in the carrier of X holds (( Proj ( TrivExt D)) . W) = {W}

    proof

      let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, W be Point of XX;

      assume not W in the carrier of X;

      then W in {W} & {W} in ( TrivExt D) by Th32, TARSKI:def 1;

      hence thesis by EQREL_1: 65;

    end;

    theorem :: BORSUK_1:35

    

     Th35: for XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, W,W9 be Point of XX st not W in the carrier of X & (( Proj ( TrivExt D)) . W) = (( Proj ( TrivExt D)) . W9) holds W = W9

    proof

      let XX be non empty TopSpace, X be non empty SubSpace of XX, D be non empty a_partition of the carrier of X, W,W9 be Point of XX;

      assume not W in the carrier of X;

      then

       A1: (( Proj ( TrivExt D)) . W) = {W} by Th34;

      W9 in (( Proj ( TrivExt D)) . W9) by EQREL_1:def 9;

      hence thesis by A1, TARSKI:def 1;

    end;

    theorem :: BORSUK_1:36

    

     Th36: for XX be non empty TopSpace, X be non empty SubSpace of XX holds for D be non empty a_partition of the carrier of X holds for e be Point of XX st (( Proj ( TrivExt D)) . e) in the carrier of ( space D) holds e in the carrier of X

    proof

      let XX be non empty TopSpace, X be non empty SubSpace of XX;

      let D be non empty a_partition of the carrier of X;

      let e be Point of XX;

      assume (( Proj ( TrivExt D)) . e) in the carrier of ( space D);

      then

       A1: (( Proj ( TrivExt D)) . e) in D by Def7;

      e in (( Proj ( TrivExt D)) . e) by EQREL_1:def 9;

      hence thesis by A1;

    end;

    theorem :: BORSUK_1:37

    

     Th37: for XX be non empty TopSpace, X be non empty SubSpace of XX holds for D be non empty a_partition of the carrier of X holds for e st e in the carrier of X holds (( Proj ( TrivExt D)) . e) in the carrier of ( space D)

    proof

      let XX be non empty TopSpace, X be non empty SubSpace of XX;

      let D be non empty a_partition of the carrier of X;

      let e;

      assume

       A1: e in the carrier of X;

      then

      reconsider x = e as Point of X;

      the carrier of X c= the carrier of XX by Th1;

      then (( Proj D) . x) = (( Proj ( TrivExt D)) . x) by A1, Th33;

      hence thesis;

    end;

    begin

    definition

      let X be non empty TopSpace;

      :: BORSUK_1:def10

      mode u.s.c._decomposition of X -> non empty a_partition of the carrier of X means

      : Def10: for A be Subset of X st A in it holds for V be a_neighborhood of A holds ex W be Subset of X st W is open & A c= W & W c= V & for B be Subset of X st B in it & B meets W holds B c= W;

      correctness

      proof

        take ( TrivDecomp X);

        thus thesis by Lm1;

      end;

    end

    theorem :: BORSUK_1:38

    

     Th38: for D be u.s.c._decomposition of X, t be Point of ( space D), G be a_neighborhood of (( Proj D) " {t}) holds (( Proj D) .: G) is a_neighborhood of t

    proof

      let D be u.s.c._decomposition of X, t be Point of ( space D), G be a_neighborhood of (( Proj D) " {t});

      

       A1: the carrier of ( space D) = D by Def7;

      then (( Proj D) " {t}) = t by EQREL_1: 66;

      then

      consider W be Subset of X such that

       A2: W is open and

       A3: (( Proj D) " {t}) c= W and

       A4: W c= G and

       A5: for B be Subset of X st B in D & B meets W holds B c= W by A1, Def10;

      set Q = (( Proj D) .: W);

      

       A6: (( Proj D) .: (( Proj D) " {t})) c= Q by A3, RELAT_1: 123;

      ( union Q) = (( proj D) " Q) by A1, EQREL_1: 67

      .= W by A5, EQREL_1: 69;

      then ( union Q) in the topology of X by A2;

      then Q in the topology of ( space D) by A1, Th27;

      then

       A7: Q is open;

      ( rng ( Proj D)) = the carrier of ( space D) by Th30;

      then {t} c= Q by A6, FUNCT_1: 77;

      then

       A8: t in Q by ZFMISC_1: 31;

      Q c= (( Proj D) .: G) by A4, RELAT_1: 123;

      then t in ( Int (( Proj D) .: G)) by A7, A8, TOPS_1: 22;

      hence thesis by CONNSP_2:def 1;

    end;

    theorem :: BORSUK_1:39

    

     Th39: ( TrivDecomp X) is u.s.c._decomposition of X

    proof

      thus for A be Subset of X st A in ( TrivDecomp X) holds for V be a_neighborhood of A holds ex W be Subset of X st W is open & A c= W & W c= V & for B be Subset of X st B in ( TrivDecomp X) & B meets W holds B c= W by Lm1;

    end;

    definition

      let X be TopSpace;

      let IT be SubSpace of X;

      :: BORSUK_1:def11

      attr IT is closed means

      : Def11: for A be Subset of X st A = the carrier of IT holds A is closed;

    end

    

     Lm2: for T be TopStruct holds the TopStruct of T is SubSpace of T

    proof

      let T be TopStruct;

      set S = the TopStruct of T;

      thus ( [#] S) c= ( [#] T);

      let P be Subset of S;

      hereby

        reconsider Q = P as Subset of T;

        assume

         A1: P in the topology of S;

        take Q;

        thus Q in the topology of T by A1;

        thus P = (Q /\ ( [#] S)) by XBOOLE_1: 28;

      end;

      given Q be Subset of T such that

       A2: Q in the topology of T & P = (Q /\ ( [#] S));

      thus thesis by A2, XBOOLE_1: 28;

    end;

    registration

      let X be TopSpace;

      cluster strict closed for SubSpace of X;

      existence

      proof

        reconsider Y = the TopStruct of X as strict SubSpace of X by Lm2;

        take Y;

        Y is closed

        proof

          let A be Subset of X;

          assume A = the carrier of Y;

          then A = ( [#] X);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let X;

      cluster strict closed non empty for SubSpace of X;

      existence

      proof

        (X | ( [#] X)) is closed

        proof

          let A be Subset of X;

          assume A = the carrier of (X | ( [#] X));

          

          then A = ( [#] (X | ( [#] X)))

          .= ( [#] X) by PRE_TOPC:def 5;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be u.s.c._decomposition of X;

      :: original: TrivExt

      redefine

      func TrivExt D -> u.s.c._decomposition of XX ;

      correctness

      proof

        let A be Subset of XX such that

         A1: A in ( TrivExt D);

        let V be a_neighborhood of A;

        

         A2: A c= ( Int V) by CONNSP_2:def 2;

        

         A3: ( Int V) c= V by TOPS_1: 16;

        now

          per cases by A1, Th31;

            suppose

             A4: A in D;

            then

            reconsider C = A as Subset of X;

            reconsider E = (( Int V) /\ ( [#] X)) as Subset of X;

            E is open & C c= E by A2, TOPS_2: 24, XBOOLE_1: 19;

            then C c= ( Int E) by TOPS_1: 23;

            then E is a_neighborhood of C by CONNSP_2:def 2;

            then

            consider W be Subset of X such that

             A5: W is open and

             A6: C c= W and

             A7: W c= E and

             A8: for B be Subset of X st B in D & B meets W holds B c= W by A4, Def10;

            consider G be Subset of XX such that

             A9: G is open and

             A10: W = (G /\ ( [#] X)) by A5, TOPS_2: 24;

            take H = (G /\ ( Int V));

            thus H is open by A9;

            

             A11: W c= G by A10, XBOOLE_1: 17;

            then C c= G by A6;

            hence A c= H by A2, XBOOLE_1: 19;

            H c= ( Int V) by XBOOLE_1: 17;

            hence H c= V by A3;

            let B be Subset of XX such that

             A12: B in ( TrivExt D) and

             A13: B meets H;

            E c= ( Int V) by XBOOLE_1: 17;

            then W c= ( Int V) by A7;

            then

             A14: W c= H by A11, XBOOLE_1: 19;

            now

              per cases by A12, Th31;

                suppose

                 A15: B in D;

                B meets G by A13, XBOOLE_1: 74;

                then B meets W by A10, A15, XBOOLE_1: 77;

                then B c= W by A8, A15;

                hence B c= H by A14;

              end;

                suppose ex y be Point of XX st not y in ( [#] X) & B = {y};

                then

                consider y be Point of XX such that not y in ( [#] X) and

                 A16: B = {y};

                y in H by A13, A16, ZFMISC_1: 50;

                hence B c= H by A16, ZFMISC_1: 31;

              end;

            end;

            hence B c= H;

          end;

            suppose

             A17: ex x be Point of XX st not x in ( [#] X) & A = {x};

            ( [#] X) c= ( [#] XX) by PRE_TOPC:def 4;

            then

            reconsider C = ( [#] X) as Subset of XX;

            take W = (( Int V) \ C);

            C is closed by Def11;

            then (( Int V) /\ (C ` )) is open;

            hence W is open by SUBSET_1: 13;

            consider x be Point of XX such that

             A18: not x in ( [#] X) and

             A19: A = {x} by A17;

            x in A by A19, TARSKI:def 1;

            then x in W by A2, A18, XBOOLE_0:def 5;

            hence A c= W by A19, ZFMISC_1: 31;

            W c= ( Int V) by XBOOLE_1: 36;

            hence W c= V by A3;

            let B be Subset of XX such that

             A20: B in ( TrivExt D) and

             A21: B meets W;

            now

              

               A22: W misses C by XBOOLE_1: 79;

              assume B in D;

              hence contradiction by A21, A22, XBOOLE_1: 63;

            end;

            then

            consider y be Point of XX such that not y in ( [#] X) and

             A23: B = {y} by A20, Th31;

            y in W by A21, A23, ZFMISC_1: 50;

            hence B c= W by A23, ZFMISC_1: 31;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      let IT be u.s.c._decomposition of X;

      :: BORSUK_1:def12

      attr IT is DECOMPOSITION-like means

      : Def12: for A be Subset of X st A in IT holds A is compact;

    end

    registration

      let X be non empty TopSpace;

      cluster DECOMPOSITION-like for u.s.c._decomposition of X;

      existence

      proof

        reconsider D = ( TrivDecomp X) as u.s.c._decomposition of X by Th39;

        take D;

        let A be Subset of X;

        assume A in D;

        then ex x be Point of X st A = {x} by Th26;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      mode DECOMPOSITION of X is DECOMPOSITION-like u.s.c._decomposition of X;

    end

    definition

      let XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be DECOMPOSITION of X;

      :: original: TrivExt

      redefine

      func TrivExt D -> DECOMPOSITION of XX ;

      correctness

      proof

        ( TrivExt D) is DECOMPOSITION-like

        proof

          let A be Subset of XX;

          assume A in ( TrivExt D);

          then

          consider W be Point of XX such that

           A1: A = (( proj ( TrivExt D)) . W) by EQREL_1: 68;

          

           A2: A = (( Proj ( TrivExt D)) . W) by A1;

          

           A3: the carrier of ( space D) = D by Def7;

          now

            per cases ;

              suppose W in the carrier of X;

              then

              reconsider W9 = W as Point of X;

              

               A4: A = (( Proj D) . W9) by A2, Th33;

              then

              reconsider B = A as Subset of X by A3, TARSKI:def 3;

              B is compact by A3, A4, Def12;

              hence thesis by COMPTS_1: 19;

            end;

              suppose not W in the carrier of X;

              then A = {W} by A2, Th34;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace, Y be closed non empty SubSpace of X, D be DECOMPOSITION of Y;

      :: original: space

      redefine

      func space D -> strict closed SubSpace of ( space ( TrivExt D)) ;

      correctness

      proof

        

         A1: the topology of ( space ( TrivExt D)) = { A where A be Subset of ( TrivExt D) : ( union A) in the topology of X } by Def7;

        

         A2: the carrier of ( space ( TrivExt D)) = ( TrivExt D) by Def7;

        

         A3: the topology of ( space D) = { A where A be Subset of D : ( union A) in the topology of Y } by Def7;

        

         A4: the carrier of ( space D) = D by Def7;

        

         A5: ( [#] ( space D)) = D & ( [#] ( space ( TrivExt D))) = ( TrivExt D) by Def7;

        now

          thus ( [#] ( space D)) c= ( [#] ( space ( TrivExt D))) by A5, XBOOLE_1: 7;

          let P be Subset of ( space D);

          thus P in the topology of ( space D) implies ex Q be Subset of ( space ( TrivExt D)) st Q in the topology of ( space ( TrivExt D)) & P = (Q /\ ( [#] ( space D)))

          proof

            D c= ( TrivExt D) by XBOOLE_1: 7;

            then

             A6: P c= ( TrivExt D) by A4;

            assume P in the topology of ( space D);

            then

            consider A be Subset of D such that

             A7: P = A and

             A8: ( union A) in the topology of Y by A3;

            reconsider B = ( union A) as Subset of Y by A8;

            consider C be Subset of X such that

             A9: C in the topology of X and

             A10: B = (C /\ ( [#] Y)) by A8, PRE_TOPC:def 4;

            { {x} where x be Point of X : x in (C \ ( [#] Y)) } c= ( TrivExt D)

            proof

              let e be object;

              assume e in { {x} where x be Point of X : x in (C \ ( [#] Y)) };

              then

              consider x be Point of X such that

               A11: e = {x} and

               A12: x in (C \ ( [#] Y));

               not x in the carrier of Y by A12, XBOOLE_0:def 5;

              hence thesis by A11, Th32;

            end;

            then

            reconsider Q = (P \/ { {x} where x be Point of X : x in (C \ ( [#] Y)) }) as Subset of ( space ( TrivExt D)) by A2, A6, XBOOLE_1: 8;

            take Q;

            now

              let e be object;

              thus e in C implies ex u st e in u & u in Q

              proof

                assume

                 A13: e in C;

                then

                reconsider x = e as Point of X;

                now

                  per cases ;

                    case e in ( [#] Y);

                    then e in B by A10, A13, XBOOLE_0:def 4;

                    then

                    consider u such that

                     A14: e in u & u in P by A7, TARSKI:def 4;

                    take u;

                    thus e in u & u in Q by A14, XBOOLE_0:def 3;

                  end;

                    case

                     A15: not e in ( [#] Y);

                    take u = {e};

                    thus e in u by TARSKI:def 1;

                    x in (C \ ( [#] Y)) by A13, A15, XBOOLE_0:def 5;

                    then u in { {y} where y be Point of X : y in (C \ ( [#] Y)) };

                    hence u in Q by XBOOLE_0:def 3;

                  end;

                end;

                hence thesis;

              end;

              given u such that

               A16: e in u and

               A17: u in Q;

              now

                per cases by A17, XBOOLE_0:def 3;

                  suppose u in P;

                  then e in B by A7, A16, TARSKI:def 4;

                  hence e in C by A10, XBOOLE_0:def 4;

                end;

                  suppose u in { {x} where x be Point of X : x in (C \ ( [#] Y)) };

                  then

                  consider x be Point of X such that

                   A18: u = {x} and

                   A19: x in (C \ ( [#] Y));

                  e = x by A16, A18, TARSKI:def 1;

                  hence e in C by A19, XBOOLE_0:def 5;

                end;

              end;

              hence e in C;

            end;

            then C = ( union Q) by TARSKI:def 4;

            hence Q in the topology of ( space ( TrivExt D)) by A2, A1, A9;

            P c= Q by XBOOLE_1: 7;

            hence P c= (Q /\ ( [#] ( space D))) by XBOOLE_1: 19;

            let e be object;

            assume

             A20: e in (Q /\ ( [#] ( space D)));

            then

             A21: e in ( [#] ( space D));

             A22:

            now

              assume e in { {x} where x be Point of X : x in (C \ ( [#] Y)) };

              then

              consider x be Point of X such that

               A23: e = {x} and

               A24: x in (C \ ( [#] Y));

              

               A25: not x in the carrier of Y by A24, XBOOLE_0:def 5;

              then not (( Proj ( TrivExt D)) . x) in the carrier of ( space D) by Th36;

              hence contradiction by A21, A23, A25, Th34;

            end;

            e in Q by A20, XBOOLE_0:def 4;

            hence thesis by A22, XBOOLE_0:def 3;

          end;

          given Q be Subset of ( space ( TrivExt D)) such that

           A26: Q in the topology of ( space ( TrivExt D)) and

           A27: P = (Q /\ ( [#] ( space D)));

          

           A28: ( union P) is Subset of Y by A4, EQREL_1: 61;

          now

            let e be object;

            thus e in (( union Q) /\ ( [#] Y)) implies ex u st e in u & u in P

            proof

              assume

               A29: e in (( union Q) /\ ( [#] Y));

              then

               A30: (( Proj ( TrivExt D)) . e) in the carrier of ( space D) by Th37;

              e in ( union Q) by A29, XBOOLE_0:def 4;

              then

              consider u such that

               A31: e in u and

               A32: u in Q by TARSKI:def 4;

              take u;

              thus e in u by A31;

              u is Element of ( TrivExt D) by A32, Def7;

              then u = (( Proj ( TrivExt D)) . e) by A31, EQREL_1: 65;

              hence thesis by A27, A32, A30, XBOOLE_0:def 4;

            end;

            given u such that

             A33: e in u and

             A34: u in P;

            u in Q by A27, A34, XBOOLE_0:def 4;

            then

             A35: e in ( union Q) by A33, TARSKI:def 4;

            e in ( union P) by A33, A34, TARSKI:def 4;

            hence e in (( union Q) /\ ( [#] Y)) by A28, A35, XBOOLE_0:def 4;

          end;

          then

           A36: ( union P) = (( union Q) /\ ( [#] Y)) by TARSKI:def 4;

          ex A be Subset of ( TrivExt D) st Q = A & ( union A) in the topology of X by A1, A26;

          then ( union P) in the topology of Y by A36, PRE_TOPC:def 4;

          hence P in the topology of ( space D) by A4, A3;

        end;

        then

        reconsider T = ( space D) as SubSpace of ( space ( TrivExt D)) by PRE_TOPC:def 4;

        T is closed

        proof

          let A be Subset of ( space ( TrivExt D)) such that

           A37: A = the carrier of T;

          reconsider C = (A ` ) as Subset of ( TrivExt D) by Def7;

          reconsider B = ( union A) as Subset of X by A2, EQREL_1: 61;

          B = the carrier of Y by A4, A37, EQREL_1:def 4;

          then B is closed by Def11;

          then

           A38: (B ` ) in the topology of X by PRE_TOPC:def 2;

          ( union C) = (B ` ) by A2, EQREL_1: 63;

          then (A ` ) in the topology of ( space ( TrivExt D)) by A38, Th27;

          then (A ` ) is open;

          hence thesis by TOPS_1: 3;

        end;

        hence thesis;

      end;

    end

    begin

    

     Lm3: ( TopSpaceMetr RealSpace ) = TopStruct (# the carrier of RealSpace , ( Family_open_set RealSpace ) #) by PCOMPS_1:def 5;

    definition

      :: BORSUK_1:def13

      func I[01] -> TopStruct means

      : Def13: for P be Subset of ( TopSpaceMetr RealSpace ) st P = [. 0 , 1.] holds it = (( TopSpaceMetr RealSpace ) | P);

      existence

      proof

        reconsider P = [. 0 , 1.] as non empty Subset of ( TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 13, XXREAL_1: 1;

        take (( TopSpaceMetr RealSpace ) | P);

        thus thesis;

      end;

      uniqueness

      proof

        reconsider P = [. 0 , 1.] as Subset of ( TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 13;

        let I1,I2 be TopStruct such that

         A1: for P be Subset of ( TopSpaceMetr RealSpace ) st P = [. 0 , 1.] holds I1 = (( TopSpaceMetr RealSpace ) | P) and

         A2: for P be Subset of ( TopSpaceMetr RealSpace ) st P = [. 0 , 1.] holds I2 = (( TopSpaceMetr RealSpace ) | P);

        I1 = (( TopSpaceMetr RealSpace ) | P) by A1;

        hence thesis by A2;

      end;

    end

    registration

      cluster I[01] -> strict non empty TopSpace-like;

      coherence

      proof

        reconsider P = [. 0 , 1.] as non empty Subset of ( TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 13, XXREAL_1: 1;

         I[01] = (( TopSpaceMetr RealSpace ) | P) by Def13;

        hence thesis;

      end;

    end

    theorem :: BORSUK_1:40

    

     Th40: the carrier of I[01] = [. 0 , 1.]

    proof

      reconsider P = [. 0 , 1.] as Subset of ( TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 13;

      

       A1: I[01] = (( TopSpaceMetr RealSpace ) | P) by Def13;

      

      thus the carrier of I[01] = ( [#] I[01] )

      .= [. 0 , 1.] by A1, PRE_TOPC:def 5;

    end;

    definition

      :: BORSUK_1:def14

      func 0[01] -> Point of I[01] equals 0 ;

      coherence by Th40, XXREAL_1: 1;

      :: BORSUK_1:def15

      func 1[01] -> Point of I[01] equals 1;

      coherence by Th40, XXREAL_1: 1;

    end

    definition

      let A be non empty TopSpace, B be non empty SubSpace of A, F be Function of A, B;

      :: BORSUK_1:def16

      attr F is being_a_retraction means for W be Point of A st W in the carrier of B holds (F . W) = W;

    end

    definition

      let X be non empty TopSpace, Y be non empty SubSpace of X;

      :: BORSUK_1:def17

      pred Y is_a_retract_of X means ex F be continuous Function of X, Y st F is being_a_retraction;

      :: BORSUK_1:def18

      pred Y is_an_SDR_of X means ex H be continuous Function of [:X, I[01] :], X st for A be Point of X holds (H . [A, 0[01] ]) = A & (H . [A, 1[01] ]) in the carrier of Y & (A in the carrier of Y implies for T be Point of I[01] holds (H . [A, T]) = A);

    end

    theorem :: BORSUK_1:41

    for XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be DECOMPOSITION of X st X is_a_retract_of XX holds ( space D) is_a_retract_of ( space ( TrivExt D))

    proof

      let XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be DECOMPOSITION of X;

      thus X is_a_retract_of XX implies ( space D) is_a_retract_of ( space ( TrivExt D))

      proof

        given R be continuous Function of XX, X such that

         A1: R is being_a_retraction;

        now

          given xx,xx9 be Point of XX such that

           A2: (( Proj ( TrivExt D)) . xx) = (( Proj ( TrivExt D)) . xx9) & ((( Proj D) * R) . xx) <> ((( Proj D) * R) . xx9);

          xx in the carrier of X by A2, Th35;

          then (R . xx) = xx by A1;

          then

           A3: (( Proj D) . xx) = ((( Proj D) * R) . xx) by FUNCT_2: 15;

          xx9 in the carrier of X by A2, Th35;

          then

           A4: (R . xx9) = xx9 by A1;

          (( Proj ( TrivExt D)) . xx) = (( Proj D) . xx) & (( Proj ( TrivExt D)) . xx9) = (( Proj D) . xx9) by A2, Th33, Th35;

          hence contradiction by A2, A4, A3, FUNCT_2: 15;

        end;

        then

        consider F be Function of the carrier of ( space ( TrivExt D)), the carrier of ( space D) such that

         A5: (F * ( Proj ( TrivExt D))) = (( Proj D) * R) by EQREL_1: 56;

        reconsider F as Function of ( space ( TrivExt D)), ( space D);

        F is continuous

        proof

          let W be Point of ( space ( TrivExt D));

          let G be a_neighborhood of (F . W);

          reconsider GG = ((( Proj D) * R) " G) as a_neighborhood of (( Proj ( TrivExt D)) " {W}) by A5, Th4, EQREL_1: 57;

          reconsider V9 = (( Proj ( TrivExt D)) .: GG) as a_neighborhood of W by Th38;

          take V = V9;

          (F .: V) = ((( Proj D) * R) .: GG) by A5, RELAT_1: 126;

          hence thesis by FUNCT_1: 75;

        end;

        then

        reconsider F9 = F as continuous Function of ( space ( TrivExt D)), ( space D);

        take F9;

        let W be Point of ( space ( TrivExt D));

        consider W9 be Point of XX such that

         A6: (( Proj ( TrivExt D)) . W9) = W by Th29;

        assume

         A7: W in the carrier of ( space D);

        then W9 in the carrier of X by A6, Th36;

        then

         A8: W9 = (R . W9) by A1;

        

         A9: (F9 . W) = ((F * ( Proj ( TrivExt D))) . W9) by A6, FUNCT_2: 15;

        (( Proj D) . W9) = (( Proj ( TrivExt D)) . W9) by A6, A7, Th33, Th36;

        hence thesis by A5, A6, A8, A9, FUNCT_2: 15;

      end;

    end;

    ::$Notion-Name

    theorem :: BORSUK_1:42

    for XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be DECOMPOSITION of X st X is_an_SDR_of XX holds ( space D) is_an_SDR_of ( space ( TrivExt D))

    proof

      let XX be non empty TopSpace, X be closed non empty SubSpace of XX, D be DECOMPOSITION of X;

      given CH1 be continuous Function of [:XX, I[01] :], XX such that

       A1: for A be Point of XX holds (CH1 . [A, 0[01] ]) = A & (CH1 . [A, 1[01] ]) in the carrier of X & (A in the carrier of X implies for T be Point of I[01] holds (CH1 . [A, T]) = A);

      the carrier of [:XX, I[01] :] = [:the carrier of XX, the carrier of I[01] :] by Def2;

      then

      reconsider II = [:( Proj ( TrivExt D)), ( id the carrier of I[01] ):] as Function of the carrier of [:XX, I[01] :], the carrier of [:( space ( TrivExt D)), I[01] :] by Def2;

      now

        given xx,xx9 be Point of [:XX, I[01] :] such that

         A2: (II . xx) = (II . xx9) and

         A3: ((( Proj ( TrivExt D)) * CH1) . xx) <> ((( Proj ( TrivExt D)) * CH1) . xx9);

        

         A4: ((( Proj ( TrivExt D)) * CH1) . xx) = (( Proj ( TrivExt D)) . (CH1 . xx)) & ((( Proj ( TrivExt D)) * CH1) . xx9) = (( Proj ( TrivExt D)) . (CH1 . xx9)) by FUNCT_2: 15;

        consider x be Point of XX, t be Point of I[01] such that

         A5: xx = [x, t] by Th10;

        consider x9 be Point of XX, t9 be Point of I[01] such that

         A6: xx9 = [x9, t9] by Th10;

        

         A7: (II . (x,t)) = [(( Proj ( TrivExt D)) . x), t] & (II . (x9,t9)) = [(( Proj ( TrivExt D)) . x9), t9] by EQREL_1: 58;

        then t = t9 & (( Proj ( TrivExt D)) . x) = (( Proj ( TrivExt D)) . x9) by A2, A5, A6, XTUPLE_0: 1;

        then (CH1 . xx) = x & (CH1 . xx9) = x9 by A1, A3, A5, A6, Th35;

        hence contradiction by A2, A3, A5, A6, A7, A4, XTUPLE_0: 1;

      end;

      then

      consider THETA be Function of the carrier of [:( space ( TrivExt D)), I[01] :], the carrier of ( space ( TrivExt D)) such that

       A8: (( Proj ( TrivExt D)) * CH1) = (THETA * II) by EQREL_1: 56;

      reconsider THETA as Function of [:( space ( TrivExt D)), I[01] :], ( space ( TrivExt D));

      THETA is continuous

      proof

        let WT be Point of [:( space ( TrivExt D)), I[01] :];

        reconsider xt9 = WT as Element of [:the carrier of ( space ( TrivExt D)), the carrier of I[01] :] by Def2;

        let G be a_neighborhood of (THETA . WT);

        reconsider FF = (( Proj ( TrivExt D)) * CH1) as continuous Function of [:XX, I[01] :], ( space ( TrivExt D));

        consider W be Point of ( space ( TrivExt D)), T be Point of I[01] such that

         A9: WT = [W, T] by Th10;

        (II " {xt9}) = [:(( Proj ( TrivExt D)) " {W}), {T}:] by A9, EQREL_1: 60;

        then

        reconsider GG = (FF " G) as a_neighborhood of [:(( Proj ( TrivExt D)) " {W}), {T}:] by A8, Th4, EQREL_1: 57;

        W in the carrier of ( space ( TrivExt D));

        then

         A10: W in ( TrivExt D) by Def7;

        then (( Proj ( TrivExt D)) " {W}) = W by EQREL_1: 66;

        then (( Proj ( TrivExt D)) " {W}) is compact by A10, Def12;

        then

        consider U be a_neighborhood of (( Proj ( TrivExt D)) " {W}), V be a_neighborhood of T such that

         A11: [:U, V:] c= GG by Th25;

        reconsider H9 = (( Proj ( TrivExt D)) .: U) as a_neighborhood of W by Th38;

        reconsider H99 = [:H9, V:] as a_neighborhood of WT by A9;

        take H = H99;

        (II .: [:U, V:]) = [:(( Proj ( TrivExt D)) .: U), V:] by EQREL_1: 59;

        then

         A12: ((( Proj ( TrivExt D)) * CH1) .: GG) c= G & (THETA .: H) = ((( Proj ( TrivExt D)) * CH1) .: [:U, V:]) by A8, FUNCT_1: 75, RELAT_1: 126;

        ((( Proj ( TrivExt D)) * CH1) .: [:U, V:]) c= ((( Proj ( TrivExt D)) * CH1) .: GG) by A11, RELAT_1: 123;

        hence thesis by A12;

      end;

      then

      reconsider THETA9 = THETA as continuous Function of [:( space ( TrivExt D)), I[01] :], ( space ( TrivExt D));

      take THETA99 = THETA9;

      let W be Point of ( space ( TrivExt D));

      consider W9 be Point of XX such that

       A13: (( Proj ( TrivExt D)) . W9) = W by Th29;

      (II . (W9, 0[01] )) = [W, 0[01] ] by A13, EQREL_1: 58;

      then

       A14: ((THETA9 * II) . [W9, 0[01] ]) = (THETA9 . [W, 0[01] ]) by FUNCT_2: 15;

      (CH1 . (W9, 0[01] )) = W9 by A1;

      hence (THETA99 . [W, 0[01] ]) = W by A8, A13, A14, FUNCT_2: 15;

      

       A15: (CH1 . [W9, 1[01] ]) in the carrier of X by A1;

      (II . (W9, 1[01] )) = [W, 1[01] ] by A13, EQREL_1: 58;

      then

       A16: ((THETA9 * II) . [W9, 1[01] ]) = (THETA9 . [W, 1[01] ]) by FUNCT_2: 15;

      ((THETA9 * II) . [W9, 1[01] ]) = (( Proj ( TrivExt D)) . (CH1 . [W9, 1[01] ])) by A8, FUNCT_2: 15;

      hence (THETA99 . [W, 1[01] ]) in the carrier of ( space D) by A16, A15, Th37;

      assume

       A17: W in the carrier of ( space D);

      let T be Point of I[01] ;

      (II . (W9,T)) = [W, T] by A13, EQREL_1: 58;

      then

       A18: ((THETA9 * II) . [W9, T]) = (THETA9 . [W, T]) by FUNCT_2: 15;

      (CH1 . (W9,T)) = W9 by A1, A13, A17, Th36;

      hence thesis by A8, A13, A18, FUNCT_2: 15;

    end;

    theorem :: BORSUK_1:43

    for r be Real holds 0 <= r & r <= 1 iff r in the carrier of I[01]

    proof

      let r be Real;

      

       A1: [. 0 , 1.] = { r1 where r1 be Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;

      thus 0 <= r & r <= 1 implies r in the carrier of I[01] by A1, Th40;

      assume r in the carrier of I[01] ;

      then ex r2 be Real st r2 = r & 0 <= r2 & r2 <= 1 by A1, Th40;

      hence thesis;

    end;