borsuk_3.miz

    begin

    theorem :: BORSUK_3:1

    for S,T be TopSpace holds ( [#] [:S, T:]) = [:( [#] S), ( [#] T):] by BORSUK_1:def 2;

    theorem :: BORSUK_3:2



     Th2: for X,Y be non empty TopSpace, x be Point of X holds (Y --> x) is continuous Function of Y, (X | {x})

    proof

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

      set Z = {x};

      set f = (Y --> x);

      x in Z & the carrier of (X | Z) = Z by PRE_TOPC: 8, TARSKI:def 1;

      then

      reconsider g = f as Function of Y, (X | Z) by FUNCOP_1: 45;

      g is continuous by TOPMETR: 6;

      hence thesis;

    end;

    registration

      let T be TopStruct;

      cluster ( id T) -> being_homeomorphism;

      coherence by TOPGRP_1: 20;

    end



     Lm1: for S be TopStruct holds (S,S) are_homeomorphic

    proof

      let S be TopStruct;

      take ( id S);

      thus thesis;

    end;



     Lm2: for S,T be non empty TopStruct st (S,T) are_homeomorphic holds (T,S) are_homeomorphic

    proof

      let S,T be non empty TopStruct;

      assume (S,T) are_homeomorphic ;

      then

      consider f be Function of S, T such that

       A1: f is being_homeomorphism;

      (f " ) is being_homeomorphism by A1, TOPS_2: 56;

      hence thesis;

    end;

    definition

      let S,T be TopStruct;

      :: original: are_homeomorphic

      redefine

      pred S,T are_homeomorphic ;

      reflexivity by Lm1;

    end

    definition

      let S,T be non empty TopStruct;

      :: original: are_homeomorphic

      redefine

      pred S,T are_homeomorphic ;

      reflexivity by Lm1;

      symmetry by Lm2;

    end

    theorem :: BORSUK_3:3

    for S,T,V be non empty TopSpace st (S,T) are_homeomorphic & (T,V) are_homeomorphic holds (S,V) are_homeomorphic

    proof

      let S,T,V be non empty TopSpace;

      assume that

       A1: (S,T) are_homeomorphic and

       A2: (T,V) are_homeomorphic ;

      consider f be Function of S, T such that

       A3: f is being_homeomorphism by A1;

      consider g be Function of T, V such that

       A4: g is being_homeomorphism by A2;

      (g * f) is being_homeomorphism by A3, A4, TOPS_2: 57;

      hence thesis;

    end;

    begin

    registration

      let T be TopStruct, P be empty Subset of T;

      cluster (T | P) -> empty;

      coherence ;

    end

    registration

      cluster empty -> compact for TopSpace;

      coherence ;

    end

    theorem :: BORSUK_3:4



     Th4: for X,Y be non empty TopSpace, x be Point of X, f be Function of [:Y, (X | {x}):], Y st f = ( pr1 (the carrier of Y, {x})) holds f is one-to-one

    proof

      let X,Y be non empty TopSpace, x be Point of X, f be Function of [:Y, (X | {x}):], Y;

      set Z = {x};

      assume

       A1: f = ( pr1 (the carrier of Y,Z));

      let z,y be object such that

       A2: z in ( dom f) and

       A3: y in ( dom f) and

       A4: (f . z) = (f . y);



       A5: ( dom f) = [:the carrier of Y, Z:] by A1, FUNCT_3:def 4;

      then

      consider x1,x2 be object such that

       A6: x1 in the carrier of Y and

       A7: x2 in Z and

       A8: z = [x1, x2] by A2, ZFMISC_1:def 2;

      consider y1,y2 be object such that

       A9: y1 in the carrier of Y and

       A10: y2 in Z and

       A11: y = [y1, y2] by A5, A3, ZFMISC_1:def 2;



       A12: x2 = x by A7, TARSKI:def 1

      .= y2 by A10, TARSKI:def 1;

      x1 = (f . (x1,x2)) by A1, A6, A7, FUNCT_3:def 4

      .= (f . (y1,y2)) by A4, A8, A11

      .= y1 by A1, A9, A10, FUNCT_3:def 4;

      hence thesis by A8, A11, A12;

    end;

    theorem :: BORSUK_3:5



     Th5: for X,Y be non empty TopSpace, x be Point of X, f be Function of [:(X | {x}), Y:], Y st f = ( pr2 ( {x},the carrier of Y)) holds f is one-to-one

    proof

      let X,Y be non empty TopSpace, x be Point of X, f be Function of [:(X | {x}), Y:], Y;

      set Z = {x};

      assume

       A1: f = ( pr2 (Z,the carrier of Y));

      let z,y be object such that

       A2: z in ( dom f) and

       A3: y in ( dom f) and

       A4: (f . z) = (f . y);



       A5: ( dom f) = [:Z, the carrier of Y:] by A1, FUNCT_3:def 5;

      then

      consider x1,x2 be object such that

       A6: x1 in Z and

       A7: x2 in the carrier of Y and

       A8: z = [x1, x2] by A2, ZFMISC_1:def 2;

      consider y1,y2 be object such that

       A9: y1 in Z and

       A10: y2 in the carrier of Y and

       A11: y = [y1, y2] by A5, A3, ZFMISC_1:def 2;



       A12: x1 = x by A6, TARSKI:def 1

      .= y1 by A9, TARSKI:def 1;

      x2 = (f . (x1,x2)) by A1, A6, A7, FUNCT_3:def 5

      .= (f . (y1,y2)) by A4, A8, A11

      .= y2 by A1, A9, A10, FUNCT_3:def 5;

      hence thesis by A8, A11, A12;

    end;

    theorem :: BORSUK_3:6



     Th6: for X,Y be non empty TopSpace, x be Point of X, f be Function of [:Y, (X | {x}):], Y st f = ( pr1 (the carrier of Y, {x})) holds (f " ) = <:( id Y), (Y --> x):>

    proof

      let X,Y be non empty TopSpace, x be Point of X, f be Function of [:Y, (X | {x}):], Y;

      set Z = {x};

      set idZ = ( id Y);



       A1: ( rng idZ) c= the carrier of Y;

      assume

       A2: f = ( pr1 (the carrier of Y,Z));

      then

       A3: ( rng f) = the carrier of Y by FUNCT_3: 44;

      reconsider Z as non empty Subset of X;

      reconsider idY = (Y --> x) as continuous Function of Y, (X | Z) by Th2;

      reconsider KA = <:idZ, idY:> as continuous Function of Y, [:Y, (X | Z):] by YELLOW12: 41;



       A4: [:the carrier of Y, Z:] c= ( rng KA)

      proof

        let y be object;

        assume y in [:the carrier of Y, Z:];

        then

        consider y1,y2 be object such that

         A5: y1 in the carrier of Y and

         A6: y2 in {x} & y = [y1, y2] by ZFMISC_1:def 2;



         A7: y = [y1, x] by A6, TARSKI:def 1;



         A8: (idY . y1) = ((the carrier of Y --> x) . y1)

        .= x by A5, FUNCOP_1: 7;



         A9: y1 in ( dom KA) by A5, FUNCT_2:def 1;



        then (KA . y1) = [(idZ . y1), (idY . y1)] by FUNCT_3:def 7

        .= [y1, x] by A5, A8, FUNCT_1: 18;

        hence thesis by A7, A9, FUNCT_1:def 3;

      end;

      ( rng idY) c= the carrier of (X | Z);

      then

       A10: ( rng idY) c= Z by PRE_TOPC: 8;

      then ( rng KA) c= [:( rng idZ), ( rng idY):] & [:( rng idZ), ( rng idY):] c= [:the carrier of Y, Z:] by FUNCT_3: 51, ZFMISC_1: 96;

      then ( rng KA) c= [:the carrier of Y, Z:];



      then

       A11: ( rng KA) = [:the carrier of Y, Z:] by A4

      .= ( dom f) by A2, FUNCT_3:def 4;



       A12: f is one-to-one by A2, Th4;



       A13: f is onto by A3, FUNCT_2:def 3;

      ( dom idY) = the carrier of Y by FUNCT_2:def 1

      .= ( dom idZ) by FUNCT_2:def 1;

      then (f * KA) = ( id ( rng f)) by A2, A3, A10, A1, FUNCT_3: 52;

      then KA = (f qua Function " ) by A12, A11, FUNCT_1: 42;

      hence thesis by A12, A13, TOPS_2:def 4;

    end;

    theorem :: BORSUK_3:7



     Th7: for X,Y be non empty TopSpace, x be Point of X, f be Function of [:(X | {x}), Y:], Y st f = ( pr2 ( {x},the carrier of Y)) holds (f " ) = <:(Y --> x), ( id Y):>

    proof

      let X,Y be non empty TopSpace, x be Point of X, f be Function of [:(X | {x}), Y:], Y;

      set Z = {x};

      set idY = ( id Y);



       A1: ( rng idY) c= the carrier of Y;

      assume

       A2: f = ( pr2 (Z,the carrier of Y));

      then

       A3: ( rng f) = the carrier of Y by FUNCT_3: 46;

      reconsider Z as non empty Subset of X;

      reconsider idZ = (Y --> x) as continuous Function of Y, (X | Z) by Th2;

      reconsider KA = <:idZ, idY:> as continuous Function of Y, [:(X | Z), Y:] by YELLOW12: 41;



       A4: [: {x}, the carrier of Y:] c= ( rng KA)

      proof

        let y be object;

        assume y in [: {x}, the carrier of Y:];

        then

        consider y1,y2 be object such that

         A5: y1 in {x} and

         A6: y2 in the carrier of Y and

         A7: y = [y1, y2] by ZFMISC_1:def 2;



         A8: y = [x, y2] by A5, A7, TARSKI:def 1;



         A9: (idZ . y2) = ((the carrier of Y --> x) . y2)

        .= x by A6, FUNCOP_1: 7;



         A10: y2 in ( dom KA) by A6, FUNCT_2:def 1;



        then (KA . y2) = [(idZ . y2), (idY . y2)] by FUNCT_3:def 7

        .= [x, y2] by A6, A9, FUNCT_1: 18;

        hence thesis by A8, A10, FUNCT_1:def 3;

      end;

      ( rng idZ) c= the carrier of (X | Z);

      then

       A11: ( rng idZ) c= Z by PRE_TOPC: 8;

      then ( rng KA) c= [:( rng idZ), ( rng idY):] & [:( rng idZ), ( rng idY):] c= [: {x}, the carrier of Y:] by FUNCT_3: 51, ZFMISC_1: 96;

      then ( rng KA) c= [: {x}, the carrier of Y:];



      then

       A12: ( rng KA) = [:Z, the carrier of Y:] by A4

      .= ( dom f) by A2, FUNCT_3:def 5;



       A13: f is one-to-one by A2, Th5;



       A14: f is onto by A3, FUNCT_2:def 3;

      ( dom idZ) = the carrier of Y by FUNCT_2:def 1

      .= ( dom idY) by FUNCT_2:def 1;

      then (f * KA) = ( id ( rng f)) by A2, A3, A11, A1, FUNCT_3: 52;

      then KA = (f qua Function " ) by A13, A12, FUNCT_1: 42;

      hence thesis by A13, A14, TOPS_2:def 4;

    end;

    theorem :: BORSUK_3:8

    for X,Y be non empty TopSpace, x be Point of X, f be Function of [:Y, (X | {x}):], Y st f = ( pr1 (the carrier of Y, {x})) holds f is being_homeomorphism

    proof

      let X,Y be non empty TopSpace, x be Point of X, f be Function of [:Y, (X | {x}):], Y;

      set Z = {x};

      assume

       A1: f = ( pr1 (the carrier of Y,Z));

      thus ( dom f) = ( [#] [:Y, (X | Z):]) by FUNCT_2:def 1;

      thus ( rng f) = ( [#] Y) by A1, FUNCT_3: 44;

      thus f is one-to-one by A1, Th4;

      the carrier of (X | Z) = Z by PRE_TOPC: 8;

      hence f is continuous by A1, YELLOW12: 39;

      reconsider Z as non empty Subset of X;

      reconsider idZ = (Y --> x) as continuous Function of Y, (X | Z) by Th2;

      reconsider KA = <:( id Y), idZ:> as continuous Function of Y, [:Y, (X | Z):] by YELLOW12: 41;

      KA = (f " ) by A1, Th6;

      hence thesis;

    end;

    theorem :: BORSUK_3:9



     Th9: for X,Y be non empty TopSpace, x be Point of X, f be Function of [:(X | {x}), Y:], Y st f = ( pr2 ( {x},the carrier of Y)) holds f is being_homeomorphism

    proof

      let X,Y be non empty TopSpace, x be Point of X, f be Function of [:(X | {x}), Y:], Y;

      set Z = {x};

      assume

       A1: f = ( pr2 (Z,the carrier of Y));

      thus ( dom f) = ( [#] [:(X | Z), Y:]) by FUNCT_2:def 1;

      thus ( rng f) = ( [#] Y) by A1, FUNCT_3: 46;

      thus f is one-to-one by A1, Th5;

      the carrier of (X | Z) = Z by PRE_TOPC: 8;

      hence f is continuous by A1, YELLOW12: 40;

      reconsider Z as non empty Subset of X;

      reconsider idZ = (Y --> x) as continuous Function of Y, (X | Z) by Th2;

      reconsider KA = <:idZ, ( id Y):> as continuous Function of Y, [:(X | Z), Y:] by YELLOW12: 41;

      KA = (f " ) by A1, Th7;

      hence thesis;

    end;

    begin

    theorem :: BORSUK_3:10

    for X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:X, Y:], x be set st [: {x}, the carrier of Y:] c= G holds ex f be ManySortedSet of the carrier of Y st for i be object st i in the carrier of Y holds ex G1 be Subset of X, H1 be Subset of Y st (f . i) = [G1, H1] & [x, i] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G

    proof

      let X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:X, Y:], x be set;

      set y = the Point of Y;



       A1: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] & [x, y] in [: {x}, the carrier of Y:] by BORSUK_1:def 2, ZFMISC_1: 105;

      defpred P[ object, object] means ex G1 be Subset of X, H1 be Subset of Y st $2 = [G1, H1] & [x, $1] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G;

      assume

       A2: [: {x}, the carrier of Y:] c= G;

      then [: {x}, the carrier of Y:] c= the carrier of [:X, Y:] by XBOOLE_1: 1;

      then

      reconsider x9 = x as Point of X by A1, ZFMISC_1: 87;



       A3: [: {x9}, the carrier of Y:] c= ( union ( Base-Appr G)) by A2, BORSUK_1: 13;

       A4:

      now

        let y be set;



         A5: x in {x9} by TARSKI:def 1;

        assume y in the carrier of Y;

        then [x, y] in [: {x9}, the carrier of Y:] by A5, ZFMISC_1: 87;

        then

        consider Z be set such that

         A6: [x, y] in Z and

         A7: Z in ( Base-Appr G) by A3, TARSKI:def 4;

        ( Base-Appr G) = { [:X1, Y1:] where X1 be Subset of X, Y1 be Subset of Y : [:X1, Y1:] c= G & X1 is open & Y1 is open } by BORSUK_1:def 3;

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

        hence ex G1 be Subset of X, H1 be Subset of Y st [x, y] in [:G1, H1:] & [:G1, H1:] c= G & G1 is open & H1 is open by A6;

      end;



       A8: for i be object st i in the carrier of Y holds ex j be object st P[i, j]

      proof

        let i be object;

        assume i in the carrier of Y;

        then

        consider G1 be Subset of X, H1 be Subset of Y such that

         A9: [x, i] in [:G1, H1:] & [:G1, H1:] c= G & G1 is open & H1 is open by A4;

        ex G2 be Subset of X, H2 be Subset of Y st [G1, H1] = [G2, H2] & [x, i] in [:G2, H2:] & G2 is open & H2 is open & [:G2, H2:] c= G by A9;

        hence thesis;

      end;

      ex f be ManySortedSet of the carrier of Y st for i be object st i in the carrier of Y holds P[i, (f . i)] from PBOOLE:sch 3( A8);

      hence thesis;

    end;

    theorem :: BORSUK_3:11



     Th11: for X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:Y, X:] holds for x be set st [:( [#] Y), {x}:] c= G holds ex R be open Subset of X st x in R & R c= { y where y be Point of X : [:( [#] Y), {y}:] c= G }

    proof

      let X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:Y, X:];

      let x be set;

      set y = the Point of Y;



       A1: the carrier of [:Y, X:] = [:the carrier of Y, the carrier of X:] & [y, x] in [:the carrier of Y, {x}:] by BORSUK_1:def 2, ZFMISC_1: 106;

      assume

       A2: [:( [#] Y), {x}:] c= G;

      then [:( [#] Y), {x}:] c= the carrier of [:Y, X:] by XBOOLE_1: 1;

      then

      reconsider x9 = x as Point of X by A1, ZFMISC_1: 87;

      ( Int G) = G by TOPS_1: 23;

      then ( [#] Y) is compact & G is a_neighborhood of [:( [#] Y), {x9}:] by A2, COMPTS_1: 1, CONNSP_2:def 2;

      then

      consider W be a_neighborhood of ( [#] Y), V be a_neighborhood of x9 such that

       A3: [:W, V:] c= G by BORSUK_1: 25;

      take R = ( Int V);

      ( Int W) c= W & ( [#] Y) c= ( Int W) by CONNSP_2:def 2, TOPS_1: 16;

      then

       A4: ( [#] Y) c= W;



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

      R c= { z where z be Point of X : [:( [#] Y), {z}:] c= G }

      proof

        let r be object;

        assume

         A6: r in R;

        then

        reconsider r9 = r as Point of X;

         {r} c= V by A5, A6, ZFMISC_1: 31;

        then [:( [#] Y), {r9}:] c= [:W, V:] by A4, ZFMISC_1: 96;

        then [:( [#] Y), {r9}:] c= G by A3;

        hence thesis;

      end;

      hence thesis by CONNSP_2:def 1;

    end;

    theorem :: BORSUK_3:12



     Th12: for X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:Y, X:] holds { x where x be Point of X : [:( [#] Y), {x}:] c= G } in the topology of X

    proof

      let X be non empty TopSpace, Y be compact non empty TopSpace, G be open Subset of [:Y, X:];

      set Q = { x where x be Point of X : [:( [#] Y), {x}:] c= G };

      Q c= the carrier of X

      proof

        let q be object;

        assume q in Q;

        then ex x9 be Point of X st q = x9 & [:( [#] Y), {x9}:] c= G;

        hence thesis;

      end;

      then

      reconsider Q as Subset of X;

      defpred P[ set] means ex y be set st y in Q & ex S be Subset of X st S = $1 & S is open & y in S & S c= Q;

      consider RR be set such that

       A1: for x be set holds x in RR iff x in ( bool Q) & P[x] from XFAMILY:sch 1;

      RR c= ( bool Q) by A1;

      then

      reconsider RR as Subset-Family of Q;

      Q c= ( union RR)

      proof

        let a be object;

        assume a in Q;

        then ex x9 be Point of X st a = x9 & [:( [#] Y), {x9}:] c= G;

        then

        consider R be open Subset of X such that

         A2: a in R and

         A3: R c= Q by Th11;

        R in RR by A1, A2, A3;

        hence thesis by A2, TARSKI:def 4;

      end;

      then

       A4: ( union RR) = Q;

      ( bool Q) c= ( bool the carrier of X) by ZFMISC_1: 67;

      then

      reconsider RR as Subset-Family of X by XBOOLE_1: 1;

      RR c= the topology of X

      proof

        let x be object;

        assume x in RR;

        then ex y be set st y in Q & ex S be Subset of X st S = x & S is open & y in S & S c= Q by A1;

        hence thesis by PRE_TOPC:def 2;

      end;

      hence thesis by A4, PRE_TOPC:def 1;

    end;

    theorem :: BORSUK_3:13



     Th13: for X,Y be non empty TopSpace, x be Point of X holds ( [:(X | {x}), Y:],Y) are_homeomorphic

    proof

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

      set Z = {x};

      the carrier of [:(X | Z), Y:] = [:the carrier of (X | Z), the carrier of Y:] by BORSUK_1:def 2

      .= [:Z, the carrier of Y:] by PRE_TOPC: 8;

      then

      reconsider f = ( pr2 (Z,the carrier of Y)) as Function of [:(X | Z), Y:], Y;

      take f;

      thus thesis by Th9;

    end;



     Lm3: for X be non empty TopSpace, Y be non empty TopSpace, x be Point of X, Z be non empty Subset of X st Z = {x} holds ( [:Y, (X | Z):],Y) are_homeomorphic

    proof

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

      ( [:Y, (X | Z):], [:(X | Z), Y:]) are_homeomorphic by YELLOW12: 44;

      then

      consider g be Function of [:Y, (X | Z):], [:(X | Z), Y:] such that

       A1: g is being_homeomorphism;

      assume Z = {x};

      then ( [:(X | Z), Y:],Y) are_homeomorphic by Th13;

      then

      consider f be Function of [:(X | Z), Y:], Y such that

       A2: f is being_homeomorphism;

      reconsider gf = (f * g) as Function of [:Y, (X | Z):], Y;

      gf is being_homeomorphism by A2, A1, TOPS_2: 57;

      hence thesis;

    end;

    theorem :: BORSUK_3:14



     Th14: for S,T be non empty TopSpace st (S,T) are_homeomorphic & S is compact holds T is compact

    proof

      let S,T be non empty TopSpace;

      assume that

       A1: (S,T) are_homeomorphic and

       A2: S is compact;

      consider f be Function of S, T such that

       A3: f is being_homeomorphism by A1;

      f is continuous & ( rng f) = ( [#] T) by A3;

      hence thesis by A2, COMPTS_1: 14;

    end;

    theorem :: BORSUK_3:15



     Th15: for X,Y be TopSpace, XV be SubSpace of X holds [:Y, XV:] is SubSpace of [:Y, X:]

    proof

      let X,Y be TopSpace, XV be SubSpace of X;

      set S = [:Y, XV:], T = [:Y, X:];



       A1: the carrier of [:Y, XV:] = [:the carrier of Y, the carrier of XV:] by BORSUK_1:def 2;



       A2: the carrier of [:Y, X:] = [:the carrier of Y, the carrier of X:] & the carrier of XV c= the carrier of X by BORSUK_1: 1, BORSUK_1:def 2;



       A3: for P be Subset of S holds P in the topology of S iff ex Q be Subset of T st Q in the topology of T & P = (Q /\ ( [#] S))

      proof

        reconsider oS = ( [#] S) as Subset of T by A1, A2, ZFMISC_1: 96;

        let P be Subset of S;

        reconsider P9 = P as Subset of S;

        hereby

          assume P in the topology of S;

          then P9 is open by PRE_TOPC:def 2;

          then

          consider A be Subset-Family of S such that

           A4: P9 = ( union A) and

           A5: for e be set st e in A holds ex X1 be Subset of Y, Y1 be Subset of XV st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

          set AA = { [:X1, Y2:] where X1 be Subset of Y, Y2 be Subset of X : ex Y1 be Subset of XV st Y1 = (Y2 /\ ( [#] XV)) & X1 is open & Y2 is open & [:X1, Y1:] in A };

          AA c= ( bool the carrier of T)

          proof

            let a be object;

            assume a in AA;

            then ex Xx1 be Subset of Y, Yy2 be Subset of X st a = [:Xx1, Yy2:] & ex Y1 be Subset of XV st Y1 = (Yy2 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Xx1, Y1:] in A;

            hence thesis;

          end;

          then

          reconsider AA as Subset-Family of T;

          reconsider AA as Subset-Family of T;



           A6: P c= (( union AA) /\ ( [#] S))

          proof

            let p be object;

            assume p in P;

            then

            consider A1 be set such that

             A7: p in A1 and

             A8: A1 in A by A4, TARSKI:def 4;

            reconsider A1 as Subset of S by A8;

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

             A9: A1 = [:X2, Y2:] and

             A10: X2 is open and

             A11: Y2 is open by A5, A8;

            Y2 in the topology of XV by A11, PRE_TOPC:def 2;

            then

            consider Q1 be Subset of X such that

             A12: Q1 in the topology of X and

             A13: Y2 = (Q1 /\ ( [#] XV)) by PRE_TOPC:def 4;

            consider p1,p2 be object such that

             A14: p1 in X2 and

             A15: p2 in Y2 and

             A16: p = [p1, p2] by A7, A9, ZFMISC_1:def 2;

            reconsider Q1 as Subset of X;

            set EX = [:X2, Q1:];

            p2 in Q1 by A15, A13, XBOOLE_0:def 4;

            then

             A17: p in EX by A14, A16, ZFMISC_1: 87;

            Q1 is open by A12, PRE_TOPC:def 2;

            then EX in { [:Xx1, Yy2:] where Xx1 be Subset of Y, Yy2 be Subset of X : ex Z1 be Subset of XV st Z1 = (Yy2 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Xx1, Z1:] in A } by A8, A9, A10, A13;

            then p in ( union AA) by A17, TARSKI:def 4;

            hence thesis by A7, A8, XBOOLE_0:def 4;

          end;

          AA c= the topology of T

          proof

            let t be object;

            set A9 = {t};

            assume t in AA;

            then

            consider Xx1 be Subset of Y, Yy2 be Subset of X such that

             A18: t = [:Xx1, Yy2:] and

             A19: ex Y1 be Subset of XV st Y1 = (Yy2 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Xx1, Y1:] in A;

            A9 c= ( bool the carrier of T)

            proof

              let a be object;

              assume a in A9;

              then a = t by TARSKI:def 1;

              hence thesis by A18;

            end;

            then

            reconsider A9 as Subset-Family of T;



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

            proof

              let x be object;

              assume x in A9;

              then

               A21: x = [:Xx1, Yy2:] by A18, TARSKI:def 1;

              Xx1 in the topology of Y & Yy2 in the topology of X by A19, PRE_TOPC:def 2;

              hence thesis by A21;

            end;

            t = ( union A9);

            then t in { ( union As) where As be Subset-Family of T : As c= { [:X1, Y1:] where X1 be Subset of Y, Y1 be Subset of X : X1 in the topology of Y & Y1 in the topology of X } } by A20;

            hence thesis by BORSUK_1:def 2;

          end;

          then

           A22: ( union AA) in the topology of T by PRE_TOPC:def 1;

          (( union AA) /\ ( [#] S)) c= P

          proof

            let h be object;

            assume

             A23: h in (( union AA) /\ ( [#] S));

            then h in ( union AA) by XBOOLE_0:def 4;

            then

            consider A2 be set such that

             A24: h in A2 and

             A25: A2 in AA by TARSKI:def 4;

            consider Xx1 be Subset of Y, Yy2 be Subset of X such that

             A26: A2 = [:Xx1, Yy2:] and

             A27: ex Y1 be Subset of XV st Y1 = (Yy2 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Xx1, Y1:] in A by A25;

            consider Yy1 be Subset of XV such that

             A28: Yy1 = (Yy2 /\ ( [#] XV)) and Xx1 is open and Yy2 is open and

             A29: [:Xx1, Yy1:] in A by A27;

            consider p1,p2 be object such that

             A30: p1 in Xx1 and

             A31: p2 in Yy2 and

             A32: h = [p1, p2] by A24, A26, ZFMISC_1:def 2;

            p2 in the carrier of XV by A1, A23, A32, ZFMISC_1: 87;

            then p2 in (Yy2 /\ ( [#] XV)) by A31, XBOOLE_0:def 4;

            then h in [:Xx1, Yy1:] by A30, A32, A28, ZFMISC_1: 87;

            hence thesis by A4, A29, TARSKI:def 4;

          end;

          then P = (( union AA) /\ ( [#] S)) by A6;

          hence ex Q be Subset of T st Q in the topology of T & P = (Q /\ ( [#] S)) by A22;

        end;

        given Q be Subset of T such that

         A33: Q in the topology of T and

         A34: P = (Q /\ ( [#] S));

        reconsider Q9 = Q as Subset of T;

        Q9 is open by A33, PRE_TOPC:def 2;

        then

        consider A be Subset-Family of T such that

         A35: Q9 = ( union A) and

         A36: for e be set st e in A holds ex X1 be Subset of Y, Y1 be Subset of X st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

        reconsider A as Subset-Family of T;

        reconsider AA = (A | oS) as Subset-Family of (T | oS);

        reconsider AA as Subset-Family of S by PRE_TOPC: 8;

        reconsider AA as Subset-Family of S;



         A37: for e be set st e in AA holds ex X1 be Subset of Y, Y1 be Subset of XV st e = [:X1, Y1:] & X1 is open & Y1 is open

        proof

          let e be set;

          assume

           A38: e in AA;

          then

          reconsider e9 = e as Subset of (T | oS);

          consider R be Subset of T such that

           A39: R in A and

           A40: (R /\ oS) = e9 by A38, TOPS_2:def 3;

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

           A41: R = [:X1, Y1:] and

           A42: X1 is open and

           A43: Y1 is open by A36, A39;

          reconsider D2 = (Y1 /\ ( [#] XV)) as Subset of XV;

          Y1 in the topology of X by A43, PRE_TOPC:def 2;

          then D2 in the topology of XV by PRE_TOPC:def 4;

          then

           A44: D2 is open by PRE_TOPC:def 2;

          ( [#] [:Y, XV:]) = [:( [#] Y), ( [#] XV):] by BORSUK_1:def 2;

          then e9 = [:(X1 /\ ( [#] Y)), (Y1 /\ ( [#] XV)):] by A40, A41, ZFMISC_1: 100;

          hence thesis by A42, A44;

        end;



         A45: (( union A) /\ oS) c= ( union AA)

        proof

          let s be object;

          assume

           A46: s in (( union A) /\ oS);

          then s in ( union A) by XBOOLE_0:def 4;

          then

          consider A1 be set such that

           A47: s in A1 and

           A48: A1 in A by TARSKI:def 4;

          s in oS by A46, XBOOLE_0:def 4;

          then

           A49: s in (A1 /\ oS) by A47, XBOOLE_0:def 4;

          reconsider A1 as Subset of T by A48;

          (A1 /\ oS) in AA by A48, TOPS_2: 31;

          hence thesis by A49, TARSKI:def 4;

        end;

        ( union AA) c= ( union A) by TOPS_2: 34;

        then ( union AA) c= (( union A) /\ oS) by XBOOLE_1: 19;

        then P = ( union AA) by A34, A35, A45;

        then P9 is open by A37, BORSUK_1: 5;

        hence thesis by PRE_TOPC:def 2;

      end;

      ( [#] S) c= ( [#] T) by A1, A2, ZFMISC_1: 96;

      hence thesis by A3, PRE_TOPC:def 4;

    end;



     Lm4: for X,Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X st Z = [:( [#] Y), V:] holds the TopStruct of [:Y, (X | V):] = the TopStruct of ( [:Y, X:] | Z)

    proof

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

      reconsider A = [:Y, (X | V):] as SubSpace of [:Y, X:] by Th15;

      assume

       A1: Z = [:( [#] Y), V:];

      the carrier of A = [:the carrier of Y, the carrier of (X | V):] by BORSUK_1:def 2

      .= Z by A1, PRE_TOPC: 8

      .= the carrier of ( [:Y, X:] | Z) by PRE_TOPC: 8;

      then A is SubSpace of ( [:Y, X:] | Z) & ( [:Y, X:] | Z) is SubSpace of A by TOPMETR: 3;

      hence thesis by TSEP_1: 6;

    end;

    theorem :: BORSUK_3:16



     Th16: for X be non empty TopSpace, Y be compact non empty TopSpace, x be Point of X, Z be Subset of [:Y, X:] st Z = [:( [#] Y), {x}:] holds Z is compact

    proof

      let X be non empty TopSpace, Y be compact non empty TopSpace, x be Point of X, Z be Subset of [:Y, X:];

      reconsider V = {x} as non empty Subset of X;

      (Y, [:Y, (X | V):]) are_homeomorphic by Lm3;

      then

       A1: [:Y, (X | V):] is compact by Th14;

      assume

       A2: Z = [:( [#] Y), {x}:];

      then the TopStruct of [:Y, (X | V):] = the TopStruct of ( [:Y, X:] | Z) by Lm4;

      hence thesis by A2, A1, COMPTS_1: 3;

    end;

    registration

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

      cluster [:Y, (X | {x}):] -> compact;

      coherence

      proof

        (Y, [:Y, (X | {x}):]) are_homeomorphic by Lm3;

        hence thesis by Th14;

      end;

    end

    theorem :: BORSUK_3:17

    for X,Y be compact non empty TopSpace, R be Subset-Family of X st R = { Q where Q be open Subset of X : [:( [#] Y), Q:] c= ( union ( Base-Appr ( [#] [:Y, X:]))) } holds R is open & R is Cover of ( [#] X)

    proof

      let X,Y be compact non empty TopSpace, R be Subset-Family of X;

      assume

       A1: R = { Q where Q be open Subset of X : [:( [#] Y), Q:] c= ( union ( Base-Appr ( [#] [:Y, X:]))) };

      now

        let P be Subset of X;

        assume P in R;

        then ex E be open Subset of X st E = P & [:( [#] Y), E:] c= ( union ( Base-Appr ( [#] [:Y, X:]))) by A1;

        hence P is open;

      end;

      hence R is open;

      ( [#] X) c= ( union R)

      proof

        let k be object;

        assume k in ( [#] X);

        then

        reconsider k9 = k as Point of X;

        reconsider Z = [:( [#] Y), {k9}:] as Subset of [:Y, X:];

        Z c= ( [#] [:Y, X:]);

        then Z c= ( union ( Base-Appr ( [#] [:Y, X:]))) by BORSUK_1: 13;

        then

         A2: ( Base-Appr ( [#] [:Y, X:])) is Cover of Z by SETFAM_1:def 11;

        Z is compact by Th16;

        then

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

         A3: G c= ( Base-Appr ( [#] [:Y, X:])) and

         A4: G is Cover of Z and G is finite by A2;

        set uR = ( union G);

        set Q = { x where x be Point of X : [:( [#] Y), {x}:] c= uR };

        Q c= the carrier of X

        proof

          let k be object;

          assume k in Q;

          then ex x1 be Point of X st k = x1 & [:( [#] Y), {x1}:] c= uR;

          hence thesis;

        end;

        then

        reconsider Q as Subset of X;

        Z c= ( union G) by A4, SETFAM_1:def 11;

        then

         A5: k9 in Q;



         A6: [:( [#] Y), Q:] c= ( union ( Base-Appr ( [#] [:Y, X:])))

        proof

          let z be object;

          assume z in [:( [#] Y), Q:];

          then

          consider x1,x2 be object such that

           A7: x1 in ( [#] Y) and

           A8: x2 in Q and

           A9: z = [x1, x2] by ZFMISC_1:def 2;

          consider x29 be Point of X such that

           A10: x29 = x2 and

           A11: [:( [#] Y), {x29}:] c= uR by A8;

          x2 in {x29} by A10, TARSKI:def 1;

          then

           A12: z in [:( [#] Y), {x29}:] by A7, A9, ZFMISC_1: 87;

          uR c= ( union ( Base-Appr ( [#] [:Y, X:]))) by A3, ZFMISC_1: 77;

          then [:( [#] Y), {x29}:] c= ( union ( Base-Appr ( [#] [:Y, X:]))) by A11;

          hence thesis by A12;

        end;

        uR is open by A3, TOPS_2: 11, TOPS_2: 19;

        then Q in the topology of X by Th12;

        then Q is open by PRE_TOPC:def 2;

        then Q in R by A1, A6;

        hence thesis by A5, TARSKI:def 4;

      end;

      hence thesis by SETFAM_1:def 11;

    end;

    theorem :: BORSUK_3:18



     Th18: for X,Y be compact non empty TopSpace, R be Subset-Family of X, F be Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open & R = { Q where Q be open Subset of X : ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q:] c= ( union FQ) } holds R is open & R is Cover of X

    proof

      let X,Y be compact non empty TopSpace, R be Subset-Family of X, F be Subset-Family of [:Y, X:];

      assume that

       A1: F is Cover of [:Y, X:] and

       A2: F is open and

       A3: R = { Q where Q be open Subset of X : ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q:] c= ( union FQ) };

      now

        let P be Subset of X;

        assume P in R;

        then ex E be open Subset of X st E = P & ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), E:] c= ( union FQ) by A3;

        hence P is open;

      end;

      hence R is open;



       A4: ( union F) = ( [#] [:Y, X:]) by A1, SETFAM_1: 45;

      ( [#] X) c= ( union R)

      proof

        let k be object;

        assume k in ( [#] X);

        then

        reconsider k9 = k as Point of X;

        reconsider Z = [:( [#] Y), {k9}:] as Subset of [:Y, X:];

        F is Cover of Z & Z is compact by A4, Th16, SETFAM_1:def 11;

        then

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

         A5: G c= F and

         A6: G is Cover of Z and

         A7: G is finite by A2;

        set uR = ( union G);

        set Q = { x where x be Point of X : [:( [#] Y), {x}:] c= uR };

        Q c= the carrier of X

        proof

          let k be object;

          assume k in Q;

          then ex x1 be Point of X st k = x1 & [:( [#] Y), {x1}:] c= uR;

          hence thesis;

        end;

        then

        reconsider Q as Subset of X;

        Z c= ( union G) by A6, SETFAM_1:def 11;

        then

         A8: k9 in Q;



         A9: ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q:] c= ( union FQ)

        proof

          take G;

           [:( [#] Y), Q:] c= ( union G)

          proof

            let z be object;

            assume z in [:( [#] Y), Q:];

            then

            consider x1,x2 be object such that

             A10: x1 in ( [#] Y) and

             A11: x2 in Q and

             A12: z = [x1, x2] by ZFMISC_1:def 2;

            consider x29 be Point of X such that

             A13: x29 = x2 and

             A14: [:( [#] Y), {x29}:] c= uR by A11;

            x2 in {x29} by A13, TARSKI:def 1;

            then z in [:( [#] Y), {x29}:] by A10, A12, ZFMISC_1: 87;

            hence thesis by A14;

          end;

          hence thesis by A5, A7;

        end;

        uR is open by A2, A5, TOPS_2: 11, TOPS_2: 19;

        then Q in the topology of X by Th12;

        then Q is open by PRE_TOPC:def 2;

        then Q in R by A3, A9;

        hence thesis by A8, TARSKI:def 4;

      end;

      hence thesis by SETFAM_1:def 11;

    end;

    theorem :: BORSUK_3:19



     Th19: for X,Y be compact non empty TopSpace, R be Subset-Family of X, F be Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open & R = { Q where Q be open Subset of X : ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q:] c= ( union FQ) } holds ex C be Subset-Family of X st C c= R & C is finite & C is Cover of X

    proof

      let X,Y be compact non empty TopSpace, R be Subset-Family of X, F be Subset-Family of [:Y, X:];

      assume F is Cover of [:Y, X:] & F is open & R = { Q where Q be open Subset of X : ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q:] c= ( union FQ) };

      then R is open & R is Cover of X by Th18;

      then ex G be Subset-Family of X st G c= R & G is Cover of X & G is finite by COMPTS_1:def 1;

      hence thesis;

    end;

    theorem :: BORSUK_3:20



     Th20: for X,Y be compact non empty TopSpace, F be Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open holds ex G be Subset-Family of [:Y, X:] st G c= F & G is Cover of [:Y, X:] & G is finite

    proof

      let X,Y be compact non empty TopSpace;

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

      set R = { Q where Q be open Subset of X : ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q:] c= ( union FQ) };

      R c= ( bool the carrier of X)

      proof

        let s be object;

        assume s in R;

        then ex Q1 be open Subset of X st s = Q1 & ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q1:] c= ( union FQ);

        hence thesis;

      end;

      then

      reconsider R as Subset-Family of X;

      reconsider R as Subset-Family of X;

      defpred P[ object, object] means ex D1 be set, FQ be Subset-Family of [:Y, X:] st D1 = $1 & FQ c= F & FQ is finite & [:( [#] Y), D1:] c= ( union FQ) & $2 = FQ;

      deffunc F( set) = [:( [#] Y), $1:];

      assume F is Cover of [:Y, X:] & F is open;

      then

      consider C be Subset-Family of X such that

       A1: C c= R and

       A2: C is finite and

       A3: C is Cover of X by Th19;

      set CX = { F(f) where f be Subset of X : f in C };

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

      proof

        let s be object;

        assume s in CX;

        then

        consider f1 be Subset of X such that

         A4: s = F(f1) and f1 in C;

         [:( [#] Y), f1:] c= the carrier of [:Y, X:];

        hence thesis by A4;

      end;

      then

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

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



       A5: for e be object st e in C holds ex u be object st P[e, u]

      proof

        let e be object;

        assume e in C;

        then e in R by A1;

        then ex Q1 be open Subset of X st Q1 = e & ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q1:] c= ( union FQ);

        hence thesis;

      end;

      consider t be Function such that

       A6: ( dom t) = C & for s be object st s in C holds P[s, (t . s)] from CLASSES1:sch 1( A5);

      set G = ( union ( rng t));



       A7: ( union ( rng t)) c= F

      proof

        let k be object;

        assume k in ( union ( rng t));

        then

        consider K be set such that

         A8: k in K and

         A9: K in ( rng t) by TARSKI:def 4;

        consider x1 be object such that

         A10: x1 in ( dom t) & K = (t . x1) by A9, FUNCT_1:def 3;

        reconsider x1 as set by TARSKI: 1;

         P[x1, (t . x1)] by A6, A10;

        then ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), x1:] c= ( union FQ) & K = FQ by A10;

        hence thesis by A8;

      end;

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

      proof

        let s be object;

        assume s in G;

        then s in F by A7;

        hence thesis;

      end;

      then

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

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

      take G;

      thus G c= F by A7;

      ( union CX) = [:( [#] Y), ( union C):]

      proof

        hereby

          let g be object;

          assume g in ( union CX);

          then

          consider GG be set such that

           A11: g in GG and

           A12: GG in CX by TARSKI:def 4;

          consider FF be Subset of X such that

           A13: GG = [:( [#] Y), FF:] and

           A14: FF in C by A12;

          consider g1,g2 be object such that

           A15: g1 in ( [#] Y) and

           A16: g2 in FF and

           A17: g = [g1, g2] by A11, A13, ZFMISC_1:def 2;

          g2 in ( union C) by A14, A16, TARSKI:def 4;

          hence g in [:( [#] Y), ( union C):] by A15, A17, ZFMISC_1: 87;

        end;

        let g be object;

        assume g in [:( [#] Y), ( union C):];

        then

        consider g1,g2 be object such that

         A18: g1 in ( [#] Y) and

         A19: g2 in ( union C) and

         A20: g = [g1, g2] by ZFMISC_1:def 2;

        consider GG be set such that

         A21: g2 in GG and

         A22: GG in C by A19, TARSKI:def 4;

        GG in { Q where Q be open Subset of X : ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q:] c= ( union FQ) } by A1, A22;

        then

        consider Q1 be open Subset of X such that

         A23: GG = Q1 and ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Q1:] c= ( union FQ);



         A24: [:( [#] Y), Q1:] in CX by A22, A23;

        g in [:( [#] Y), Q1:] by A18, A20, A21, A23, ZFMISC_1: 87;

        hence thesis by A24, TARSKI:def 4;

      end;



      then

       A25: ( union CX) = [:( [#] Y), ( [#] X):] by A3, SETFAM_1: 45

      .= ( [#] [:Y, X:]) by BORSUK_1:def 2;

      ( [#] [:Y, X:]) c= ( union ( union ( rng t)))

      proof

        let d be object;

        assume d in ( [#] [:Y, X:]);

        then

        consider CC be set such that

         A26: d in CC and

         A27: CC in CX by A25, TARSKI:def 4;

        consider Cc be Subset of X such that

         A28: CC = [:( [#] Y), Cc:] and

         A29: Cc in C by A27;

        Cc in R by A1, A29;

        then

        consider Qq be open Subset of X such that

         A30: Cc = Qq and ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), Qq:] c= ( union FQ);

         P[Cc, (t . Cc)] by A6, A29;

        then

        consider FQ1 be Subset-Family of [:Y, X:] such that FQ1 c= F and FQ1 is finite and

         A31: [:( [#] Y), Qq:] c= ( union FQ1) and

         A32: (t . Qq) = FQ1 by A30;

        consider DC be set such that

         A33: d in DC and

         A34: DC in FQ1 by A26, A28, A30, A31, TARSKI:def 4;

        FQ1 in ( rng t) by A6, A29, A30, A32, FUNCT_1:def 3;

        then DC in ( union ( rng t)) by A34, TARSKI:def 4;

        hence thesis by A33, TARSKI:def 4;

      end;

      hence G is Cover of [:Y, X:] by SETFAM_1:def 11;



       A35: for X1 be set st X1 in ( rng t) holds X1 is finite

      proof

        let X1 be set;

        assume X1 in ( rng t);

        then

        consider x1 be object such that

         A36: x1 in ( dom t) and

         A37: X1 = (t . x1) by FUNCT_1:def 3;

        reconsider x1 as set by TARSKI: 1;

         P[x1, (t . x1)] by A6, A36;

        then ex FQ be Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:( [#] Y), x1:] c= ( union FQ) & (t . x1) = FQ;

        hence thesis by A37;

      end;

      ( rng t) is finite by A2, A6, FINSET_1: 8;

      hence thesis by A35, FINSET_1: 7;

    end;



     Lm5: for T1,T2 be compact non empty TopSpace holds [:T1, T2:] is compact by Th20;

    registration

      let T1,T2 be compact TopSpace;

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

      coherence

      proof

        per cases ;

          suppose T1 is non empty & T2 is non empty;

          hence thesis by Lm5;

        end;

          suppose T1 is empty & T2 is empty;

          hence thesis;

        end;

          suppose T1 is empty & T2 is non empty;

          hence thesis;

        end;

          suppose T1 is non empty & T2 is empty;

          hence thesis;

        end;

      end;

    end



     Lm6: for X,Y be TopSpace, XV be SubSpace of X holds [:XV, Y:] is SubSpace of [:X, Y:]

    proof

      let X,Y be TopSpace, XV be SubSpace of X;

      set S = [:XV, Y:], T = [:X, Y:];



       A1: the carrier of S = [:the carrier of XV, the carrier of Y:] by BORSUK_1:def 2;



       A2: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] & the carrier of XV c= the carrier of X by BORSUK_1: 1, BORSUK_1:def 2;



       A3: for P be Subset of S holds P in the topology of S iff ex Q be Subset of T st Q in the topology of T & P = (Q /\ ( [#] S))

      proof

        reconsider oS = ( [#] S) as Subset of T by A1, A2, ZFMISC_1: 96;

        let P be Subset of S;

        reconsider P9 = P as Subset of S;

        hereby

          assume P in the topology of S;

          then P9 is open by PRE_TOPC:def 2;

          then

          consider A be Subset-Family of S such that

           A4: P9 = ( union A) and

           A5: for e be set st e in A holds ex X1 be Subset of XV, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

          set AA = { [:X1, Y2:] where X1 be Subset of X, Y2 be Subset of Y : ex Y1 be Subset of XV st Y1 = (X1 /\ ( [#] XV)) & X1 is open & Y2 is open & [:Y1, Y2:] in A };

          AA c= ( bool the carrier of T)

          proof

            let a be object;

            assume a in AA;

            then ex Xx1 be Subset of X, Yy2 be Subset of Y st a = [:Xx1, Yy2:] & ex Y1 be Subset of XV st Y1 = (Xx1 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Y1, Yy2:] in A;

            hence thesis;

          end;

          then

          reconsider AA as Subset-Family of T;

          reconsider AA as Subset-Family of T;



           A6: P c= (( union AA) /\ ( [#] S))

          proof

            let p be object;

            assume p in P;

            then

            consider A1 be set such that

             A7: p in A1 and

             A8: A1 in A by A4, TARSKI:def 4;

            reconsider A1 as Subset of S by A8;

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

             A9: A1 = [:X2, Y2:] and

             A10: X2 is open and

             A11: Y2 is open by A5, A8;

            X2 in the topology of XV by A10, PRE_TOPC:def 2;

            then

            consider Q1 be Subset of X such that

             A12: Q1 in the topology of X and

             A13: X2 = (Q1 /\ ( [#] XV)) by PRE_TOPC:def 4;

            consider p1,p2 be object such that

             A14: p1 in X2 and

             A15: p2 in Y2 & p = [p1, p2] by A7, A9, ZFMISC_1:def 2;

            reconsider Q1 as Subset of X;

            set EX = [:Q1, Y2:];

            p1 in Q1 by A14, A13, XBOOLE_0:def 4;

            then

             A16: p in EX by A15, ZFMISC_1: 87;

            Q1 is open by A12, PRE_TOPC:def 2;

            then EX in { [:Xx1, Yy2:] where Xx1 be Subset of X, Yy2 be Subset of Y : ex Z1 be Subset of XV st Z1 = (Xx1 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Z1, Yy2:] in A } by A8, A9, A11, A13;

            then p in ( union AA) by A16, TARSKI:def 4;

            hence thesis by A7, A8, XBOOLE_0:def 4;

          end;

          AA c= the topology of T

          proof

            let t be object;

            set A9 = {t};

            assume t in AA;

            then

            consider Xx1 be Subset of X, Yy2 be Subset of Y such that

             A17: t = [:Xx1, Yy2:] and

             A18: ex Y1 be Subset of XV st Y1 = (Xx1 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Y1, Yy2:] in A;

            A9 c= ( bool the carrier of T)

            proof

              let a be object;

              assume a in A9;

              then a = t by TARSKI:def 1;

              hence thesis by A17;

            end;

            then

            reconsider A9 as Subset-Family of T;



             A19: A9 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 x be object;

              assume x in A9;

              then

               A20: x = [:Xx1, Yy2:] by A17, TARSKI:def 1;

              Xx1 in the topology of X & Yy2 in the topology of Y by A18, PRE_TOPC:def 2;

              hence thesis by A20;

            end;

            t = ( union A9);

            then t in { ( union As) where As be Subset-Family of T : As 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 A19;

            hence thesis by BORSUK_1:def 2;

          end;

          then

           A21: ( union AA) in the topology of T by PRE_TOPC:def 1;

          (( union AA) /\ ( [#] S)) c= P

          proof

            let h be object;

            assume

             A22: h in (( union AA) /\ ( [#] S));

            then h in ( union AA) by XBOOLE_0:def 4;

            then

            consider A2 be set such that

             A23: h in A2 and

             A24: A2 in AA by TARSKI:def 4;

            consider Xx1 be Subset of X, Yy2 be Subset of Y such that

             A25: A2 = [:Xx1, Yy2:] and

             A26: ex Y1 be Subset of XV st Y1 = (Xx1 /\ ( [#] XV)) & Xx1 is open & Yy2 is open & [:Y1, Yy2:] in A by A24;

            consider Yy1 be Subset of XV such that

             A27: Yy1 = (Xx1 /\ ( [#] XV)) and Xx1 is open and Yy2 is open and

             A28: [:Yy1, Yy2:] in A by A26;

            consider p1,p2 be object such that

             A29: p1 in Xx1 and

             A30: p2 in Yy2 and

             A31: h = [p1, p2] by A23, A25, ZFMISC_1:def 2;

            p1 in the carrier of XV by A1, A22, A31, ZFMISC_1: 87;

            then p1 in (Xx1 /\ ( [#] XV)) by A29, XBOOLE_0:def 4;

            then h in [:Yy1, Yy2:] by A30, A31, A27, ZFMISC_1: 87;

            hence thesis by A4, A28, TARSKI:def 4;

          end;

          then P = (( union AA) /\ ( [#] S)) by A6;

          hence ex Q be Subset of T st Q in the topology of T & P = (Q /\ ( [#] S)) by A21;

        end;

        given Q be Subset of T such that

         A32: Q in the topology of T and

         A33: P = (Q /\ ( [#] S));

        reconsider Q9 = Q as Subset of T;

        Q9 is open by A32, PRE_TOPC:def 2;

        then

        consider A be Subset-Family of T such that

         A34: Q9 = ( union A) and

         A35: for e be set 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 BORSUK_1: 5;

        reconsider A as Subset-Family of T;

        reconsider AA = (A | oS) as Subset-Family of (T | oS);

        reconsider AA as Subset-Family of S by PRE_TOPC: 8;

        reconsider AA as Subset-Family of S;



         A36: for e be set st e in AA holds ex X1 be Subset of XV, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open

        proof

          let e be set;

          assume

           A37: e in AA;

          then

          reconsider e9 = e as Subset of (T | oS);

          consider R be Subset of T such that

           A38: R in A and

           A39: (R /\ oS) = e9 by A37, TOPS_2:def 3;

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

           A40: R = [:X1, Y1:] and

           A41: X1 is open and

           A42: Y1 is open by A35, A38;

          reconsider D2 = (X1 /\ ( [#] XV)) as Subset of XV;

          X1 in the topology of X by A41, PRE_TOPC:def 2;

          then D2 in the topology of XV by PRE_TOPC:def 4;

          then

           A43: D2 is open by PRE_TOPC:def 2;

          ( [#] [:XV, Y:]) = [:( [#] XV), ( [#] Y):] by BORSUK_1:def 2;

          then e9 = [:(X1 /\ ( [#] XV)), (Y1 /\ ( [#] Y)):] by A39, A40, ZFMISC_1: 100;

          hence thesis by A42, A43;

        end;



         A44: (( union A) /\ oS) c= ( union AA)

        proof

          let s be object;

          assume

           A45: s in (( union A) /\ oS);

          then s in ( union A) by XBOOLE_0:def 4;

          then

          consider A1 be set such that

           A46: s in A1 and

           A47: A1 in A by TARSKI:def 4;

          s in oS by A45, XBOOLE_0:def 4;

          then

           A48: s in (A1 /\ oS) by A46, XBOOLE_0:def 4;

          reconsider A1 as Subset of T by A47;

          (A1 /\ oS) in AA by A47, TOPS_2: 31;

          hence thesis by A48, TARSKI:def 4;

        end;

        ( union AA) c= ( union A) by TOPS_2: 34;

        then ( union AA) c= (( union A) /\ oS) by XBOOLE_1: 19;

        then P = ( union AA) by A33, A34, A44;

        then P9 is open by A36, BORSUK_1: 5;

        hence thesis by PRE_TOPC:def 2;

      end;

      ( [#] S) c= ( [#] T) by A1, A2, ZFMISC_1: 96;

      hence thesis by A3, PRE_TOPC:def 4;

    end;

    theorem :: BORSUK_3:21



     Th21: for X,Y be TopSpace, XV be SubSpace of X, YV be SubSpace of Y holds [:XV, YV:] is SubSpace of [:X, Y:]

    proof

      let X,Y be TopSpace, XV be SubSpace of X, YV be SubSpace of Y;

       [:XV, Y:] is SubSpace of [:X, Y:] & [:XV, YV:] is SubSpace of [:XV, Y:] by Lm6, Th15;

      hence thesis by TSEP_1: 7;

    end;

    theorem :: BORSUK_3:22



     Th22: for X,Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X, W be Subset of Y st Z = [:W, V:] holds the TopStruct of [:(Y | W), (X | V):] = the TopStruct of ( [:Y, X:] | Z)

    proof

      let X,Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X, W be Subset of Y;

      reconsider A = [:(Y | W), (X | V):] as SubSpace of [:Y, X:] by Th21;

      assume

       A1: Z = [:W, V:];

      the carrier of A = [:the carrier of (Y | W), the carrier of (X | V):] by BORSUK_1:def 2

      .= [:the carrier of (Y | W), V:] by PRE_TOPC: 8

      .= Z by A1, PRE_TOPC: 8

      .= the carrier of ( [:Y, X:] | Z) by PRE_TOPC: 8;

      then A is SubSpace of ( [:Y, X:] | Z) & ( [:Y, X:] | Z) is SubSpace of A by TOPMETR: 3;

      hence thesis by TSEP_1: 6;

    end;

    registration

      let T be TopSpace;

      cluster empty for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    registration

      let T be TopSpace, P be compact Subset of T;

      cluster (T | P) -> compact;

      coherence

      proof

        per cases ;

          suppose P is non empty;

          hence thesis by COMPTS_1: 3;

        end;

          suppose P is empty;

          hence thesis;

        end;

      end;

    end

    theorem :: BORSUK_3:23

    for T1,T2 be TopSpace, S1 be Subset of T1, S2 be Subset of T2 st S1 is compact & S2 is compact holds [:S1, S2:] is compact Subset of [:T1, T2:]

    proof

      let T1,T2 be TopSpace, S1 be Subset of T1, S2 be Subset of T2;

      assume that

       A1: S1 is compact and

       A2: S2 is compact;

      per cases ;

        suppose

         A3: S1 is non empty & S2 is non empty;

        then (ex x be object st x in S1) & ex y be object st y in S2;

        then

        reconsider T1, T2 as non empty TopSpace;

        reconsider S2 as compact non empty Subset of T2 by A2, A3;

        reconsider S1 as compact non empty Subset of T1 by A1, A3;

        reconsider X = [:S1, S2:] as Subset of [:T1, T2:];

         the TopStruct of [:(T1 | S1), (T2 | S2):] = the TopStruct of ( [:T1, T2:] | X) by Th22;

        hence thesis by COMPTS_1: 3;

      end;

        suppose S1 is empty & S2 is non empty;

        then

        reconsider S1 as empty Subset of T1;

         [:S1, S2:] = ( {} [:T1, T2:]);

        hence thesis;

      end;

        suppose S1 is non empty & S2 is empty;

        then

        reconsider S2 as empty Subset of T2;

         [:S1, S2:] = ( {} [:T1, T2:]);

        hence thesis;

      end;

        suppose S1 is empty & S2 is empty;

        then

        reconsider S2 as empty Subset of T2;

         [:S1, S2:] = ( {} [:T1, T2:]);

        hence thesis;

      end;

    end;