compts_1.miz



    begin

    reserve x,y,z for set,

T for TopStruct,

A for SubSpace of T,

P,Q for Subset of T;

    definition

      let T be TopStruct;

      :: COMPTS_1:def1

      attr T is compact means for F be Subset-Family of T st F is Cover of T & F is open holds ex G be Subset-Family of T st G c= F & G is Cover of T & G is finite;

    end

    definition

      let T be non empty TopSpace;

      :: original: regular

      redefine

      :: COMPTS_1:def2

      attr T is regular means for p be Point of T, P be Subset of T st P <> {} & P is closed & p in (P ` ) holds ex W,V be Subset of T st W is open & V is open & p in W & P c= V & W misses V;

      compatibility

      proof

        thus T is regular implies for p be Point of T, P be Subset of T st P <> {} & P is closed & p in (P ` ) holds ex W,V be Subset of T st W is open & V is open & p in W & P c= V & W misses V;

        assume

         A1: for p be Point of T, P be Subset of T st P <> {} & P is closed & p in (P ` ) holds ex W,V be Subset of T st W is open & V is open & p in W & P c= V & W misses V;

        let p be Point of T, P be Subset of T;

        assume that

         A2: P is closed and

         A3: p in (P ` );

        per cases ;

          suppose

           A4: P = {} ;

          take G1 = ( [#] T), G2 = ( {} T);

          thus G1 is open & G2 is open;

          thus p in G1;

          thus thesis by A4;

        end;

          suppose P <> {} ;

          hence thesis by A1, A2, A3;

        end;

      end;

      :: original: normal

      redefine

      :: COMPTS_1:def3

      attr T is normal means for W,V be Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P,Q be Subset of T st P is open & Q is open & W c= P & V c= Q & P misses Q;

      compatibility

      proof

        thus T is normal implies for W,V be Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P,Q be Subset of T st P is open & Q is open & W c= P & V c= Q & P misses Q;

        assume

         A5: for W,V be Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P,Q be Subset of T st P is open & Q is open & W c= P & V c= Q & P misses Q;

        let F1,F2 be Subset of T such that

         A6: F1 is closed and

         A7: F2 is closed and

         A8: F1 misses F2;

        per cases ;

          suppose

           A9: F1 = {} ;

          take G1 = ( {} T), G2 = ( [#] T);

          thus G1 is open & G2 is open;

          thus F1 c= G1 by A9;

          thus F2 c= G2;

          thus thesis;

        end;

          suppose

           A10: F2 = {} ;

          take G1 = ( [#] T), G2 = ( {} T);

          thus G1 is open & G2 is open;

          thus F1 c= G1;

          thus F2 c= G2 by A10;

          thus thesis;

        end;

          suppose F1 <> {} & F2 <> {} ;

          hence thesis by A5, A6, A7, A8;

        end;

      end;

    end

    notation

      let T be TopStruct;

      synonym T is Hausdorff for T is T_2;

    end

    definition

      let T be TopStruct, P be Subset of T;

      :: COMPTS_1:def4

      attr P is compact means

      : Def4: for F be Subset-Family of T st F is Cover of P & F is open holds ex G be Subset-Family of T st G c= F & G is Cover of P & G is finite;

    end

    registration

      let T;

      cluster empty -> compact for Subset of T;

      coherence

      proof

        reconsider C = {} as Subset-Family of T by XBOOLE_1: 2;

        let S be Subset of T;

        assume S is empty;

        then

         A1: S c= ( union C);

        let F be Subset-Family of T such that F is Cover of S and F is open;

        take C;

        thus thesis by A1, SETFAM_1:def 11;

      end;

    end

    theorem :: COMPTS_1:1

    T is compact iff ( [#] T) is compact;

    theorem :: COMPTS_1:2

    

     Th2: Q c= ( [#] A) implies (Q is compact iff for P be Subset of A st P = Q holds P is compact)

    proof

      ( [#] A) c= ( [#] T) by PRE_TOPC:def 4;

      then

      reconsider AA = ( [#] A) as Subset of T;

      assume

       A1: Q c= ( [#] A);

      then

       A2: (Q /\ AA) = Q by XBOOLE_1: 28;

      thus Q is compact implies for P be Subset of A st P = Q holds P is compact

      proof

        assume

         A3: Q is compact;

        let P be Subset of A such that

         A4: P = Q;

        thus P is compact

        proof

          let G be Subset-Family of A;

          set GG = G;

          assume that

           A5: G is Cover of P and

           A6: G is open;

          consider F be Subset-Family of T such that

           A7: F is open and

           A8: for AA be Subset of T st AA = ( [#] A) holds GG = (F | AA) by A6, TOPS_2: 39;

          

           A9: Q c= ( union G) by A4, A5, SETFAM_1:def 11;

          ( union (F | AA)) c= ( union F) by TOPS_2: 34;

          then ( union G) c= ( union F) by A8;

          then Q c= ( union F) by A9;

          then F is Cover of Q by SETFAM_1:def 11;

          then

          consider F9 be Subset-Family of T such that

           A10: F9 c= F and

           A11: F9 is Cover of Q and

           A12: F9 is finite by A3, A7;

          (F9 | AA) c= ( bool ( [#] (T | AA)));

          then

          reconsider G9 = (F9 | AA) as Subset-Family of A by PRE_TOPC:def 5;

          take G9;

          (F9 | AA) c= (F | AA) by A10, TOPS_2: 30;

          hence G9 c= G by A8;

          Q c= ( union F9) by A11, SETFAM_1:def 11;

          then P c= ( union G9) by A2, A4, TOPS_2: 32;

          hence G9 is Cover of P by SETFAM_1:def 11;

          thus thesis by A12, TOPS_2: 36;

        end;

      end;

      thus (for P be Subset of A st P = Q holds P is compact) implies Q is compact

      proof

        reconsider QQ = Q as Subset of A by A1;

        assume for P be Subset of A st P = Q holds P is compact;

        then

         A13: QQ is compact;

        thus Q is compact

        proof

          let F be Subset-Family of T;

          set F9 = F;

          assume that

           A14: F is Cover of Q and

           A15: F is open;

          consider f be Function such that

           A16: ( dom f) = F9 and

           A17: ( rng f) = (F9 | AA) and

           A18: for x st x in F holds for Q be Subset of T st Q = x holds (f . x) = (Q /\ AA) by TOPS_2: 40;

          (F9 | AA) c= ( bool ( [#] (T | AA)));

          then

          reconsider F9 = ( rng f) as Subset-Family of A by A17, PRE_TOPC:def 5;

          

           A19: F9 is open

          proof

            let X be Subset of A;

            assume

             A20: X in F9;

            then

            reconsider Y = X as Subset of (T | AA) by A17;

            consider R be Subset of T such that

             A21: R in F and

             A22: (R /\ AA) = Y by A17, A20, TOPS_2:def 3;

            R is open by A15, A21;

            then R in the topology of T;

            then X in the topology of A by A22, PRE_TOPC:def 4;

            hence thesis;

          end;

          Q c= ( union F) by A14, SETFAM_1:def 11;

          then QQ c= ( union F9) by A2, A17, TOPS_2: 32;

          then F9 is Cover of QQ by SETFAM_1:def 11;

          then

          consider G be Subset-Family of A such that

           A23: G c= F9 and

           A24: G is Cover of QQ and

           A25: G is finite by A13, A19;

          consider X be set such that

           A26: X c= ( dom f) and

           A27: X is finite and

           A28: (f .: X) = G by A23, A25, ORDERS_1: 85;

          reconsider G9 = X as Subset-Family of T by A16, A26, TOPS_2: 2;

          take G9;

          Q c= ( union G9)

          proof

            let x be object;

            assume

             A29: x in Q;

            QQ c= ( union G) by A24, SETFAM_1:def 11;

            then

            consider Y be set such that

             A30: x in Y and

             A31: Y in G by A29, TARSKI:def 4;

            consider z be object such that

             A32: z in ( dom f) and

             A33: z in X and

             A34: (f . z) = Y by A28, A31, FUNCT_1:def 6;

            reconsider Z = z as Subset of T by A16, A32;

            Y = (Z /\ AA) by A16, A18, A32, A34;

            then x in Z by A30, XBOOLE_0:def 4;

            hence thesis by A33, TARSKI:def 4;

          end;

          hence thesis by A16, A26, A27, SETFAM_1:def 11;

        end;

      end;

    end;

    theorem :: COMPTS_1:3

    

     Th3: (P = {} implies (P is compact iff (T | P) is compact)) & (T is TopSpace-like & P <> {} implies (P is compact iff (T | P) is compact))

    proof

      

       A1: ( [#] (T | P)) = P by PRE_TOPC:def 5;

      thus P = {} implies (P is compact iff (T | P) is compact);

      assume that

       A2: T is TopSpace-like and

       A3: P <> {} ;

      reconsider T9 = T as non empty TopSpace by A2, A3;

      reconsider P9 = P as non empty Subset of T9 by A3;

      

       A4: ( [#] (T9 | P9)) is compact iff (T9 | P9) is compact;

      hence P is compact implies (T | P) is compact by A1, Th2;

      assume (T | P) is compact;

      then for Q be Subset of (T | P) st Q = P holds Q is compact by A4, PRE_TOPC:def 5;

      hence thesis by A1, Th2;

    end;

    theorem :: COMPTS_1:4

    

     Th4: for T be non empty TopSpace holds T is compact iff for F be Subset-Family of T st F is centered & F is closed holds ( meet F) <> {}

    proof

      let T be non empty TopSpace;

      thus T is compact implies for F be Subset-Family of T st F is centered & F is closed holds ( meet F) <> {}

      proof

        assume

         A1: T is compact;

        let F be Subset-Family of T such that

         A2: F is centered and

         A3: F is closed;

        reconsider C = ( COMPLEMENT F) as Subset-Family of T;

        assume

         A4: ( meet F) = {} ;

        F <> {} by A2, FINSET_1:def 3;

        

        then ( union ( COMPLEMENT F)) = (( meet F) ` ) by TOPS_2: 7

        .= ( [#] T) by A4;

        then

         A5: ( COMPLEMENT F) is Cover of T by SETFAM_1:def 11;

        ( COMPLEMENT F) is open by A3, TOPS_2: 9;

        then

        consider G9 be Subset-Family of T such that

         A6: G9 c= C and

         A7: G9 is Cover of T and

         A8: G9 is finite by A1, A5;

        set F9 = ( COMPLEMENT G9);

        

         A9: F9 is finite by A8, TOPS_2: 8;

        

         A10: F9 c= F

        proof

          let X be object;

          assume

           A11: X in F9;

          then

          reconsider X1 = X as Subset of T;

          (X1 ` ) in G9 by A11, SETFAM_1:def 7;

          then ((X1 ` ) ` ) in F by A6, SETFAM_1:def 7;

          hence thesis;

        end;

        G9 <> {} by A7, TOPS_2: 3;

        then

         A12: F9 <> {} by TOPS_2: 5;

        ( meet F9) = (( union G9) ` ) by A7, TOPS_2: 3, TOPS_2: 6

        .= (( [#] T) \ ( [#] T)) by A7, SETFAM_1: 45

        .= {} by XBOOLE_1: 37;

        hence contradiction by A2, A10, A9, A12, FINSET_1:def 3;

      end;

      assume

       A13: for F be Subset-Family of T st F is centered & F is closed holds ( meet F) <> {} ;

      thus T is compact

      proof

        let F be Subset-Family of T such that

         A14: F is Cover of T and

         A15: F is open;

        reconsider G = ( COMPLEMENT F) as Subset-Family of T;

        

         A16: G is closed by A15, TOPS_2: 10;

        F <> {} by A14, TOPS_2: 3;

        then

         A17: G <> {} by TOPS_2: 5;

        ( meet G) = (( union F) ` ) by A14, TOPS_2: 3, TOPS_2: 6

        .= (( [#] T) \ ( [#] T)) by A14, SETFAM_1: 45

        .= {} by XBOOLE_1: 37;

        then not G is centered by A13, A16;

        then

        consider G9 be set such that

         A18: G9 <> {} and

         A19: G9 c= G and

         A20: G9 is finite and

         A21: ( meet G9) = {} by A17, FINSET_1:def 3;

        reconsider G9 as Subset-Family of T by A19, XBOOLE_1: 1;

        take F9 = ( COMPLEMENT G9);

        thus F9 c= F

        proof

          let A be object;

          assume

           A22: A in F9;

          then

          reconsider A1 = A as Subset of T;

          (A1 ` ) in G9 by A22, SETFAM_1:def 7;

          then ((A1 ` ) ` ) in F by A19, SETFAM_1:def 7;

          hence thesis;

        end;

        ( union F9) = (( meet G9) ` ) by A18, TOPS_2: 7

        .= ( [#] T) by A21;

        hence F9 is Cover of T by SETFAM_1:def 11;

        thus thesis by A20, TOPS_2: 8;

      end;

    end;

    theorem :: COMPTS_1:5

    for T be non empty TopSpace holds T is compact iff for F be Subset-Family of T st F <> {} & F is closed & ( meet F) = {} holds ex G be Subset-Family of T st G <> {} & G c= F & G is finite & ( meet G) = {}

    proof

      let T be non empty TopSpace;

      thus T is compact implies for F be Subset-Family of T st F <> {} & F is closed & ( meet F) = {} holds ex G be Subset-Family of T st G <> {} & G c= F & G is finite & ( meet G) = {}

      proof

        assume

         A1: T is compact;

        let F be Subset-Family of T such that

         A2: F <> {} and

         A3: F is closed and

         A4: ( meet F) = {} ;

         not F is centered by A1, A3, A4, Th4;

        then

        consider G be set such that

         A5: G <> {} and

         A6: G c= F and

         A7: G is finite and

         A8: ( meet G) = {} by A2, FINSET_1:def 3;

        reconsider G as Subset-Family of T by A6, XBOOLE_1: 1;

        take G;

        thus thesis by A5, A6, A7, A8;

      end;

      assume

       A9: for F be Subset-Family of T st F <> {} & F is closed & ( meet F) = {} holds ex G be Subset-Family of T st G <> {} & G c= F & G is finite & ( meet G) = {} ;

      for F be Subset-Family of T st F is centered & F is closed holds ( meet F) <> {}

      proof

        let F be Subset-Family of T;

        assume that

         A10: F is centered and

         A11: F is closed;

        assume

         A12: ( meet F) = {} ;

        F <> {} by A10, FINSET_1:def 3;

        then ex G be Subset-Family of T st G <> {} & G c= F & G is finite & ( meet G) = {} by A9, A11, A12;

        hence contradiction by A10, FINSET_1:def 3;

      end;

      hence thesis by Th4;

    end;

    reserve TS for TopSpace;

    reserve PS,QS for Subset of TS;

    theorem :: COMPTS_1:6

    

     Th6: TS is T_2 implies for A be Subset of TS st A <> {} & A is compact holds for p be Point of TS st p in (A ` ) holds ex PS, QS st PS is open & QS is open & p in PS & A c= QS & PS misses QS

    proof

      assume

       A1: TS is T_2;

      let F be Subset of TS such that

       A2: F <> {} and

       A3: F is compact;

      set z = the Element of F;

      let a be Point of TS;

      assume a in (F ` );

      then

       A4: not a in F by XBOOLE_0:def 5;

      defpred P[ object, object, object] means ex PS, QS st $2 = PS & $3 = QS & PS is open & QS is open & a in PS & $1 in QS & (PS /\ QS) = {} ;

      

       A5: for x be object holds x in F implies ex y,z be object st y in the topology of TS & z in the topology of TS & P[x, y, z]

      proof

        let x be object;

        assume

         A6: x in F;

        then

        reconsider p = x as Point of TS;

        consider W,V be Subset of TS such that

         A7: W is open and

         A8: V is open and

         A9: a in W and

         A10: p in V and

         A11: W misses V by A1, A4, A6;

        reconsider PS = W, QS = V as set;

        take PS, QS;

        thus PS in the topology of TS & QS in the topology of TS by A7, A8;

        take W, V;

        thus thesis by A7, A8, A9, A10, A11;

      end;

      consider f,g be Function such that

       A12: ( dom f) = F & ( dom g) = F and

       A13: for x be object st x in F holds P[x, (f . x), (g . x)] from MCART_1:sch 1( A5);

      (g .: F) c= ( bool the carrier of TS)

      proof

        let x be object;

        assume x in (g .: F);

        then

        consider y be object such that y in ( dom g) and

         A14: y in F and

         A15: (g . y) = x by FUNCT_1:def 6;

        ex PS, QS st (f . y) = PS & (g . y) = QS & PS is open & QS is open & a in PS & y in QS & (PS /\ QS) = {} by A13, A14;

        hence thesis by A15;

      end;

      then

      reconsider C = (g .: F) as Subset-Family of TS;

      

       A16: C is open

      proof

        let G be Subset of TS;

        assume G in C;

        then

        consider x be object such that x in ( dom g) and

         A17: x in F and

         A18: G = (g . x) by FUNCT_1:def 6;

        ex PS, QS st (f . x) = PS & (g . x) = QS & PS is open & QS is open & a in PS & x in QS & (PS /\ QS) = {} by A13, A17;

        hence thesis by A18;

      end;

      F c= ( union C)

      proof

        let x be object;

        assume

         A19: x in F;

        then

        consider PS, QS such that (f . x) = PS and

         A20: (g . x) = QS and PS is open and QS is open and a in PS and

         A21: x in QS and (PS /\ QS) = {} by A13;

        QS in C by A12, A19, A20, FUNCT_1:def 6;

        hence thesis by A21, TARSKI:def 4;

      end;

      then C is Cover of F by SETFAM_1:def 11;

      then

      consider C9 be Subset-Family of TS such that

       A22: C9 c= C and

       A23: C9 is Cover of F and

       A24: C9 is finite by A3, A16;

      C9 c= ( rng g) by A12, A22, RELAT_1: 113;

      then

      consider H9 be set such that

       A25: H9 c= ( dom g) and

       A26: H9 is finite and

       A27: (g .: H9) = C9 by A24, ORDERS_1: 85;

      (f .: H9) c= ( bool the carrier of TS)

      proof

        let x be object;

        assume x in (f .: H9);

        then

        consider y be object such that y in ( dom f) and

         A28: y in H9 and

         A29: (f . y) = x by FUNCT_1:def 6;

        ex PS, QS st (f . y) = PS & (g . y) = QS & PS is open & QS is open & a in PS & y in QS & (PS /\ QS) = {} by A12, A13, A25, A28;

        hence thesis by A29;

      end;

      then

      reconsider B = (f .: H9) as Subset-Family of TS;

      take G0 = ( meet B), G1 = ( union C9);

      B is open

      proof

        let G be Subset of TS;

        assume G in B;

        then

        consider x be object such that

         A30: x in ( dom f) and x in H9 and

         A31: G = (f . x) by FUNCT_1:def 6;

        ex PS, QS st (f . x) = PS & (g . x) = QS & PS is open & QS is open & a in PS & x in QS & (PS /\ QS) = {} by A12, A13, A30;

        hence thesis by A31;

      end;

      hence G0 is open by A26, TOPS_2: 20;

      thus G1 is open by A16, A22, TOPS_2: 11, TOPS_2: 19;

      

       A32: for G be set st G in B holds a in G

      proof

        let G be set;

        assume

         A33: G in B;

        then

        reconsider G9 = G as Subset of TS;

        consider x be object such that

         A34: x in ( dom f) and x in H9 and

         A35: G9 = (f . x) by A33, FUNCT_1:def 6;

        ex PS, QS st (f . x) = PS & (g . x) = QS & PS is open & QS is open & a in PS & x in QS & (PS /\ QS) = {} by A12, A13, A34;

        hence thesis by A35;

      end;

      F c= ( union C9) by A23, SETFAM_1:def 11;

      then z in ( union C9) by A2;

      then

      consider D be set such that z in D and

       A36: D in C9 by TARSKI:def 4;

      reconsider D9 = D as Subset of TS by A36;

      consider y be object such that

       A37: y in ( dom g) and

       A38: y in H9 and D9 = (g . y) by A27, A36, FUNCT_1:def 6;

      ex PS, QS st (f . y) = PS & (g . y) = QS & PS is open & QS is open & a in PS & y in QS & (PS /\ QS) = {} by A12, A13, A37;

      then B <> {} by A12, A37, A38, FUNCT_1:def 6;

      hence a in G0 by A32, SETFAM_1:def 1;

      thus F c= G1 by A23, SETFAM_1:def 11;

      thus (G0 /\ G1) = {}

      proof

        set x = the Element of (( meet B) /\ ( union C9));

        assume

         A39: (G0 /\ G1) <> {} ;

        then

         A40: x in ( meet B) by XBOOLE_0:def 4;

        x in ( union C9) by A39, XBOOLE_0:def 4;

        then

        consider A be set such that

         A41: x in A and

         A42: A in C9 by TARSKI:def 4;

        consider z be object such that

         A43: z in ( dom g) and

         A44: z in H9 and

         A45: A = (g . z) by A27, A42, FUNCT_1:def 6;

        consider PS, QS such that

         A46: (f . z) = PS and

         A47: (g . z) = QS and PS is open and QS is open and a in PS and z in QS and

         A48: (PS /\ QS) = {} by A12, A13, A43;

        PS in B by A12, A43, A44, A46, FUNCT_1:def 6;

        then x in PS by A40, SETFAM_1:def 1;

        hence contradiction by A41, A45, A47, A48, XBOOLE_0:def 4;

      end;

    end;

    theorem :: COMPTS_1:7

    

     Th7: TS is T_2 & PS is compact implies PS is closed

    proof

      assume that

       A1: TS is T_2 and

       A2: PS is compact;

      per cases ;

        suppose PS = {} ;

        hence thesis;

      end;

        suppose

         A3: PS <> {} ;

        now

          let a be set;

          thus a in (PS ` ) implies ex Q be Subset of TS st Q is open & Q c= (PS ` ) & a in Q

          proof

            assume

             A4: a in (PS ` );

            then

            reconsider p = a as Point of TS;

            consider W,V be Subset of TS such that

             A5: W is open and V is open and

             A6: p in W and

             A7: PS c= V and

             A8: W misses V by A1, A2, A3, A4, Th6;

            take Q = W;

            W misses ((V ` ) ` ) by A8;

            then

             A9: W c= (V ` ) by SUBSET_1: 24;

            (V ` ) c= (PS ` ) by A7, SUBSET_1: 12;

            hence thesis by A5, A6, A9;

          end;

          thus (ex Q be Subset of TS st Q is open & Q c= (PS ` ) & a in Q) implies a in (PS ` );

        end;

        then (PS ` ) is open by TOPS_1: 25;

        hence thesis;

      end;

    end;

    theorem :: COMPTS_1:8

    

     Th8: T is compact & P is closed implies P is compact

    proof

      assume that

       A1: T is compact and

       A2: P is closed;

      reconsider pp = {(P ` )} as Subset-Family of T;

      let F be Subset-Family of T such that

       A3: F is Cover of P and

       A4: F is open;

      set FP = (F \/ pp);

      

       A5: (P ` ) is open by A2;

      

       A6: FP is open

      proof

        let H be Subset of T;

        assume H in FP;

        then H in F or H in {(P ` )} by XBOOLE_0:def 3;

        hence thesis by A4, A5, TARSKI:def 1;

      end;

      reconsider M = {(P ` )} as Subset-Family of T;

      ((F \/ {(P ` )}) \ {(P ` )}) = (F \ {(P ` )}) by XBOOLE_1: 40;

      then

       A7: ((F \/ {(P ` )}) \ {(P ` )}) c= F by XBOOLE_1: 36;

      P c= ( union F) by A3, SETFAM_1:def 11;

      then (P \/ (P ` )) c= (( union F) \/ (P ` )) by XBOOLE_1: 9;

      then ( [#] T) c= (( union F) \/ (P ` )) by PRE_TOPC: 2;

      

      then ( [#] T) = (( union F) \/ (P ` ))

      .= (( union F) \/ ( union {(P ` )})) by ZFMISC_1: 25

      .= ( union (F \/ {(P ` )})) by ZFMISC_1: 78;

      then FP is Cover of T by SETFAM_1:def 11;

      then

      consider G be Subset-Family of T such that

       A8: G c= FP and

       A9: G is Cover of T and

       A10: G is finite by A1, A6;

      reconsider G9 = (G \ pp) as Subset-Family of T;

      take G9;

      G9 c= ((F \/ {(P ` )}) \ {(P ` )}) by A8, XBOOLE_1: 33;

      hence G9 c= F by A7;

      (( union G) \ ( union M)) = (( [#] T) \ ( union {(P ` )})) by A9, SETFAM_1: 45

      .= ((P ` ) ` ) by ZFMISC_1: 25

      .= P;

      then P c= ( union G9) by TOPS_2: 4;

      hence G9 is Cover of P by SETFAM_1:def 11;

      thus thesis by A10;

    end;

    theorem :: COMPTS_1:9

    

     Th9: PS is compact & QS c= PS & QS is closed implies QS is compact

    proof

      assume that

       A1: PS is compact and

       A2: QS c= PS and

       A3: QS is closed;

      per cases ;

        suppose PS = {} ;

        hence thesis by A2;

      end;

        suppose PS <> {} ;

        then (TS | PS) is compact by A1, Th3;

        then

         A4: for QQ be Subset of (TS | PS) st QQ = QS holds QQ is compact by A3, Th8, TOPS_2: 26;

        PS = ( [#] (TS | PS)) by PRE_TOPC:def 5;

        hence thesis by A2, A4, Th2;

      end;

    end;

    theorem :: COMPTS_1:10

    P is compact & Q is compact implies (P \/ Q) is compact

    proof

      assume that

       A1: P is compact and

       A2: Q is compact;

      let F be Subset-Family of T such that

       A3: F is Cover of (P \/ Q) and

       A4: F is open;

      

       A5: (P \/ Q) c= ( union F) by A3, SETFAM_1:def 11;

      Q c= (P \/ Q) by XBOOLE_1: 7;

      then Q c= ( union F) by A5;

      then F is Cover of Q by SETFAM_1:def 11;

      then

      consider G2 be Subset-Family of T such that

       A6: G2 c= F and

       A7: G2 is Cover of Q and

       A8: G2 is finite by A2, A4;

      

       A9: Q c= ( union G2) by A7, SETFAM_1:def 11;

      P c= (P \/ Q) by XBOOLE_1: 7;

      then P c= ( union F) by A5;

      then F is Cover of P by SETFAM_1:def 11;

      then

      consider G1 be Subset-Family of T such that

       A10: G1 c= F and

       A11: G1 is Cover of P and

       A12: G1 is finite by A1, A4;

      reconsider G = (G1 \/ G2) as Subset-Family of T;

      take G;

      thus G c= F by A10, A6, XBOOLE_1: 8;

      P c= ( union G1) by A11, SETFAM_1:def 11;

      then (P \/ Q) c= (( union G1) \/ ( union G2)) by A9, XBOOLE_1: 13;

      then (P \/ Q) c= ( union (G1 \/ G2)) by ZFMISC_1: 78;

      hence G is Cover of (P \/ Q) by SETFAM_1:def 11;

      thus thesis by A12, A8;

    end;

    theorem :: COMPTS_1:11

    TS is T_2 & PS is compact & QS is compact implies (PS /\ QS) is compact

    proof

      assume that

       A1: TS is T_2 and

       A2: PS is compact and

       A3: QS is compact;

      

       A4: QS is closed by A1, A3, Th7;

      PS is closed by A1, A2, Th7;

      hence thesis by A2, A4, Th9, XBOOLE_1: 17;

    end;

    theorem :: COMPTS_1:12

    for TS be non empty TopSpace holds TS is T_2 & TS is compact implies TS is regular by Th6, Th8;

    theorem :: COMPTS_1:13

    for TS be non empty TopSpace holds TS is T_2 & TS is compact implies TS is normal

    proof

      let TS be non empty TopSpace;

      assume that

       A1: TS is T_2 and

       A2: TS is compact;

      let A,B be Subset of TS such that

       A3: A <> {} and

       A4: B <> {} and

       A5: A is closed and

       A6: B is closed and

       A7: (A /\ B) = {} ;

      defpred P[ object, object, object] means ex P,Q be Subset of TS st $2 = P & $3 = Q & P is open & Q is open & $1 in P & B c= Q & (P /\ Q) = {} ;

      

       A8: for x be object holds x in A implies ex y,z be object st y in the topology of TS & z in the topology of TS & P[x, y, z]

      proof

        let x be object;

        assume

         A9: x in A;

        then

        reconsider p = x as Point of TS;

         not p in B by A7, A9, XBOOLE_0:def 4;

        then p in (B ` ) by SUBSET_1: 29;

        then

        consider W,V be Subset of TS such that

         A10: W is open and

         A11: V is open and

         A12: p in W and

         A13: B c= V and

         A14: W misses V by A1, A2, A4, A6, Th6, Th8;

        reconsider X = W, Y = V as set;

        take X, Y;

        thus X in the topology of TS & Y in the topology of TS by A10, A11;

        (W /\ V) = {} by A14;

        hence thesis by A10, A11, A12, A13;

      end;

      consider f,g be Function such that

       A15: ( dom f) = A & ( dom g) = A and

       A16: for x be object st x in A holds P[x, (f . x), (g . x)] from MCART_1:sch 1( A8);

      (f .: A) c= ( bool the carrier of TS)

      proof

        let x be object;

        assume x in (f .: A);

        then

        consider y be object such that y in ( dom f) and

         A17: y in A and

         A18: (f . y) = x by FUNCT_1:def 6;

        ex P,Q be Subset of TS st (f . y) = P & (g . y) = Q & P is open & Q is open & y in P & B c= Q & (P /\ Q) = {} by A16, A17;

        hence thesis by A18;

      end;

      then

      reconsider Cf = (f .: A) as Subset-Family of TS;

      A c= ( union Cf)

      proof

        let x be object;

        assume

         A19: x in A;

        then

        consider P,Q be Subset of TS such that

         A20: (f . x) = P and (g . x) = Q and P is open and Q is open and

         A21: x in P and B c= Q and (P /\ Q) = {} by A16;

        P in Cf by A15, A19, A20, FUNCT_1:def 6;

        hence thesis by A21, TARSKI:def 4;

      end;

      then

       A22: Cf is Cover of A by SETFAM_1:def 11;

      

       A23: Cf is open

      proof

        let G be Subset of TS;

        assume G in Cf;

        then

        consider x be object such that x in ( dom f) and

         A24: x in A and

         A25: G = (f . x) by FUNCT_1:def 6;

        ex P,Q be Subset of TS st (f . x) = P & (g . x) = Q & P is open & Q is open & x in P & B c= Q & (P /\ Q) = {} by A16, A24;

        hence thesis by A25;

      end;

      A is compact by A2, A5, Th8;

      then

      consider C be Subset-Family of TS such that

       A26: C c= Cf and

       A27: C is Cover of A and

       A28: C is finite by A22, A23;

      set z = the Element of A;

      A c= ( union C) by A27, SETFAM_1:def 11;

      then z in ( union C) by A3;

      then

      consider D be set such that z in D and

       A29: D in C by TARSKI:def 4;

      C c= ( rng f) by A15, A26, RELAT_1: 113;

      then

      consider H9 be set such that

       A30: H9 c= ( dom f) and

       A31: H9 is finite and

       A32: (f .: H9) = C by A28, ORDERS_1: 85;

      (g .: H9) c= ( bool the carrier of TS)

      proof

        let x be object;

        assume x in (g .: H9);

        then

        consider y be object such that y in ( dom g) and

         A33: y in H9 and

         A34: (g . y) = x by FUNCT_1:def 6;

        ex P,Q be Subset of TS st (f . y) = P & (g . y) = Q & P is open & Q is open & y in P & B c= Q & (P /\ Q) = {} by A15, A16, A30, A33;

        hence thesis by A34;

      end;

      then

      reconsider Bk = (g .: H9) as Subset-Family of TS;

      consider y be object such that

       A35: y in ( dom f) and

       A36: y in H9 and D = (f . y) by A32, A29, FUNCT_1:def 6;

      

       A37: for X be set st X in Bk holds B c= X

      proof

        let X be set;

        assume

         A38: X in Bk;

        then

        reconsider X9 = X as Subset of TS;

        consider x be object such that

         A39: x in ( dom g) and x in H9 and

         A40: X9 = (g . x) by A38, FUNCT_1:def 6;

        ex P,Q be Subset of TS st (f . x) = P & (g . x) = Q & P is open & Q is open & x in P & B c= Q & (P /\ Q) = {} by A15, A16, A39;

        hence thesis by A40;

      end;

      take W = ( union C), V = ( meet Bk);

      thus W is open by A23, A26, TOPS_2: 11, TOPS_2: 19;

      Bk is open

      proof

        let G be Subset of TS;

        assume G in Bk;

        then

        consider x be object such that

         A41: x in ( dom g) and x in H9 and

         A42: G = (g . x) by FUNCT_1:def 6;

        ex P,Q be Subset of TS st (f . x) = P & (g . x) = Q & P is open & Q is open & x in P & B c= Q & (P /\ Q) = {} by A15, A16, A41;

        hence thesis by A42;

      end;

      hence V is open by A31, TOPS_2: 20;

      thus A c= W by A27, SETFAM_1:def 11;

      ex P,Q be Subset of TS st (f . y) = P & (g . y) = Q & P is open & Q is open & y in P & B c= Q & (P /\ Q) = {} by A15, A16, A35;

      then Bk <> {} by A15, A35, A36, FUNCT_1:def 6;

      hence B c= V by A37, SETFAM_1: 5;

      thus (W /\ V) = {}

      proof

        set x = the Element of (( union C) /\ ( meet Bk));

        assume

         A43: (W /\ V) <> {} ;

        then

         A44: x in ( meet Bk) by XBOOLE_0:def 4;

        x in ( union C) by A43, XBOOLE_0:def 4;

        then

        consider D be set such that

         A45: x in D and

         A46: D in C by TARSKI:def 4;

        consider z be object such that

         A47: z in ( dom f) and

         A48: z in H9 and

         A49: D = (f . z) by A32, A46, FUNCT_1:def 6;

        consider P,Q be Subset of TS such that

         A50: (f . z) = P and

         A51: (g . z) = Q and P is open and Q is open and z in P and B c= Q and

         A52: (P /\ Q) = {} by A15, A16, A47;

        Q in Bk by A15, A47, A48, A51, FUNCT_1:def 6;

        then x in Q by A44, SETFAM_1:def 1;

        hence contradiction by A45, A49, A50, A52, XBOOLE_0:def 4;

      end;

    end;

    reserve S for non empty TopStruct;

    reserve f for Function of T, S;

    theorem :: COMPTS_1:14

    T is compact & f is continuous & ( rng f) = ( [#] S) implies S is compact

    proof

      assume

       A1: T is compact;

      ( [#] T) c= ( dom f) by FUNCT_2:def 1;

      then

       A2: ( [#] T) c= (f " (f .: ( [#] T))) by FUNCT_1: 76;

      assume that

       A3: f is continuous and

       A4: ( rng f) = ( [#] S);

      let F be Subset-Family of S such that

       A5: F is Cover of S and

       A6: F is open;

      set F1 = F;

      reconsider G = (( " f) .: F1) as Subset-Family of T by TOPS_2: 42;

      ( union G) = (f " ( union F)) by A4, FUNCT_3: 26

      .= (f " ( rng f)) by A4, A5, SETFAM_1: 45

      .= (f " (f .: ( dom f))) by RELAT_1: 113

      .= (f " (f .: ( [#] T))) by FUNCT_2:def 1;

      then

       A7: G is Cover of T by A2, SETFAM_1:def 11;

      

       A8: (( .: f) .: (( .: f) " F)) c= F by FUNCT_1: 75;

      (( .: f) .: (( " f) .: F)) c= (( .: f) .: (( .: f) " F)) by FUNCT_3: 29, RELAT_1: 123;

      then

       A9: (( .: f) .: G) c= F by A8;

      G is open by A3, A6, TOPS_2: 47;

      then

      consider G9 be Subset-Family of T such that

       A10: G9 c= G and

       A11: G9 is Cover of T and

       A12: G9 is finite by A1, A7;

      reconsider F9 = (( .: f) .: G9) as Subset-Family of S;

      take F9;

      (( .: f) .: G9) c= (( .: f) .: G) by A10, RELAT_1: 123;

      hence F9 c= F by A9;

      ( dom f) = ( [#] T) by FUNCT_2:def 1;

      

      then ( union F9) = (f .: ( union G9)) by FUNCT_3: 14

      .= (f .: ( [#] T)) by A11, SETFAM_1: 45

      .= (f .: ( dom f)) by FUNCT_2:def 1

      .= ( [#] S) by A4, RELAT_1: 113;

      hence F9 is Cover of S by SETFAM_1:def 11;

      thus thesis by A12;

    end;

    theorem :: COMPTS_1:15

    

     Th15: f is continuous & ( rng f) = ( [#] S) & P is compact implies (f .: P) is compact

    proof

      assume that

       A1: f is continuous and

       A2: ( rng f) = ( [#] S) and

       A3: P is compact;

      let F be Subset-Family of S such that

       A4: F is Cover of (f .: P) and

       A5: F is open;

      reconsider G = (( " f) .: F) as Subset-Family of T by TOPS_2: 42;

      (f .: P) c= ( union F) by A4, SETFAM_1:def 11;

      then

       A6: (f " (f .: P)) c= (f " ( union F)) by RELAT_1: 143;

      P c= ( [#] T);

      then P c= ( dom f) by FUNCT_2:def 1;

      then

       A7: P c= (f " (f .: P)) by FUNCT_1: 76;

      ( union G) = (f " ( union F)) by A2, FUNCT_3: 26;

      then P c= ( union G) by A6, A7;

      then

       A8: G is Cover of P by SETFAM_1:def 11;

      G is open by A1, A5, TOPS_2: 47;

      then

      consider G9 be Subset-Family of T such that

       A9: G9 c= G and

       A10: G9 is Cover of P and

       A11: G9 is finite by A3, A8;

      reconsider F9 = (( .: f) .: G9) as Subset-Family of S;

      take F9;

      

       A12: (( .: f) .: (( .: f) " F)) c= F by FUNCT_1: 75;

      (( .: f) .: (( " f) .: F)) c= (( .: f) .: (( .: f) " F)) by FUNCT_3: 29, RELAT_1: 123;

      then

       A13: (( .: f) .: G) c= F by A12;

      (( .: f) .: G9) c= (( .: f) .: G) by A9, RELAT_1: 123;

      hence F9 c= F by A13;

      

       A14: P c= ( union G9) by A10, SETFAM_1:def 11;

      ( dom f) = ( [#] T) by FUNCT_2:def 1;

      then ( union F9) = (f .: ( union G9)) by FUNCT_3: 14;

      then (f .: P) c= ( union F9) by A14, RELAT_1: 123;

      hence F9 is Cover of (f .: P) by SETFAM_1:def 11;

      thus thesis by A11;

    end;

    reserve SS for non empty TopSpace;

    reserve f for Function of TS, SS;

    theorem :: COMPTS_1:16

    

     Th16: TS is compact & SS is T_2 & ( rng f) = ( [#] SS) & f is continuous implies for PS st PS is closed holds (f .: PS) is closed

    proof

      assume that

       A1: TS is compact and

       A2: SS is T_2 and

       A3: ( rng f) = ( [#] SS) and

       A4: f is continuous;

      let PS;

      assume PS is closed;

      then PS is compact by A1, Th8;

      hence thesis by A2, A3, A4, Th7, Th15;

    end;

    theorem :: COMPTS_1:17

    TS is compact & SS is T_2 & ( rng f) = ( [#] SS) & f is one-to-one & f is continuous implies f is being_homeomorphism

    proof

      assume that

       A1: TS is compact and

       A2: SS is T_2 and

       A3: ( rng f) = ( [#] SS) and

       A4: f is one-to-one and

       A5: f is continuous;

      

       A6: ( dom f) = ( [#] TS) by FUNCT_2:def 1;

      for P be Subset of TS holds P is closed iff (f .: P) is closed

      proof

        let P be Subset of TS;

        

         A7: P c= (f " (f .: P)) by A6, FUNCT_1: 76;

        thus P is closed implies (f .: P) is closed by A1, A2, A3, A5, Th16;

        assume (f .: P) is closed;

        then

         A8: (f " (f .: P)) is closed by A5;

        (f " (f .: P)) c= P by A4, FUNCT_1: 82;

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

      end;

      hence thesis by A6, A3, A4, TOPS_2: 58;

    end;

    definition

      let D be set;

      :: COMPTS_1:def5

      func 1TopSp D -> TopStruct equals TopStruct (# D, ( [#] ( bool D)) #);

      coherence ;

    end

    registration

      let D be set;

      cluster ( 1TopSp D) -> strict TopSpace-like;

      coherence by ZFMISC_1:def 1;

    end

    registration

      let D be non empty set;

      cluster ( 1TopSp D) -> non empty;

      coherence ;

    end

    registration

      let x be set;

      cluster ( 1TopSp {x}) -> T_2;

      coherence

      proof

        let p,q be Point of ( 1TopSp {x});

        assume

         A1: p <> q;

        p = x by TARSKI:def 1;

        hence thesis by A1, TARSKI:def 1;

      end;

    end

    registration

      cluster T_2 non empty for TopSpace;

      existence

      proof

        take ( 1TopSp { {} });

        thus thesis;

      end;

    end

    registration

      let T be T_2 non empty TopSpace;

      cluster compact -> closed for Subset of T;

      coherence by Th7;

    end

    registration

      let A be finite set;

      cluster ( 1TopSp A) -> finite;

      coherence ;

    end

    registration

      cluster non empty finite strict for TopSpace;

      existence

      proof

        take ( 1TopSp { {} });

        thus thesis;

      end;

    end

    registration

      cluster finite -> compact for TopSpace;

      coherence ;

    end

    theorem :: COMPTS_1:18

    for T be TopSpace st the carrier of T is finite holds T is compact;

    registration

      let T be TopSpace;

      cluster finite -> compact for Subset of T;

      coherence

      proof

        let A be Subset of T;

        assume A is finite;

        then

        reconsider B = A as finite Subset of T;

        ( [#] (T | B)) = B by PRE_TOPC:def 5;

        then

         A1: (T | B) is compact;

        B = {} or B <> {} ;

        hence thesis by A1, Th3;

      end;

    end

    registration

      let T be non empty TopSpace;

      cluster non empty compact for Subset of T;

      existence

      proof

        set A = the finite non empty Subset of T;

        take A;

        thus thesis;

      end;

    end

    registration

      cluster empty -> T_2 for TopStruct;

      coherence by STRUCT_0:def 10;

    end

    registration

      let T be T_2 TopStruct;

      cluster -> T_2 for SubSpace of T;

      coherence

      proof

        let A be SubSpace of T;

        per cases ;

          suppose A is empty;

          hence thesis;

        end;

          suppose

           A1: A is non empty;

          let p,q be Point of A such that

           A2: not p = q;

          ( [#] A) c= ( [#] T) by PRE_TOPC:def 4;

          then T is non empty by A1;

          then

          reconsider p9 = p, q9 = q as Point of T by A1, PRE_TOPC: 25;

          consider W,V be Subset of T such that

           A3: W is open and

           A4: V is open and

           A5: p9 in W and

           A6: q9 in V and

           A7: W misses V by A2, PRE_TOPC:def 10;

          reconsider W9 = (W /\ ( [#] A)), V9 = (V /\ ( [#] A)) as Subset of A;

          V in the topology of T by A4;

          then

           A8: V9 in the topology of A by PRE_TOPC:def 4;

          take W9, V9;

          W in the topology of T by A3;

          then W9 in the topology of A by PRE_TOPC:def 4;

          hence W9 is open & V9 is open by A8;

          thus p in W9 & q in V9 by A1, A5, A6, XBOOLE_0:def 4;

          

           A9: (W /\ V) = {} by A7;

          (W9 /\ V9) = ((W /\ (V /\ ( [#] A))) /\ ( [#] A)) by XBOOLE_1: 16

          .= ( {} /\ ( [#] A)) by A9, XBOOLE_1: 16

          .= {} ;

          hence thesis;

        end;

      end;

    end

    theorem :: COMPTS_1:19

    

     Th19: for X be TopStruct holds for Y be SubSpace of X, A be Subset of X, B be Subset of Y st A = B holds A is compact iff B is compact

    proof

      let X be TopStruct;

      let Y be SubSpace of X, A be Subset of X, B be Subset of Y such that

       A1: A = B;

      

       A2: B c= ( [#] Y);

      hence A is compact implies B is compact by A1, Th2;

      assume B is compact;

      then for P be Subset of Y st P = A holds P is compact by A1;

      hence thesis by A1, A2, Th2;

    end;

    reserve T,S for non empty TopSpace,

p for Point of T;

    

     Lm1: for X be set holds for T1,T2 be SubSpace of T, f be Function of T1, S, g be Function of T2, S st (( [#] T1) \/ ( [#] T2)) = ( [#] T) & (( [#] T1) /\ ( [#] T2)) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & (f | X) tolerates (g | X) holds (f +* g) is continuous Function of T, S

    proof

      let X be set;

      let T1,T2 be SubSpace of T, f be Function of T1, S, g be Function of T2, S;

      assume that

       A1: (( [#] T1) \/ ( [#] T2)) = ( [#] T) and

       A2: (( [#] T1) /\ ( [#] T2)) = X and

       A3: T1 is compact and

       A4: T2 is compact and

       A5: T is T_2 and

       A6: f is continuous and

       A7: g is continuous and

       A8: (f | X) tolerates (g | X);

      set h = (f +* g);

      

       A9: ( dom g) = ( [#] T2) by FUNCT_2:def 1;

      ( rng h) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

      then

       A10: ( rng h) c= the carrier of S by XBOOLE_1: 1;

      

       A11: ( dom f) = ( [#] T1) by FUNCT_2:def 1;

      then ( dom h) = the carrier of T by A1, A9, FUNCT_4:def 1;

      then

      reconsider h as Function of T, S by A10, FUNCT_2:def 1, RELSET_1: 4;

      for P be Subset of S st P is closed holds (h " P) is closed

      proof

        let P be Subset of S;

        ( [#] T1) c= ( [#] T) by A1, XBOOLE_1: 7;

        then

        reconsider P1 = (f " P) as Subset of T by XBOOLE_1: 1;

        ( [#] T2) c= ( [#] T) by A1, XBOOLE_1: 7;

        then

        reconsider P2 = (g " P) as Subset of T by XBOOLE_1: 1;

        

         A12: ( dom h) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

         A13:

        now

          let x be object;

          thus x in ((h " P) /\ ( [#] T2)) implies x in (g " P)

          proof

            assume

             A14: x in ((h " P) /\ ( [#] T2));

            then x in (h " P) by XBOOLE_0:def 4;

            then

             A15: (h . x) in P by FUNCT_1:def 7;

            (g . x) = (h . x) by A9, A14, FUNCT_4: 13;

            hence thesis by A9, A14, A15, FUNCT_1:def 7;

          end;

          assume

           A16: x in (g " P);

          then

           A17: x in ( dom g) by FUNCT_1:def 7;

          (g . x) in P by A16, FUNCT_1:def 7;

          then

           A18: (h . x) in P by A17, FUNCT_4: 13;

          x in ( dom h) by A12, A17, XBOOLE_0:def 3;

          then x in (h " P) by A18, FUNCT_1:def 7;

          hence x in ((h " P) /\ ( [#] T2)) by A16, XBOOLE_0:def 4;

        end;

        

         A19: for x be set st x in ( [#] T1) holds (h . x) = (f . x)

        proof

          let x be set such that

           A20: x in ( [#] T1);

          

           A21: ( dom g) = the carrier of T2 by FUNCT_2:def 1;

          per cases ;

            suppose

             A22: x in ( [#] T2);

            then x in (( [#] T1) /\ ( [#] T2)) by A20, XBOOLE_0:def 4;

            then

             A23: x in X by A2;

            then

             A24: ((f | X) . x) = (f . x) & ((g | X) . x) = (g . x) by FUNCT_1: 49;

            x in ( dom (f | X)) & x in ( dom (g | X)) by A11, A20, A21, A22, A23, RELAT_1: 57;

            then x in (( dom (f | X)) /\ ( dom (g | X))) by XBOOLE_0:def 4;

            then ((f | X) . x) = ((g | X) . x) by A8, PARTFUN1:def 4;

            hence thesis by A9, A22, A24, FUNCT_4: 13;

          end;

            suppose not x in ( [#] T2);

            hence thesis by A9, FUNCT_4: 11;

          end;

        end;

        now

          let x be object;

          thus x in ((h " P) /\ ( [#] T1)) implies x in (f " P)

          proof

            assume

             A25: x in ((h " P) /\ ( [#] T1));

            then x in (h " P) by XBOOLE_0:def 4;

            then

             A26: (h . x) in P by FUNCT_1:def 7;

            (f . x) = (h . x) by A19, A25;

            hence thesis by A11, A25, A26, FUNCT_1:def 7;

          end;

          assume

           A27: x in (f " P);

          then x in ( dom f) by FUNCT_1:def 7;

          then

           A28: x in ( dom h) by A12, XBOOLE_0:def 3;

          (f . x) in P by A27, FUNCT_1:def 7;

          then (h . x) in P by A19, A27;

          then x in (h " P) by A28, FUNCT_1:def 7;

          hence x in ((h " P) /\ ( [#] T1)) by A27, XBOOLE_0:def 4;

        end;

        then

         A29: ((h " P) /\ ( [#] T1)) = (f " P) by TARSKI: 2;

        assume

         A30: P is closed;

        then (f " P) is closed by A6;

        then (f " P) is compact by A3, Th8;

        then

         A31: P1 is compact by Th19;

        (g " P) is closed by A7, A30;

        then (g " P) is compact by A4, Th8;

        then

         A32: P2 is compact by Th19;

        (h " P) = ((h " P) /\ (( [#] T1) \/ ( [#] T2))) by A11, A9, A12, RELAT_1: 132, XBOOLE_1: 28

        .= (((h " P) /\ ( [#] T1)) \/ ((h " P) /\ ( [#] T2))) by XBOOLE_1: 23;

        then (h " P) = ((f " P) \/ (g " P)) by A29, A13, TARSKI: 2;

        hence thesis by A5, A31, A32;

      end;

      hence thesis by PRE_TOPC:def 6;

    end;

    theorem :: COMPTS_1:20

    for T1,T2 be SubSpace of T, f be Function of T1, S, g be Function of T2, S st (( [#] T1) \/ ( [#] T2)) = ( [#] T) & (( [#] T1) /\ ( [#] T2)) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & (f . p) = (g . p) holds (f +* g) is continuous Function of T, S

    proof

      let T1,T2 be SubSpace of T, f be Function of T1, S, g be Function of T2, S;

      assume

       A1: (( [#] T1) \/ ( [#] T2)) = ( [#] T) & (( [#] T1) /\ ( [#] T2)) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous;

      assume (f . p) = (g . p);

      then (f | {p}) tolerates (g | {p}) by PARTFUN1: 81;

      hence thesis by A1, Lm1;

    end;

    theorem :: COMPTS_1:21

    for T be non empty TopSpace, T1,T2 be SubSpace of T, p1,p2 be Point of T holds for f be Function of T1, S, g be Function of T2, S st (( [#] T1) \/ ( [#] T2)) = ( [#] T) & (( [#] T1) /\ ( [#] T2)) = {p1, p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & (f . p1) = (g . p1) & (f . p2) = (g . p2) holds (f +* g) is continuous Function of T, S

    proof

      let T be non empty TopSpace, T1,T2 be SubSpace of T, p1,p2 be Point of T;

      let f be Function of T1, S, g be Function of T2, S;

      assume

       A1: (( [#] T1) \/ ( [#] T2)) = ( [#] T) & (( [#] T1) /\ ( [#] T2)) = {p1, p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous;

      assume (f . p1) = (g . p1) & (f . p2) = (g . p2);

      then (f | {p1, p2}) tolerates (g | {p1, p2}) by PARTFUN1: 82;

      hence thesis by A1, Lm1;

    end;

    begin

    registration

      let S be TopStruct;

      cluster the topology of S -> open;

      coherence

      proof

        let P be Subset of S;

        thus thesis;

      end;

    end

    registration

      let T be TopSpace;

      cluster open non empty for Subset-Family of T;

      existence

      proof

        take the topology of T;

        thus thesis;

      end;

    end

    theorem :: COMPTS_1:22

    

     Th22: for T be non empty TopSpace, F be set holds F is open Subset-Family of T iff F is open Subset-Family of the TopStruct of T

    proof

      let T be non empty TopSpace, F be set;

      thus F is open Subset-Family of T implies F is open Subset-Family of the TopStruct of T

      proof

        assume

         A1: F is open Subset-Family of T;

        then

        reconsider F as Subset-Family of the TopStruct of T;

        F is open by A1, TOPS_2:def 1, PRE_TOPC: 30;

        hence thesis;

      end;

      assume

       A2: F is open Subset-Family of the TopStruct of T;

      then

      reconsider F as Subset-Family of T;

      F is open by A2, TOPS_2:def 1, PRE_TOPC: 30;

      hence thesis;

    end;

    theorem :: COMPTS_1:23

    for T be non empty TopSpace, X be set holds X is compact Subset of T iff X is compact Subset of the TopStruct of T

    proof

      let T be non empty TopSpace, X be set;

      thus X is compact Subset of T implies X is compact Subset of the TopStruct of T

      proof

        assume

         A1: X is compact Subset of T;

        then

        reconsider Z = X as Subset of the TopStruct of T;

        Z is compact by Th22, A1, Def4;

        hence thesis;

      end;

      assume

       A2: X is compact Subset of the TopStruct of T;

      then

      reconsider Z = X as Subset of T;

      Z is compact by Th22, A2, Def4;

      hence thesis;

    end;

    theorem :: COMPTS_1:24

    for X be set holds for T1,T2 be SubSpace of T, f be Function of T1, S, g be Function of T2, S st (( [#] T1) \/ ( [#] T2)) = ( [#] T) & (( [#] T1) /\ ( [#] T2)) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & (f | X) tolerates (g | X) holds (f +* g) is continuous Function of T, S by Lm1;