tops_2.miz



    begin

    reserve x,y for set,

T for TopStruct,

GX for TopSpace,

P,Q,M,N for Subset of T,

F,G for Subset-Family of T,

W,Z for Subset-Family of GX,

A for SubSpace of T;

    theorem :: TOPS_2:1

    for T be 1-sorted, F be Subset-Family of T holds F c= ( bool ( [#] T));

    theorem :: TOPS_2:2

    

     Th2: for T be 1-sorted, F be Subset-Family of T, X be set st X c= F holds X is Subset-Family of T

    proof

      let T be 1-sorted, F be Subset-Family of T, X be set;

      assume

       A1: X c= F;

      X c= ( bool the carrier of T)

      proof

        let y be object;

        assume y in X;

        then y in F by A1;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TOPS_2:3

    for T be non empty 1-sorted, F be Subset-Family of T st F is Cover of T holds F <> {}

    proof

      let T be non empty 1-sorted, F be Subset-Family of T;

      set x = the Element of ( union F);

      assume F is Cover of T;

      then ( union F) = the carrier of T by SETFAM_1: 45;

      then ex A be set st x in A & A in F by TARSKI:def 4;

      hence thesis;

    end;

    theorem :: TOPS_2:4

    for T be 1-sorted, F,G be Subset-Family of T holds (( union F) \ ( union G)) c= ( union (F \ G))

    proof

      let T be 1-sorted, F,G be Subset-Family of T;

      let x be object;

      assume

       A1: x in (( union F) \ ( union G));

      then x in ( union F) by XBOOLE_0:def 5;

      then

      consider A be set such that

       A2: x in A and

       A3: A in F by TARSKI:def 4;

       not x in ( union G) by A1, XBOOLE_0:def 5;

      then not A in G by A2, TARSKI:def 4;

      then A in (F \ G) by A3, XBOOLE_0:def 5;

      hence thesis by A2, TARSKI:def 4;

    end;

    theorem :: TOPS_2:5

    for T be set, F be Subset-Family of T holds F <> {} iff ( COMPLEMENT F) <> {}

    proof

      let T be set, F be Subset-Family of T;

      thus F <> {} implies ( COMPLEMENT F) <> {} by SETFAM_1: 32;

      assume ( COMPLEMENT F) <> {} ;

      then ( COMPLEMENT ( COMPLEMENT F)) <> {} by SETFAM_1: 32;

      hence thesis;

    end;

    theorem :: TOPS_2:6

    

     Th6: for T be set, F be Subset-Family of T holds F <> {} implies ( meet ( COMPLEMENT F)) = (( union F) ` )

    proof

      let T be set, F be Subset-Family of T;

      assume F <> {} ;

      then ( meet ( COMPLEMENT F)) = (( [#] T) \ ( union F)) by SETFAM_1: 33;

      hence thesis;

    end;

    theorem :: TOPS_2:7

    

     Th7: for T be set, F be Subset-Family of T holds F <> {} implies ( union ( COMPLEMENT F)) = (( meet F) ` )

    proof

      let T be set, F be Subset-Family of T;

      assume F <> {} ;

      

      then ( union ( COMPLEMENT F)) = (( [#] T) \ ( meet F)) by SETFAM_1: 34

      .= (T \ ( meet F));

      hence thesis;

    end;

    

     Lm1: for T be 1-sorted, F be Subset-Family of T st ( COMPLEMENT F) is finite holds F is finite

    proof

      let T be 1-sorted, F be Subset-Family of T;

      defpred X[ object, object] means for X be Subset of T st X = $1 holds $2 = (X ` );

      

       A1: for x be object st x in ( COMPLEMENT F) holds ex y be object st X[x, y]

      proof

        let x be object;

        assume x in ( COMPLEMENT F);

        then

        reconsider X = x as Subset of T;

        reconsider y = (X ` ) as object;

        take y;

        thus thesis;

      end;

      consider f be Function such that

       A2: ( dom f) = ( COMPLEMENT F) and

       A3: for x be object st x in ( COMPLEMENT F) holds X[x, (f . x)] from CLASSES1:sch 1( A1);

      for x be object holds x in ( rng f) iff x in F

      proof

        let x be object;

        hereby

          assume x in ( rng f);

          then

          consider y be object such that

           A4: y in ( dom f) and

           A5: x = (f . y) by FUNCT_1:def 3;

          reconsider Y = y as Subset of T by A2, A4;

          (Y ` ) in F by A2, A4, SETFAM_1:def 7;

          hence x in F by A2, A3, A4, A5;

        end;

        assume

         A6: x in F;

        then

        reconsider X = x as Subset of T;

        

         A7: ((X ` ) ` ) = X;

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

        then

         A8: (f . (X ` )) = ((X ` ) ` ) by A3;

        (X ` ) in ( dom f) by A2, A6, A7, SETFAM_1:def 7;

        hence thesis by A8, FUNCT_1:def 3;

      end;

      then ( rng f) = F by TARSKI: 2;

      then

       A9: (f .: ( COMPLEMENT F)) = F by A2, RELAT_1: 113;

      assume ( COMPLEMENT F) is finite;

      hence thesis by A9, FINSET_1: 5;

    end;

    theorem :: TOPS_2:8

    

     Th8: for T be 1-sorted, F be Subset-Family of T holds ( COMPLEMENT F) is finite iff F is finite

    proof

      let T be 1-sorted, F be Subset-Family of T;

      thus ( COMPLEMENT F) is finite implies F is finite by Lm1;

      assume F is finite;

      then ( COMPLEMENT ( COMPLEMENT F)) is finite;

      hence thesis by Lm1;

    end;

    definition

      let T be TopStruct, F be Subset-Family of T;

      :: TOPS_2:def1

      attr F is open means for P be Subset of T holds P in F implies P is open;

      :: TOPS_2:def2

      attr F is closed means for P be Subset of T holds P in F implies P is closed;

    end

    theorem :: TOPS_2:9

    

     Th9: F is closed iff ( COMPLEMENT F) is open

    proof

      thus F is closed implies ( COMPLEMENT F) is open

      proof

        assume

         A1: F is closed;

        let P;

        assume P in ( COMPLEMENT F);

        then (P ` ) in F by SETFAM_1:def 7;

        then (P ` ) is closed by A1;

        hence thesis by TOPS_1: 4;

      end;

      assume

       A2: ( COMPLEMENT F) is open;

      let P such that

       A3: P in F;

      ((P ` ) ` ) = P;

      then (P ` ) in ( COMPLEMENT F) by A3, SETFAM_1:def 7;

      then (P ` ) is open by A2;

      hence thesis;

    end;

    theorem :: TOPS_2:10

    F is open iff ( COMPLEMENT F) is closed

    proof

      F = ( COMPLEMENT ( COMPLEMENT F));

      hence thesis by Th9;

    end;

    theorem :: TOPS_2:11

    F c= G & G is open implies F is open;

    theorem :: TOPS_2:12

    F c= G & G is closed implies F is closed;

    theorem :: TOPS_2:13

    F is open & G is open implies (F \/ G) is open

    proof

      assume

       A1: F is open & G is open;

      let P;

      assume P in (F \/ G);

      then P in F or P in G by XBOOLE_0:def 3;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:14

    F is open implies (F /\ G) is open

    proof

      assume

       A1: F is open;

      let P;

      assume P in (F /\ G);

      then P in F by XBOOLE_0:def 4;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:15

    F is open implies (F \ G) is open

    proof

      assume

       A1: F is open;

      let P;

      assume P in (F \ G);

      then P in F by XBOOLE_0:def 5;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:16

    F is closed & G is closed implies (F \/ G) is closed

    proof

      assume

       A1: F is closed & G is closed;

      let P;

      assume P in (F \/ G);

      then P in F or P in G by XBOOLE_0:def 3;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:17

    F is closed implies (F /\ G) is closed

    proof

      assume

       A1: F is closed;

      let P;

      assume P in (F /\ G);

      then P in F by XBOOLE_0:def 4;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:18

    F is closed implies (F \ G) is closed

    proof

      assume

       A1: F is closed;

      let P;

      assume P in (F \ G);

      then P in F by XBOOLE_0:def 5;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:19

    

     Th19: W is open implies ( union W) is open

    proof

      assume

       A1: W is open;

      W c= the topology of GX

      proof

        let x be object;

        assume

         A2: x in W;

        then

        reconsider X = x as Subset of GX;

        X is open by A1, A2;

        hence thesis;

      end;

      then ( union W) in the topology of GX by PRE_TOPC:def 1;

      hence thesis;

    end;

    theorem :: TOPS_2:20

    

     Th20: W is open & W is finite implies ( meet W) is open

    proof

      assume that

       A1: W is open and

       A2: W is finite;

      consider p be FinSequence such that

       A3: ( rng p) = W by A2, FINSEQ_1: 52;

      consider n be Nat such that

       A4: ( dom p) = ( Seg n) by FINSEQ_1:def 2;

      defpred X[ Nat] means for Z st Z = (p .: ( Seg $1)) & $1 <= n & 1 <= n holds ( meet Z) is open;

      

       A5: for k be Nat holds X[k] implies X[(k + 1)]

      proof

        let k be Nat;

        assume

         A6: for Z st Z = (p .: ( Seg k)) & k <= n & 1 <= n holds ( meet Z) is open;

        let Z such that

         A7: Z = (p .: ( Seg (k + 1)));

        assume that

         A8: (k + 1) <= n and

         A9: 1 <= n;

         A10:

        now

          reconsider G2 = ( Im (p,(k + 1))) as Subset-Family of GX by A3, Th2, RELAT_1: 111;

          reconsider G1 = (p .: ( Seg k)) as Subset-Family of GX by A3, Th2, RELAT_1: 111;

          assume

           A11: 0 < k;

          (k + 1) <= (n + 1) by A8, NAT_1: 12;

          then k <= n by XREAL_1: 6;

          then ( Seg k) c= ( dom p) by A4, FINSEQ_1: 5;

          then

           A12: G1 <> {} by A11, RELAT_1: 119;

          (k + 1) <= (n + 1) by A8, NAT_1: 12;

          then k <= n by XREAL_1: 6;

          then

           A13: ( meet G1) is open by A6, A9;

           0 <= k & ( 0 + 1) = 1 by NAT_1: 2;

          then 1 <= (k + 1) by XREAL_1: 7;

          then

           A14: (k + 1) in ( dom p) by A4, A8, FINSEQ_1: 1;

          then G2 = {(p . (k + 1))} by FUNCT_1: 59;

          then

           A15: ( meet G2) = (p . (k + 1)) by SETFAM_1: 10;

           {(k + 1)} c= ( dom p) by A14, ZFMISC_1: 31;

          then

           A16: G2 <> {} by RELAT_1: 119;

          (p . (k + 1)) in W by A3, A14, FUNCT_1:def 3;

          then

           A17: ( meet G2) is open by A1, A15;

          (p .: ( Seg (k + 1))) = (p .: (( Seg k) \/ {(k + 1)})) by FINSEQ_1: 9

          .= ((p .: ( Seg k)) \/ (p .: {(k + 1)})) by RELAT_1: 120;

          then ( meet Z) = (( meet G1) /\ ( meet G2)) by A7, A12, A16, SETFAM_1: 9;

          hence thesis by A13, A17, TOPS_1: 11;

        end;

        now

          assume

           A18: k = 0 ;

          then

           A19: 1 in ( dom p) by A4, A8, FINSEQ_1: 1;

          then ( Im (p,1)) = {(p . 1)} by FUNCT_1: 59;

          then ( meet Z) = (p . 1) by A7, A18, FINSEQ_1: 2, SETFAM_1: 10;

          then ( meet Z) in W by A3, A19, FUNCT_1:def 3;

          hence thesis by A1;

        end;

        hence thesis by A10, NAT_1: 3;

      end;

      

       A20: X[ 0 ]

      proof

        let Z;

        assume that

         A21: Z = (p .: ( Seg 0 )) and 0 <= n;

        

         A22: {} in the topology of GX by PRE_TOPC: 1;

        ( meet Z) = {} by A21, SETFAM_1: 1;

        hence thesis by A22;

      end;

      

       A23: for k be Nat holds X[k] from NAT_1:sch 2( A20, A5);

       A24:

      now

        assume

         A25: 1 <= n;

        W = (p .: ( Seg n)) by A3, A4, RELAT_1: 113;

        hence thesis by A23, A25;

      end;

       A26:

      now

        assume n = 0 ;

        then ( Seg n) = {} ;

        then W = (p .: {} ) by A3, A4, RELAT_1: 113;

        then

         A27: ( meet W) = {} by SETFAM_1: 1;

         {} in the topology of GX by PRE_TOPC: 1;

        hence thesis by A27;

      end;

      now

        assume n <> 0 ;

        then

         A28: 0 < n by NAT_1: 3;

        1 = ( 0 + 1);

        hence 1 <= n by A28, NAT_1: 13;

      end;

      hence thesis by A24, A26;

    end;

    theorem :: TOPS_2:21

    W is closed & W is finite implies ( union W) is closed

    proof

      reconsider C = ( COMPLEMENT W) as Subset-Family of GX;

      assume W is closed & W is finite;

      then ( COMPLEMENT W) is open & ( COMPLEMENT W) is finite by Th8, Th9;

      then

       A1: ( meet C) is open by Th20;

      now

        assume W <> {} ;

        then ( meet ( COMPLEMENT W)) = (( union W) ` ) by Th6;

        hence thesis by A1;

      end;

      hence thesis by ZFMISC_1: 2;

    end;

    theorem :: TOPS_2:22

    W is closed implies ( meet W) is closed

    proof

      reconsider C = ( COMPLEMENT W) as Subset-Family of GX;

      assume W is closed;

      then ( COMPLEMENT W) is open by Th9;

      then

       A1: ( union C) is open by Th19;

       A2:

      now

        assume W <> {} ;

        then ( union ( COMPLEMENT W)) = (( meet W) ` ) by Th7;

        hence thesis by A1;

      end;

      now

        assume W = {} ;

        then ( meet W) = ( {} GX) by SETFAM_1:def 1;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: TOPS_2:23

    for F be Subset-Family of A holds F is Subset-Family of T

    proof

      let F be Subset-Family of A;

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

      then ( bool the carrier of A) c= ( bool the carrier of T) by ZFMISC_1: 67;

      hence thesis by XBOOLE_1: 1;

    end;

    theorem :: TOPS_2:24

    

     Th24: for B be Subset of A holds B is open iff ex C be Subset of T st C is open & (C /\ ( [#] A)) = B

    proof

      let B be Subset of A;

      hereby

        assume B is open;

        then B in the topology of A;

        then

        consider C be Subset of T such that

         A1: C in the topology of T & (C /\ ( [#] A)) = B by PRE_TOPC:def 4;

        reconsider C as Subset of T;

        take C;

        thus C is open & (C /\ ( [#] A)) = B by A1;

      end;

      given C be Subset of T such that

       A2: C is open and

       A3: (C /\ ( [#] A)) = B;

      C in the topology of T by A2;

      then B in the topology of A by A3, PRE_TOPC:def 4;

      hence thesis;

    end;

    theorem :: TOPS_2:25

    

     Th25: Q is open implies for P be Subset of A st P = Q holds P is open

    proof

      assume

       A1: Q is open;

      let P be Subset of A;

      assume P = Q;

      then (Q /\ ( [#] A)) = P by XBOOLE_1: 28;

      hence thesis by A1, Th24;

    end;

    theorem :: TOPS_2:26

    

     Th26: Q is closed implies for P be Subset of A st P = Q holds P is closed

    proof

      assume

       A1: Q is closed;

      let P be Subset of A;

      assume P = Q;

      then (Q /\ ( [#] A)) = P by XBOOLE_1: 28;

      hence thesis by A1, PRE_TOPC: 13;

    end;

    theorem :: TOPS_2:27

    F is open implies for G be Subset-Family of A st G = F holds G is open by Th25;

    theorem :: TOPS_2:28

    F is closed implies for G be Subset-Family of A st G = F holds G is closed by Th26;

    theorem :: TOPS_2:29

    

     Th29: (M /\ N) is Subset of (T | N)

    proof

      (M /\ N) c= N by XBOOLE_1: 17;

      then (M /\ N) c= ( [#] (T | N)) by PRE_TOPC:def 5;

      hence thesis;

    end;

    definition

      let T be TopStruct, P be Subset of T, F be Subset-Family of T;

      :: TOPS_2:def3

      func F | P -> Subset-Family of (T | P) means

      : Def3: for Q be Subset of (T | P) holds Q in it iff ex R be Subset of T st R in F & (R /\ P) = Q;

      existence

      proof

        thus ex G be Subset-Family of (T | P) st for Q be Subset of (T | P) holds Q in G iff ex R be Subset of T st R in F & (R /\ P) = Q

        proof

          defpred X[ Subset of (T | P)] means ex R be Subset of T st R in F & (R /\ P) = $1;

          ex G be Subset-Family of (T | P) st for Q be Subset of (T | P) holds Q in G iff X[Q] from SUBSET_1:sch 3;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        thus for G,H be Subset-Family of (T | P) st (for Q be Subset of (T | P) holds Q in G iff ex R be Subset of T st R in F & (R /\ P) = Q) & (for Q be Subset of (T | P) holds Q in H iff ex R be Subset of T st R in F & (R /\ P) = Q) holds G = H

        proof

          let G,H be Subset-Family of (T | P) such that

           A1: for Q be Subset of (T | P) holds Q in G iff ex R be Subset of T st R in F & (R /\ P) = Q and

           A2: for Q be Subset of (T | P) holds Q in H iff ex R be Subset of T st R in F & (R /\ P) = Q;

          for x be object holds x in G iff x in H

          proof

            let x be object;

            hereby

              assume

               A3: x in G;

              then

              reconsider X = x as Subset of (T | P);

              ex R be Subset of T st R in F & (R /\ P) = X by A1, A3;

              hence x in H by A2;

            end;

            assume

             A4: x in H;

            then

            reconsider X = x as Subset of (T | P);

            ex R be Subset of T st R in F & (R /\ P) = X by A2, A4;

            hence thesis by A1;

          end;

          hence thesis by TARSKI: 2;

        end;

      end;

    end

    theorem :: TOPS_2:30

    F c= G implies (F | M) c= (G | M)

    proof

      assume

       A1: F c= G;

      let x be object;

      assume

       A2: x in (F | M);

      then

      reconsider X = x as Subset of (T | M);

      ex R be Subset of T st R in F & (R /\ M) = X by A2, Def3;

      hence thesis by A1, Def3;

    end;

    theorem :: TOPS_2:31

    

     Th31: Q in F implies (Q /\ M) in (F | M)

    proof

      reconsider QQ = (Q /\ M) as Subset of (T | M) by Th29;

      

       A1: (Q /\ M) = QQ;

      assume Q in F;

      hence thesis by A1, Def3;

    end;

    theorem :: TOPS_2:32

    Q c= ( union F) implies (Q /\ M) c= ( union (F | M))

    proof

      assume

       A1: Q c= ( union F);

      now

        assume M <> {} ;

        thus (Q /\ M) c= ( union (F | M))

        proof

          let x be object;

          assume

           A2: x in (Q /\ M);

          then x in Q by XBOOLE_0:def 4;

          then

          consider Z be set such that

           A3: x in Z and

           A4: Z in F by A1, TARSKI:def 4;

          reconsider ZZ = Z as Subset of T by A4;

          (ZZ /\ M) in (F | M) by A4, Th31;

          then

          reconsider ZP = (ZZ /\ M) as Subset of (T | M);

          

           A5: ZP in (F | M) by A4, Th31;

          x in M by A2, XBOOLE_0:def 4;

          then x in ZP by A3, XBOOLE_0:def 4;

          hence thesis by A5, TARSKI:def 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPS_2:33

    M c= ( union F) implies M = ( union (F | M))

    proof

      assume

       A1: M c= ( union F);

      for x be object holds x in M iff x in ( union (F | M))

      proof

        let x be object;

        hereby

          assume

           A2: x in M;

          then

          consider A be set such that

           A3: x in A and

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

          reconsider A9 = A as Subset of T by A4;

          (A /\ M) c= M by XBOOLE_1: 17;

          then (A /\ M) c= ( [#] (T | M)) by PRE_TOPC:def 5;

          then

          reconsider B = (A9 /\ M) as Subset of (T | M);

          

           A5: B in (F | M) by A4, Def3;

          x in (A /\ M) by A2, A3, XBOOLE_0:def 4;

          hence x in ( union (F | M)) by A5, TARSKI:def 4;

        end;

        assume x in ( union (F | M));

        then

        consider A be set such that

         A6: x in A and

         A7: A in (F | M) by TARSKI:def 4;

        reconsider B = A as Subset of (T | M) by A7;

        ex R be Subset of T st R in F & (R /\ M) = B by A7, Def3;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPS_2:34

    

     Th34: ( union (F | M)) c= ( union F)

    proof

      let x be object;

      assume x in ( union (F | M));

      then

      consider A be set such that

       A1: x in A and

       A2: A in (F | M) by TARSKI:def 4;

      reconsider Q = A as Subset of (T | M) by A2;

      consider R be Subset of T such that

       A3: R in F and

       A4: (R /\ M) = Q by A2, Def3;

      x in R by A1, A4, XBOOLE_0:def 4;

      hence thesis by A3, TARSKI:def 4;

    end;

    theorem :: TOPS_2:35

    M c= ( union (F | M)) implies M c= ( union F)

    proof

      assume

       A1: M c= ( union (F | M));

      ( union (F | M)) c= ( union F) by Th34;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:36

    F is finite implies (F | M) is finite

    proof

      defpred X[ object, object] means for X be Subset of T st X = $1 holds $2 = (X /\ M);

      

       A1: for x be object st x in F holds ex y be object st X[x, y]

      proof

        let x be object;

        assume x in F;

        then

        reconsider X = x as Subset of T;

        reconsider y = (X /\ M) as set;

        take y;

        thus thesis;

      end;

      consider f be Function such that

       A2: ( dom f) = F and

       A3: for x be object st x in F holds X[x, (f . x)] from CLASSES1:sch 1( A1);

      for x be object holds x in ( rng f) iff x in (F | M)

      proof

        let x be object;

        hereby

          assume x in ( rng f);

          then

          consider y be object such that

           A4: y in ( dom f) and

           A5: x = (f . y) by FUNCT_1:def 3;

          reconsider Y = y as Subset of T by A2, A4;

          (Y /\ M) c= M by XBOOLE_1: 17;

          then (Y /\ M) c= ( [#] (T | M)) by PRE_TOPC:def 5;

          then

          reconsider X = (f . y) as Subset of (T | M) by A2, A3, A4;

          (f . y) = (Y /\ M) by A2, A3, A4;

          then X in (F | M) by A2, A4, Def3;

          hence x in (F | M) by A5;

        end;

        assume

         A6: x in (F | M);

        then

        reconsider X = x as Subset of (T | M);

        consider R be Subset of T such that

         A7: R in F and

         A8: (R /\ M) = X by A6, Def3;

        (f . R) = (R /\ M) by A3, A7;

        hence thesis by A2, A7, A8, FUNCT_1:def 3;

      end;

      then ( rng f) = (F | M) by TARSKI: 2;

      then

       A9: (f .: F) = (F | M) by A2, RELAT_1: 113;

      assume F is finite;

      hence thesis by A9, FINSET_1: 5;

    end;

    theorem :: TOPS_2:37

    F is open implies (F | M) is open

    proof

      assume

       A1: F is open;

      let Q be Subset of (T | M);

      assume Q in (F | M);

      then

      consider R be Subset of T such that

       A2: R in F and

       A3: (R /\ M) = Q by Def3;

      reconsider R as Subset of T;

      

       A4: Q = (R /\ ( [#] (T | M))) by A3, PRE_TOPC:def 5;

      R is open by A1, A2;

      hence thesis by A4, Th24;

    end;

    theorem :: TOPS_2:38

    F is closed implies (F | M) is closed

    proof

      assume

       A1: F is closed;

      let Q be Subset of (T | M);

      assume Q in (F | M);

      then

      consider R be Subset of T such that

       A2: R in F and

       A3: (R /\ M) = Q by Def3;

      reconsider R as Subset of T;

      

       A4: Q = (R /\ ( [#] (T | M))) by A3, PRE_TOPC:def 5;

      R is closed by A1, A2;

      hence thesis by A4, PRE_TOPC: 13;

    end;

    theorem :: TOPS_2:39

    for F be Subset-Family of A st F is open holds ex G be Subset-Family of T st G is open & for AA be Subset of T st AA = ( [#] A) holds F = (G | AA)

    proof

      let F be Subset-Family of A;

      assume

       A1: F is open;

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

      then

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

      defpred X[ Subset of T] means ex X1 be Subset of T st X1 = $1 & X1 is open & ($1 /\ At) in F;

      consider G be Subset-Family of T such that

       A2: for X be Subset of T holds X in G iff X[X] from SUBSET_1:sch 3;

      take G;

      thus G is open

      proof

        let H be Subset of T;

        assume H in G;

        then ex X1 be Subset of T st X1 = H & X1 is open & (H /\ At) in F by A2;

        hence thesis;

      end;

      let AA be Subset of T;

      assume

       A3: AA = ( [#] A);

      then F c= ( bool AA);

      then F c= ( bool ( [#] (T | AA))) by PRE_TOPC:def 5;

      then

      reconsider FF = F as Subset-Family of (T | AA);

      for X be Subset of (T | AA) holds X in FF iff ex X9 be Subset of T st X9 in G & (X9 /\ AA) = X

      proof

        let X be Subset of (T | AA);

        thus X in FF implies ex X9 be Subset of T st X9 in G & (X9 /\ AA) = X

        proof

          assume

           A4: X in FF;

          then

          reconsider XX = X as Subset of A;

          XX is open by A1, A4;

          then

          consider Y be Subset of T such that

           A5: Y is open & (Y /\ ( [#] A)) = XX by Th24;

          take Y;

          thus thesis by A2, A3, A4, A5;

        end;

        given X9 be Subset of T such that

         A6: X9 in G and

         A7: (X9 /\ AA) = X;

        ex X1 be Subset of T st X1 = X9 & X1 is open & (X9 /\ At) in F by A2, A6;

        hence thesis by A3, A7;

      end;

      hence thesis by Def3;

    end;

    theorem :: TOPS_2:40

    ex f be Function st ( dom f) = F & ( rng f) = (F | P) & for x st x in F holds for Q st Q = x holds (f . x) = (Q /\ P)

    proof

      defpred X[ object, object] means for Q st Q = $1 holds $2 = (Q /\ P);

      

       A1: for x be object st x in F holds ex y be object st X[x, y]

      proof

        let x be object;

        assume x in F;

        then

        reconsider Q = x as Subset of T;

        reconsider y = (Q /\ P) as set;

        take y;

        thus thesis;

      end;

      consider f be Function such that

       A2: ( dom f) = F and

       A3: for x be object st x in F holds X[x, (f . x)] from CLASSES1:sch 1( A1);

      take f;

      thus ( dom f) = F by A2;

      for x be object holds x in ( rng f) iff x in (F | P)

      proof

        let x be object;

        hereby

          assume x in ( rng f);

          then

          consider y be object such that

           A4: y in ( dom f) and

           A5: (f . y) = x by FUNCT_1:def 3;

          reconsider Y = y as Subset of T by A2, A4;

          (Y /\ P) c= P by XBOOLE_1: 17;

          then (Y /\ P) c= ( [#] (T | P)) by PRE_TOPC:def 5;

          then

          reconsider X = x as Subset of (T | P) by A2, A3, A4, A5;

          X = (Y /\ P) by A2, A3, A4, A5;

          hence x in (F | P) by A2, A4, Def3;

        end;

        assume

         A6: x in (F | P);

        then

        reconsider X = x as Subset of (T | P);

        consider Q be Subset of T such that

         A7: Q in F and

         A8: (Q /\ P) = X by A6, Def3;

        reconsider p = Q as set;

        (f . p) = x by A3, A7, A8;

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

      end;

      hence ( rng f) = (F | P) by TARSKI: 2;

      thus thesis by A3;

    end;

    theorem :: TOPS_2:41

    

     Th41: for X,Y be 1-sorted, f be Function of X, Y st ( [#] Y) = {} implies ( [#] X) = {} holds (f " ( [#] Y)) = ( [#] X)

    proof

      let X,Y be 1-sorted, f be Function of X, Y such that

       A1: ( [#] Y) = {} implies ( [#] X) = {} ;

      (f " ( rng f)) = ( dom f) by RELAT_1: 134

      .= ( [#] X) by A1, FUNCT_2:def 1;

      then ( [#] X) c= (f " ( [#] Y)) by RELAT_1: 143;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: TOPS_2:42

    for T be 1-sorted, S be non empty 1-sorted, f be Function of T, S, H be Subset-Family of S holds (( " f) .: H) is Subset-Family of T

    proof

      let T be 1-sorted, S be non empty 1-sorted, f be Function of T, S, H be Subset-Family of S;

      (( " f) .: H) c= ( rng ( " f)) & ( rng ( " f)) c= ( bool ( dom f)) by FUNCT_3: 22, RELAT_1: 111;

      then (( " f) .: H) c= ( bool ( dom f));

      hence thesis by FUNCT_2:def 1;

    end;

    reserve S for non empty TopStruct,

f for Function of T, S,

H for Subset-Family of S;

    theorem :: TOPS_2:43

    

     Th43: for X,Y be TopStruct, f be Function of X, Y st ( [#] Y) = {} implies ( [#] X) = {} holds f is continuous iff for P be Subset of Y st P is open holds (f " P) is open

    proof

      let X,Y be TopStruct, f be Function of X, Y;

      assume

       A1: ( [#] Y) = {} implies ( [#] X) = {} ;

      hereby

        assume

         A2: f is continuous;

        let P1 be Subset of Y;

        assume P1 is open;

        then (P1 ` ) is closed by TOPS_1: 4;

        then

         A3: (f " (P1 ` )) is closed by A2;

        (f " (P1 ` )) = ((f " ( [#] Y)) \ (f " P1)) by FUNCT_1: 69

        .= (( [#] X) \ (f " P1)) by A1, Th41

        .= ((f " P1) ` );

        hence (f " P1) is open by A3, TOPS_1: 4;

      end;

      assume

       A4: for P1 be Subset of Y st P1 is open holds (f " P1) is open;

      let P1 be Subset of Y;

      assume P1 is closed;

      then (P1 ` ) is open;

      then

       A5: (f " (P1 ` )) is open by A4;

      (f " (P1 ` )) = ((f " ( [#] Y)) \ (f " P1)) by FUNCT_1: 69

      .= (( [#] X) \ (f " P1)) by A1, Th41

      .= ((f " P1) ` );

      hence thesis by A5;

    end;

    theorem :: TOPS_2:44

    

     Th44: for T be TopSpace, S be TopSpace, f be Function of T, S holds f is continuous iff for P1 be Subset of S holds ( Cl (f " P1)) c= (f " ( Cl P1))

    proof

      let T be TopSpace, S be TopSpace, f be Function of T, S;

      hereby

        assume

         A1: f is continuous;

        let P1 be Subset of S;

        ( Cl ( Cl P1)) = ( Cl P1);

        then ( Cl P1) is closed by PRE_TOPC: 22;

        then

         A2: (f " ( Cl P1)) is closed by A1;

        (f " P1) c= (f " ( Cl P1)) by PRE_TOPC: 18, RELAT_1: 143;

        then ( Cl (f " P1)) c= ( Cl (f " ( Cl P1))) by PRE_TOPC: 19;

        hence ( Cl (f " P1)) c= (f " ( Cl P1)) by A2, PRE_TOPC: 22;

      end;

      assume

       A3: for P1 be Subset of S holds ( Cl (f " P1)) c= (f " ( Cl P1));

      let P1 be Subset of S;

      assume P1 is closed;

      then ( Cl P1) = P1 by PRE_TOPC: 22;

      then (f " P1) c= ( Cl (f " P1)) & ( Cl (f " P1)) c= (f " P1) by A3, PRE_TOPC: 18;

      then (f " P1) = ( Cl (f " P1)) by XBOOLE_0:def 10;

      hence thesis by PRE_TOPC: 22;

    end;

    theorem :: TOPS_2:45

    

     Th45: for T be TopSpace, S be non empty TopSpace, f be Function of T, S holds f is continuous iff for P be Subset of T holds (f .: ( Cl P)) c= ( Cl (f .: P))

    proof

      let T be TopSpace, S be non empty TopSpace, f be Function of T, S;

      hereby

        assume

         A1: f is continuous;

        let P be Subset of T;

        P c= ( [#] T);

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

        then

         A2: ( Cl P) c= ( Cl (f " (f .: P))) by FUNCT_1: 76, PRE_TOPC: 19;

        ( Cl (f " (f .: P))) c= (f " ( Cl (f .: P))) by A1, Th44;

        then ( Cl P) c= (f " ( Cl (f .: P))) by A2;

        then

         A3: (f .: ( Cl P)) c= (f .: (f " ( Cl (f .: P)))) by RELAT_1: 123;

        (f .: (f " ( Cl (f .: P)))) c= ( Cl (f .: P)) by FUNCT_1: 75;

        hence (f .: ( Cl P)) c= ( Cl (f .: P)) by A3;

      end;

      assume

       A4: for P be Subset of T holds (f .: ( Cl P)) c= ( Cl (f .: P));

      now

        let P1 be Subset of S;

        ( Cl (f " P1)) c= ( [#] T);

        then ( Cl (f " P1)) c= ( dom f) by FUNCT_2:def 1;

        then

         A5: ( Cl (f " P1)) c= (f " (f .: ( Cl (f " P1)))) by FUNCT_1: 76;

        (f .: ( Cl (f " P1))) c= ( Cl (f .: (f " P1))) & ( Cl (f .: (f " P1))) c= ( Cl P1) by A4, FUNCT_1: 75, PRE_TOPC: 19;

        then (f .: ( Cl (f " P1))) c= ( Cl P1);

        then (f " (f .: ( Cl (f " P1)))) c= (f " ( Cl P1)) by RELAT_1: 143;

        hence ( Cl (f " P1)) c= (f " ( Cl P1)) by A5;

      end;

      hence thesis by Th44;

    end;

    theorem :: TOPS_2:46

    

     Th46: for T,V be TopStruct, S be non empty TopStruct, f be Function of T, S, g be Function of S, V holds f is continuous & g is continuous implies (g * f) is continuous

    proof

      let T,V be TopStruct, S be non empty TopStruct;

      let f be Function of T, S, g be Function of S, V;

      assume that

       A1: f is continuous and

       A2: g is continuous;

      let P be Subset of V;

      assume P is closed;

      then ((g * f) " P) = (f " (g " P)) & (g " P) is closed by A2, RELAT_1: 146;

      hence thesis by A1;

    end;

    theorem :: TOPS_2:47

    f is continuous & H is open implies for F st F = (( " f) .: H) holds F is open

    proof

      assume that

       A1: f is continuous and

       A2: H is open;

      let F such that

       A3: F = (( " f) .: H);

      let X be Subset of T;

      assume X in F;

      then

      consider y be object such that

       A4: y in ( dom ( " f)) and

       A5: y in H and

       A6: X = (( " f) . y) by A3, FUNCT_1:def 6;

      reconsider Y = y as Subset of S by A5;

      

       A7: X = (f " Y) by A4, A6, FUNCT_3: 21;

      

       A8: ( [#] S) = {} implies ( [#] T) = {} ;

      Y is open by A2, A5;

      hence thesis by A1, A8, A7, Th43;

    end;

    theorem :: TOPS_2:48

    for T,S be TopStruct, f be Function of T, S, H be Subset-Family of S st f is continuous & H is closed holds for F be Subset-Family of T st F = (( " f) .: H) holds F is closed

    proof

      let T,S be TopStruct, f be Function of T, S, H be Subset-Family of S;

      assume that

       A1: f is continuous and

       A2: H is closed;

      let F be Subset-Family of T such that

       A3: F = (( " f) .: H);

      let X be Subset of T;

      assume X in F;

      then

      consider y be object such that

       A4: y in ( dom ( " f)) and

       A5: y in H and

       A6: X = (( " f) . y) by A3, FUNCT_1:def 6;

      reconsider Y = y as Subset of S by A5;

      

       A7: X = (f " Y) by A4, A6, FUNCT_3: 21;

      Y is closed by A2, A5;

      hence thesis by A1, A7;

    end;

    definition

      let S,T be set, f be Function of S, T;

      assume

       A1: f is bijective;

      :: TOPS_2:def4

      func f /" -> Function of T, S equals

      : Def4: (f " );

      coherence

      proof

        ( rng f) = ( [#] T) by A1, FUNCT_2:def 3;

        hence thesis by A1, FUNCT_2: 25;

      end;

    end

    notation

      let S,T be set, f be Function of S, T;

      synonym f " for f /" ;

    end

    theorem :: TOPS_2:49

    

     Th49: for T be 1-sorted, S be non empty 1-sorted, f be Function of T, S st ( rng f) = ( [#] S) & f is one-to-one holds ( dom (f " )) = ( [#] S) & ( rng (f " )) = ( [#] T)

    proof

      let T be 1-sorted, S be non empty 1-sorted, f be Function of T, S;

      assume that

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

       A2: f is one-to-one;

      

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

      

      hence ( dom (f " )) = ( dom (f qua Function " )) by A2, Def4

      .= ( [#] S) by A1, A2, FUNCT_1: 32;

      

      thus ( rng (f " )) = ( rng (f qua Function " )) by A2, A3, Def4

      .= ( dom f) by A2, FUNCT_1: 33

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

    end;

    theorem :: TOPS_2:50

    

     Th50: for T,S be 1-sorted, f be Function of T, S st ( rng f) = ( [#] S) & f is one-to-one holds (f " ) is one-to-one

    proof

      let T,S be 1-sorted, f be Function of T, S;

      assume that

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

       A2: f is one-to-one;

      

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

      (f qua Function " ) is one-to-one by A2;

      hence thesis by A2, A3, Def4;

    end;

    theorem :: TOPS_2:51

    

     Th51: for T be 1-sorted, S be non empty 1-sorted, f be Function of T, S st ( rng f) = ( [#] S) & f is one-to-one holds ((f " ) " ) = f

    proof

      let T be 1-sorted, S be non empty 1-sorted, f be Function of T, S;

      assume that

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

       A2: f is one-to-one;

      

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

      f = ((f qua Function " ) " ) by A2, FUNCT_1: 43;

      then

       A4: f = ((f " ) qua Function " ) by A3, A2, Def4;

      

       A5: (f " ) is one-to-one by A1, A2, Th50;

      ( rng (f " )) = ( [#] T) by A1, A2, Th49;

      then (f " ) is onto by FUNCT_2:def 3;

      hence thesis by A4, A5, Def4;

    end;

    theorem :: TOPS_2:52

    for T,S be 1-sorted, f be Function of T, S st ( rng f) = ( [#] S) & f is one-to-one holds ((f " ) * f) = ( id ( dom f)) & (f * (f " )) = ( id ( rng f))

    proof

      let T,S be 1-sorted, f be Function of T, S;

      assume that

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

       A2: f is one-to-one;

      

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

      ((f qua Function " ) * f) = ( id ( dom f)) & (f * (f qua Function " )) = ( id ( rng f)) by A2, FUNCT_1: 39;

      hence thesis by A2, A3, Def4;

    end;

    theorem :: TOPS_2:53

    

     Th53: for T be 1-sorted, S,V be non empty 1-sorted, f be Function of T, S, g be Function of S, V st ( rng f) = ( [#] S) & f is one-to-one & ( dom g) = ( [#] S) & ( rng g) = ( [#] V) & g is one-to-one holds ((g * f) " ) = ((f " ) * (g " ))

    proof

      let T be 1-sorted, S,V be non empty 1-sorted;

      let f be Function of T, S;

      let g be Function of S, V;

      assume that

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

       A2: f is one-to-one;

      assume that

       A3: ( dom g) = ( [#] S) and

       A4: ( rng g) = ( [#] V) and

       A5: g is one-to-one;

      

       A6: f is onto & g is onto by A1, A4, FUNCT_2:def 3;

      ( rng (g * f)) = ( [#] V) by A1, A3, A4, RELAT_1: 28;

      then (g * f) is onto by FUNCT_2:def 3;

      then

       A7: ((g * f) " ) = ((g * f) qua Function " ) by A2, A5, Def4;

      

       A8: (f " ) = (f qua Function " ) by A2, A6, Def4;

      (g " ) = (g qua Function " ) by A5, A6, Def4;

      hence thesis by A2, A5, A8, A7, FUNCT_1: 44;

    end;

    theorem :: TOPS_2:54

    

     Th54: for T,S be 1-sorted, f be Function of T, S, P be Subset of T st ( rng f) = ( [#] S) & f is one-to-one holds (f .: P) = ((f " ) " P)

    proof

      let T,S be 1-sorted, f be Function of T, S, P be Subset of T;

      assume that

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

       A2: f is one-to-one;

      

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

      (f .: P) = ((f qua Function " ) " P) by A2, FUNCT_1: 84;

      hence thesis by A2, A3, Def4;

    end;

    theorem :: TOPS_2:55

    

     Th55: for T,S be 1-sorted, f be Function of T, S, P1 be Subset of S st ( rng f) = ( [#] S) & f is one-to-one holds (f " P1) = ((f " ) .: P1)

    proof

      let T,S be 1-sorted, f be Function of T, S, P1 be Subset of S;

      assume ( rng f) = ( [#] S);

      then

       A1: f is onto by FUNCT_2:def 3;

      assume

       A2: f is one-to-one;

      (f " P1) = ((f qua Function " ) .: P1) by A2, FUNCT_1: 85;

      hence thesis by A1, A2, Def4;

    end;

    definition

      let S,T be TopStruct, f be Function of S, T;

      :: TOPS_2:def5

      attr f is being_homeomorphism means ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one & f is continuous & (f " ) is continuous;

    end

    theorem :: TOPS_2:56

    f is being_homeomorphism implies (f " ) is being_homeomorphism by Th49, Th50, Th51;

    theorem :: TOPS_2:57

    for T,S,V be non empty TopStruct, f be Function of T, S, g be Function of S, V st f is being_homeomorphism & g is being_homeomorphism holds (g * f) is being_homeomorphism

    proof

      let T,S,V be non empty TopStruct;

      let f be Function of T, S;

      let g be Function of S, V;

      assume that

       A1: f is being_homeomorphism and

       A2: g is being_homeomorphism;

      

       A3: ( rng f) = ( [#] S) & ( dom g) = ( [#] S) by A1, A2;

      

       A4: ( rng g) = ( [#] V) by A2;

      ( dom f) = ( [#] T) by A1;

      hence ( dom (g * f)) = ( [#] T) & ( rng (g * f)) = ( [#] V) by A3, A4, RELAT_1: 27, RELAT_1: 28;

      

       A5: f is one-to-one & g is one-to-one by A1, A2;

      hence (g * f) is one-to-one;

      f is continuous & g is continuous by A1, A2;

      hence (g * f) is continuous by Th46;

      (f " ) is continuous & (g " ) is continuous by A1, A2;

      then ((f " ) * (g " )) is continuous by Th46;

      hence thesis by A3, A4, A5, Th53;

    end;

    theorem :: TOPS_2:58

    f is being_homeomorphism iff ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one & for P holds P is closed iff (f .: P) is closed

    proof

      hereby

        assume

         A1: f is being_homeomorphism;

        hence

         A2: ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one;

        let P;

        

         A3: (f " ) is continuous by A1;

        hereby

          assume

           A4: P is closed;

          f is onto by A2, FUNCT_2:def 3;

          

          then ((f " ) " P) = ((f qua Function " ) " P) by A2, Def4

          .= (f .: P) by A2, FUNCT_1: 84;

          hence (f .: P) is closed by A3, A4;

        end;

        assume

         A5: (f .: P) is closed;

        f is continuous by A1;

        then

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

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

        then

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

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

        hence P is closed by A6, A7, XBOOLE_0:def 10;

      end;

      assume that

       A8: ( dom f) = ( [#] T) and

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

       A10: f is one-to-one;

      assume

       A11: for P be Subset of T holds P is closed iff (f .: P) is closed;

      

       A12: f is continuous

      proof

        let B be Subset of S such that

         A13: B is closed;

        set D = (f " B);

        B = (f .: D) by A9, FUNCT_1: 77;

        hence thesis by A11, A13;

      end;

      (f " ) is continuous

      proof

        let B be Subset of T such that

         A14: B is closed;

        f is onto by A9, FUNCT_2:def 3;

        

        then ((f " ) " B) = ((f qua Function " ) " B) by A10, Def4

        .= (f .: B) by A10, FUNCT_1: 84;

        hence thesis by A11, A14;

      end;

      hence thesis by A8, A9, A10, A12;

    end;

    reserve T for non empty TopSpace,

S for TopSpace,

P1 for Subset of S,

f for Function of T, S;

    theorem :: TOPS_2:59

    f is being_homeomorphism iff ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one & for P1 holds (f " ( Cl P1)) = ( Cl (f " P1))

    proof

      hereby

        assume

         A1: f is being_homeomorphism;

        hence

         A2: ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one;

        let P1;

        f is continuous by A1;

        then

         A3: ( Cl (f " P1)) c= (f " ( Cl P1)) by Th44;

        (f " ) is continuous by A1;

        then

         A4: ((f " ) .: ( Cl P1)) c= ( Cl ((f " ) .: P1)) by Th45;

        (f " ( Cl P1)) = ((f " ) .: ( Cl P1)) & (f " P1) = ((f " ) .: P1) by A2, Th55;

        hence (f " ( Cl P1)) = ( Cl (f " P1)) by A3, A4, XBOOLE_0:def 10;

      end;

      assume that

       A5: ( dom f) = ( [#] T) and

       A6: ( rng f) = ( [#] S) & f is one-to-one;

      assume

       A7: for P1 holds (f " ( Cl P1)) = ( Cl (f " P1));

      thus ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one by A5, A6;

      for P1 holds ( Cl (f " P1)) c= (f " ( Cl P1)) by A7;

      hence f is continuous by Th44;

      now

        let P1;

        ((f " ) .: ( Cl P1)) = (f " ( Cl P1)) & ((f " ) .: P1) = (f " P1) by A6, Th55;

        hence ((f " ) .: ( Cl P1)) c= ( Cl ((f " ) .: P1)) by A7;

      end;

      hence thesis by Th45;

    end;

    reserve T for TopSpace,

S for non empty TopSpace,

P for Subset of T,

f for Function of T, S;

    theorem :: TOPS_2:60

    f is being_homeomorphism iff ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one & for P holds (f .: ( Cl P)) = ( Cl (f .: P))

    proof

      hereby

        assume

         A1: f is being_homeomorphism;

        hence

         A2: ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one;

        let P;

        f is continuous by A1;

        then

         A3: (f .: ( Cl P)) c= ( Cl (f .: P)) by Th45;

        (f " ) is continuous by A1;

        then

         A4: ( Cl ((f " ) " P)) c= ((f " ) " ( Cl P)) by Th44;

        ((f " ) " P) = (f .: P) & ((f " ) " ( Cl P)) = (f .: ( Cl P)) by A2, Th54;

        hence (f .: ( Cl P)) = ( Cl (f .: P)) by A3, A4, XBOOLE_0:def 10;

      end;

      assume that

       A5: ( dom f) = ( [#] T) and

       A6: ( rng f) = ( [#] S) & f is one-to-one;

      assume

       A7: for P holds (f .: ( Cl P)) = ( Cl (f .: P));

      thus ( dom f) = ( [#] T) & ( rng f) = ( [#] S) & f is one-to-one by A5, A6;

      for P holds (f .: ( Cl P)) c= ( Cl (f .: P)) by A7;

      hence f is continuous by Th45;

      now

        let P;

        ((f " ) " P) = (f .: P) & ((f " ) " ( Cl P)) = (f .: ( Cl P)) by A6, Th54;

        hence ( Cl ((f " ) " P)) c= ((f " ) " ( Cl P)) by A7;

      end;

      hence thesis by Th44;

    end;

    theorem :: TOPS_2:61

    

     Th61: for X,Y be non empty TopSpace holds for f be Function of X, Y, A be Subset of X st f is continuous & A is connected holds (f .: A) is connected

    proof

      let X,Y be non empty TopSpace;

      let f be Function of X, Y, A be Subset of X;

      assume

       A1: f is continuous;

      assume

       A2: A is connected;

      assume not (f .: A) is connected;

      then

      consider P,Q be Subset of Y such that

       A3: (f .: A) = (P \/ Q) and

       A4: (P,Q) are_separated and

       A5: P <> ( {} Y) and

       A6: Q <> ( {} Y) by CONNSP_1: 15;

      reconsider P1 = (f " P), Q1 = (f " Q) as Subset of X;

      set P2 = (P1 /\ A), Q2 = (Q1 /\ A);

      set y = the Element of P;

      y in (f .: A) by A3, A5, XBOOLE_0:def 3;

      then

      consider x be object such that

       A7: x in ( dom f) and

       A8: x in A and

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

      x in (f " P) by A5, A7, A9, FUNCT_1:def 7;

      then

       A10: P2 <> {} by A8, XBOOLE_0:def 4;

      

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

      P misses ( Cl Q) by A4, CONNSP_1:def 1;

      then

       A12: ((f " P) /\ (f " ( Cl Q))) = (f " (P /\ ( Cl Q))) & (f " (P /\ ( Cl Q))) = (f " ( {} Y)) by FUNCT_1: 68, XBOOLE_0:def 7;

      ( Cl Q1) c= (f " ( Cl Q)) by A1, Th44;

      then (P1 /\ ( Cl Q1)) = {} by A12, XBOOLE_1: 3, XBOOLE_1: 26;

      then

       A13: P1 misses ( Cl Q1) by XBOOLE_0:def 7;

      ( Cl P) misses Q by A4, CONNSP_1:def 1;

      then

       A14: ((f " ( Cl P)) /\ (f " Q)) = (f " (( Cl P) /\ Q)) & (f " (( Cl P) /\ Q)) = (f " ( {} Y)) by FUNCT_1: 68, XBOOLE_0:def 7;

      ( Cl P1) c= (f " ( Cl P)) by A1, Th44;

      then (( Cl P1) /\ Q1) = ( {} X) by A14, XBOOLE_1: 3, XBOOLE_1: 26;

      then ( Cl P1) misses Q1 by XBOOLE_0:def 7;

      then

       A15: (P1,Q1) are_separated by A13, CONNSP_1:def 1;

      set z = the Element of Q;

      z in (P \/ Q) by A6, XBOOLE_0:def 3;

      then

      consider x1 be object such that

       A16: x1 in ( dom f) and

       A17: x1 in A and

       A18: z = (f . x1) by A3, FUNCT_1:def 6;

      x1 in (f " Q) by A6, A16, A18, FUNCT_1:def 7;

      then

       A19: Q2 <> {} by A17, XBOOLE_0:def 4;

      (f " (f .: A)) = ((f " P) \/ (f " Q)) by A3, RELAT_1: 140;

      

      then

       A20: A = ((P1 \/ Q1) /\ A) by A11, FUNCT_1: 76, XBOOLE_1: 28

      .= (P2 \/ Q2) by XBOOLE_1: 23;

      P2 c= P1 & Q2 c= Q1 by XBOOLE_1: 17;

      then ex P3,Q3 be Subset of X st A = (P3 \/ Q3) & (P3,Q3) are_separated & P3 <> ( {} X) & Q3 <> ( {} X) by A15, A20, A10, A19, CONNSP_1: 7;

      hence contradiction by A2, CONNSP_1: 15;

    end;

    theorem :: TOPS_2:62

    for S,T be non empty TopSpace, f be Function of S, T, A be Subset of T st f is being_homeomorphism & A is connected holds (f " A) is connected

    proof

      let S,T be non empty TopSpace, f be Function of S, T, A be Subset of T such that

       A1: f is being_homeomorphism and

       A2: A is connected;

      (f " ) is continuous by A1;

      then

       A3: ((f " ) .: A) is connected by A2, Th61;

      ( rng f) = ( [#] T) & f is one-to-one by A1;

      hence thesis by A3, Th55;

    end;

    begin

    reserve GX,GY for non empty TopSpace;

    theorem :: TOPS_2:63

    for GX be non empty TopSpace st (for x,y be Point of GX holds ex GY st (GY is connected & ex f be Function of GY, GX st f is continuous & x in ( rng f) & y in ( rng f))) holds GX is connected

    proof

      let GX;

      assume

       A1: for x,y be Point of GX holds ex GY st (GY is connected & ex f be Function of GY, GX st f is continuous & x in ( rng f) & y in ( rng f));

      for A,B be Subset of GX st ( [#] GX) = (A \/ B) & A <> ( {} GX) & B <> ( {} GX) & A is open & B is open holds A meets B

      proof

        let A,B be Subset of GX;

        assume that

         A2: ( [#] GX) = (A \/ B) and

         A3: A <> ( {} GX) and

         A4: B <> ( {} GX) and

         A5: A is open & B is open;

        set v = the Element of B;

        set u = the Element of A;

        reconsider y = v as Point of GX by A2, A4, XBOOLE_0:def 3;

        reconsider x = u as Point of GX by A2, A3, XBOOLE_0:def 3;

        consider GY such that

         A6: GY is connected and

         A7: ex f be Function of GY, GX st f is continuous & x in ( rng f) & y in ( rng f) by A1;

        consider f be Function of GY, GX such that

         A8: f is continuous and

         A9: x in ( rng f) and

         A10: y in ( rng f) by A7;

        (f " ( [#] GX)) = ( [#] GY) by Th41;

        then

         A11: ((f " A) \/ (f " B)) = ( [#] GY) by A2, RELAT_1: 140;

        (( rng f) /\ B) <> {} by A4, A10, XBOOLE_0:def 4;

        then ( rng f) meets B by XBOOLE_0:def 7;

        then

         A12: (f " B) <> ( {} GY) by RELAT_1: 138;

        (( rng f) /\ A) <> {} by A3, A9, XBOOLE_0:def 4;

        then ( rng f) meets A by XBOOLE_0:def 7;

        then

         A13: (f " A) <> ( {} GY) by RELAT_1: 138;

        ( [#] GX) <> {} ;

        then (f " A) is open & (f " B) is open by A5, A8, Th43;

        then (f " A) meets (f " B) by A6, A11, A13, A12, CONNSP_1: 11;

        then ((f " A) /\ (f " B)) <> {} by XBOOLE_0:def 7;

        then (f " (A /\ B)) <> {} by FUNCT_1: 68;

        then ( rng f) meets (A /\ B) by RELAT_1: 138;

        then ex u1 be object st u1 in ( rng f) & u1 in (A /\ B) by XBOOLE_0: 3;

        hence thesis by XBOOLE_0: 4;

      end;

      hence thesis by CONNSP_1: 11;

    end;

    theorem :: TOPS_2:64

    

     Th64: for X be TopStruct, F be Subset-Family of X holds F is open iff F c= the topology of X

    proof

      let X be TopStruct, F be Subset-Family of X;

      thus F is open implies F c= the topology of X

      proof

        assume

         A1: F is open;

        let A be object;

        assume

         A2: A in F;

        then

        reconsider A as Subset of X;

        A is open by A1, A2;

        hence thesis;

      end;

      assume

       A3: F c= the topology of X;

      let A be Subset of X;

      thus thesis by A3;

    end;

    theorem :: TOPS_2:65

    for X be TopStruct, F be Subset-Family of X holds F is closed iff F c= ( COMPLEMENT the topology of X)

    proof

      let X be TopStruct, F be Subset-Family of X;

      thus F is closed implies F c= ( COMPLEMENT the topology of X)

      proof

        assume

         A1: F is closed;

        let A be object;

        assume

         A2: A in F;

        then

        reconsider A as Subset of X;

        A is closed by A1, A2;

        then (A ` ) is open;

        then (A ` ) in the topology of X;

        hence thesis by SETFAM_1:def 7;

      end;

      assume

       A3: F c= ( COMPLEMENT the topology of X);

      let A be Subset of X;

      assume A in F;

      then (A ` ) in the topology of X by A3, SETFAM_1:def 7;

      then (A ` ) is open;

      hence thesis;

    end;

    registration

      let X be TopStruct;

      cluster the topology of X -> open;

      coherence by Th64;

      cluster open for Subset-Family of X;

      existence

      proof

        take the topology of X;

        thus thesis;

      end;

    end