topgen_4.miz



    begin

    definition

      let T be 1-sorted;

      :: TOPGEN_4:def1

      func TotFam T -> Subset-Family of T equals ( bool the carrier of T);

      coherence by ZFMISC_1:def 1;

    end

    theorem :: TOPGEN_4:1

    

     Th1: for T be set, F be Subset-Family of T holds F is countable iff ( COMPLEMENT F) is countable

    proof

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

      (F,( COMPLEMENT F)) are_equipotent by YELLOW_8: 3;

      hence thesis by YELLOW_8: 4;

    end;

    registration

      cluster RAT -> countable;

      coherence by TOPGEN_3: 17;

    end

    

     Lm1: for X be set holds X is countable iff ex f be Function st ( dom f) = RAT & X c= ( rng f) by CARD_1: 12, TOPGEN_3: 17;

    scheme :: TOPGEN_4:sch1

    FraenCoun11 { P[ set] } :

{ {n} where n be Element of RAT : P[n] } is countable;

      deffunc g( object) = {$1};

      consider f be Function such that

       A1: ( dom f) = RAT & for x be object st x in RAT holds (f . x) = g(x) from FUNCT_1:sch 3;

      { {n} where n be Element of RAT : P[n] } c= ( rng f)

      proof

        let x be object;

        assume x in { {n} where n be Element of RAT : P[n] };

        then

        consider n be Element of RAT such that

         A2: x = {n} and P[n];

        (f . n) = x by A1, A2;

        hence thesis by A1, FUNCT_1:def 3;

      end;

      hence thesis by A1, Lm1;

    end;

    theorem :: TOPGEN_4:2

    for T be non empty TopSpace, A be Subset of T holds ( Der A) = { x where x be Point of T : x in ( Cl (A \ {x})) }

    proof

      let T be non empty TopSpace, A be Subset of T;

      thus ( Der A) c= { x where x be Point of T : x in ( Cl (A \ {x})) }

      proof

        let x be object;

        assume x in ( Der A);

        then x is_an_accumulation_point_of A by TOPGEN_1:def 3;

        then x in ( Cl (A \ {x})) by TOPGEN_1:def 2;

        hence thesis;

      end;

      let y be object;

      assume y in { x where x be Point of T : x in ( Cl (A \ {x})) };

      then

      consider z be Point of T such that

       A1: z = y and

       A2: z in ( Cl (A \ {z}));

      z is_an_accumulation_point_of A by A2, TOPGEN_1:def 2;

      hence thesis by A1, TOPGEN_1:def 3;

    end;

    registration

      cluster finite -> second-countable for TopStruct;

      coherence

      proof

        let T be TopStruct;

        assume T is finite;

        then

        reconsider T9 = T as finite TopStruct;

        ( weight T9) is finite by TOPGEN_2:def 4;

        then ( weight T9) c= omega ;

        hence thesis by WAYBEL23:def 6;

      end;

    end

    registration

      cluster REAL -> non countable;

      coherence by TOPGEN_3: 30, TOPGEN_3:def 4;

    end

    registration

      cluster non countable -> non finite for set;

      coherence ;

      cluster non finite -> non trivial for set;

      coherence ;

      cluster non countable non empty for set;

      existence

      proof

        take REAL ;

        thus thesis;

      end;

    end

    reserve T for non empty TopSpace,

A,B for Subset of T,

F,G for Subset-Family of T;

    theorem :: TOPGEN_4:3

    A is closed iff ( Der A) c= A

    proof

      hereby

        assume A is closed;

        then

         A1: A = ( Cl A) by PRE_TOPC: 22;

        ( Cl A) = (A \/ ( Der A)) by TOPGEN_1: 29;

        hence ( Der A) c= A by A1, XBOOLE_1: 7;

      end;

      assume

       A2: ( Der A) c= A;

      ( Cl A) = (A \/ ( Der A)) by TOPGEN_1: 29

      .= A by A2, XBOOLE_1: 12;

      hence thesis;

    end;

    theorem :: TOPGEN_4:4

    

     Th4: for T be non empty TopStruct, B be Basis of T, V be Subset of T st V is open & V <> {} holds ex W be Subset of T st W in B & W c= V & W <> {}

    proof

      let T be non empty TopStruct, B be Basis of T, V be Subset of T;

      assume that

       A1: V is open and

       A2: V <> {} ;

      consider x be object such that

       A3: x in V by A2, XBOOLE_0:def 1;

      V = ( union { G where G be Subset of T : G in B & G c= V }) by A1, YELLOW_8: 9;

      then

      consider Y be set such that

       A4: x in Y and

       A5: Y in { G where G be Subset of T : G in B & G c= V } by A3, TARSKI:def 4;

      ex Z be Subset of T st Z = Y & Z in B & Z c= V by A5;

      hence thesis by A4;

    end;

    begin

    theorem :: TOPGEN_4:5

    

     Th5: ( density T) c= ( weight T)

    proof

      defpred P[ set] means $1 <> {} ;

      deffunc F( set) = the Element of $1;

      set B = the Basis of T;

      consider B1 be Basis of T such that B1 c= B and

       A1: ( card B1) = ( weight T) by TOPGEN_2: 18;

      set A = { F(BB) where BB be Element of ( bool the carrier of T) : BB in B1 & P[BB] };

      A c= the carrier of T

      proof

        let x be object;

        assume x in A;

        then

        consider B2 be Subset of T such that

         A2: x = the Element of B2 and B2 in B1 and

         A3: B2 <> {} ;

        x in B2 by A2, A3;

        hence thesis;

      end;

      then

      reconsider A as Subset of T;

      for Q be Subset of T st Q <> {} & Q is open holds A meets Q

      proof

        let Q be Subset of T;

        assume Q <> {} & Q is open;

        then

        consider W be Subset of T such that

         A4: W in B1 and

         A5: W c= Q and

         A6: W <> {} by Th4;

         the Element of W in A & the Element of W in W by A4, A6;

        hence thesis by A5, XBOOLE_0: 3;

      end;

      then A is dense by TOPS_1: 45;

      then

       A7: ( density T) c= ( card A) by TOPGEN_1:def 12;

      ( card { F(w) where w be Element of ( bool the carrier of T) : w in B1 & P[w] }) c= ( card B1) from BORSUK_2:sch 1;

      hence thesis by A1, A7;

    end;

    theorem :: TOPGEN_4:6

    T is separable iff ex A be Subset of T st A is dense countable

    proof

      hereby

        consider A be Subset of T such that

         A1: A is dense and

         A2: ( density T) = ( card A) by TOPGEN_1:def 12;

        assume T is separable;

        then ( density T) c= omega by TOPGEN_1:def 13;

        then A is countable by A2;

        hence ex A be Subset of T st A is dense countable by A1;

      end;

      given A be Subset of T such that

       A3: A is dense countable;

      ( density T) c= ( card A) & ( card A) c= omega by A3, TOPGEN_1:def 12;

      then ( density T) c= omega ;

      hence thesis by TOPGEN_1:def 13;

    end;

    theorem :: TOPGEN_4:7

    

     Th7: T is second-countable implies T is separable

    proof

      assume T is second-countable;

      then

       A1: ( weight T) c= omega by WAYBEL23:def 6;

      ( density T) c= ( weight T) by Th5;

      then ( density T) c= omega by A1;

      hence thesis by TOPGEN_1:def 13;

    end;

    registration

      cluster second-countable -> separable for non empty TopSpace;

      coherence by Th7;

    end

    theorem :: TOPGEN_4:8

    for T be non empty TopSpace, A,B be Subset of T st (A,B) are_separated holds ( Fr (A \/ B)) = (( Fr A) \/ ( Fr B))

    proof

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

      

       A1: (( Fr A) \/ ( Fr B)) = ((( Fr (A \/ B)) \/ ( Fr (A /\ B))) \/ (( Fr A) /\ ( Fr B))) & ( Fr ( {} T)) = {} by TOPS_1: 36;

      assume

       A2: (A,B) are_separated ;

      then

       A3: A misses ( Cl B) by CONNSP_1:def 1;

      A misses B by A2, CONNSP_1: 1;

      then

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

      

       A5: ( Cl A) misses B by A2, CONNSP_1:def 1;

      

       A6: (( Fr A) \/ ( Fr B)) c= ( Fr (A \/ B))

      proof

        let x be object;

        assume

         A7: x in (( Fr A) \/ ( Fr B));

        per cases by A4, A1, A7, XBOOLE_0:def 3;

          suppose x in ( Fr (A \/ B));

          hence thesis;

        end;

          suppose

           A8: x in (( Fr A) /\ ( Fr B));

          then x in ( Fr B) by XBOOLE_0:def 4;

          then x in (( Cl B) /\ ( Cl (B ` ))) by TOPS_1:def 2;

          then x in ( Cl B) by XBOOLE_0:def 4;

          then not x in A by A3, XBOOLE_0: 3;

          then

           A9: x in (A ` ) by A7, XBOOLE_0:def 5;

          x in ( Fr A) by A8, XBOOLE_0:def 4;

          then x in (( Cl A) /\ ( Cl (A ` ))) by TOPS_1:def 2;

          then

           A10: x in ( Cl A) by XBOOLE_0:def 4;

          then x in (( Cl A) \/ ( Cl B)) by XBOOLE_0:def 3;

          then

           A11: x in ( Cl (A \/ B)) by PRE_TOPC: 20;

           not x in B by A5, A10, XBOOLE_0: 3;

          then x in (B ` ) by A7, XBOOLE_0:def 5;

          then x in ((A ` ) /\ (B ` )) by A9, XBOOLE_0:def 4;

          then

           A12: x in ((A \/ B) ` ) by XBOOLE_1: 53;

          ((A \/ B) ` ) c= ( Cl ((A \/ B) ` )) by PRE_TOPC: 18;

          then x in (( Cl (A \/ B)) /\ ( Cl ((A \/ B) ` ))) by A11, A12, XBOOLE_0:def 4;

          hence thesis by TOPS_1:def 2;

        end;

      end;

      ( Fr (A \/ B)) c= (( Fr A) \/ ( Fr B)) by TOPS_1: 33;

      hence thesis by A6;

    end;

    theorem :: TOPGEN_4:9

    F is locally_finite implies ( Fr ( union F)) c= ( union ( Fr F))

    proof

      assume F is locally_finite;

      then

       A1: ( Cl ( union F)) = ( union ( clf F)) by PCOMPS_1: 20;

      let x be object;

      assume x in ( Fr ( union F));

      then

       A2: x in (( Cl ( union F)) /\ ( Cl (( union F) ` ))) by TOPS_1:def 2;

      then

       A3: x in ( Cl (( union F) ` )) by XBOOLE_0:def 4;

      x in ( Cl ( union F)) by A2, XBOOLE_0:def 4;

      then

      consider A be set such that

       A4: x in A and

       A5: A in ( clf F) by A1, TARSKI:def 4;

      consider B be Subset of T such that

       A6: A = ( Cl B) and

       A7: B in F by A5, PCOMPS_1:def 2;

      B c= ( union F) by A7, ZFMISC_1: 74;

      then (( union F) ` ) c= (B ` ) by SUBSET_1: 12;

      then ( Cl (( union F) ` )) c= ( Cl (B ` )) by PRE_TOPC: 19;

      then x in (( Cl B) /\ ( Cl (B ` ))) by A4, A6, A3, XBOOLE_0:def 4;

      then

       A8: x in ( Fr B) by TOPS_1:def 2;

      ( Fr B) in ( Fr F) by A7, TOPGEN_1:def 1;

      hence thesis by A8, TARSKI:def 4;

    end;

    theorem :: TOPGEN_4:10

    

     Th10: for T be discrete non empty TopSpace holds T is separable iff ( card ( [#] T)) c= omega

    proof

      let T be discrete non empty TopSpace;

      hereby

        assume T is separable;

        then

         A1: ( density T) c= omega by TOPGEN_1:def 13;

        ex A be Subset of T st A is dense & ( density T) = ( card A) by TOPGEN_1:def 12;

        hence ( card ( [#] T)) c= omega by A1, TOPS_3: 19;

      end;

      assume ( card ( [#] T)) c= omega ;

      then T is countable by TOPGEN_1: 2;

      hence thesis;

    end;

    theorem :: TOPGEN_4:11

    for T be discrete non empty TopSpace holds T is separable iff T is countable

    proof

      let T be discrete non empty TopSpace;

      T is separable iff ( card ( [#] T)) c= omega by Th10;

      hence thesis by TOPGEN_1: 2;

    end;

    begin

    definition

      let T, F;

      :: TOPGEN_4:def2

      attr F is all-open-containing means

      : Def2: for A be Subset of T st A is open holds A in F;

    end

    definition

      let T, F;

      :: TOPGEN_4:def3

      attr F is all-closed-containing means

      : Def3: for A be Subset of T st A is closed holds A in F;

    end

    definition

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

      :: TOPGEN_4:def4

      attr F is closed_for_countable_unions means

      : Def4: for G be countable Subset-Family of T st G c= F holds ( union G) in F;

    end

    

     Lm2: for T be set, F be Subset-Family of T st F is SigmaField of T holds F is closed_for_countable_unions

    proof

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

      assume

       A1: F is SigmaField of T;

      let G be countable Subset-Family of T;

      assume

       A2: G c= F;

      per cases ;

        suppose G is empty;

        hence thesis by A1, PROB_1: 4, ZFMISC_1: 2;

      end;

        suppose G is non empty;

        hence thesis by A1, A2, MEASURE1:def 5;

      end;

    end;

    registration

      let T be set;

      cluster -> closed_for_countable_unions for SigmaField of T;

      coherence by Lm2;

    end

    theorem :: TOPGEN_4:12

    for T be set, F be Subset-Family of T st F is closed_for_countable_unions holds {} in F

    proof

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

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

      

       A1: E c= F;

      assume F is closed_for_countable_unions;

      hence thesis by A1, ZFMISC_1: 2;

    end;

    registration

      let T be set;

      cluster closed_for_countable_unions -> non empty for Subset-Family of T;

      coherence ;

    end

    theorem :: TOPGEN_4:13

    

     Th13: for T be set, F be Subset-Family of T holds F is SigmaField of T iff F is compl-closed closed_for_countable_unions

    proof

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

      thus F is SigmaField of T implies F is compl-closed closed_for_countable_unions;

      assume

       A1: F is compl-closed closed_for_countable_unions;

      F is sigma-additive by A1;

      then

      reconsider F as non empty compl-closed sigma-additive Subset-Family of T by A1;

      F is SigmaField of T;

      hence thesis;

    end;

    definition

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

      :: TOPGEN_4:def5

      attr F is closed_for_countable_meets means

      : Def5: for G be countable Subset-Family of T st G c= F holds ( meet G) in F;

    end

    theorem :: TOPGEN_4:14

    

     Th14: for F be Subset-Family of T holds F is all-closed-containing compl-closed iff F is all-open-containing compl-closed

    proof

      let F be Subset-Family of T;

      hereby

        assume

         A1: F is all-closed-containing compl-closed;

        for A be Subset of T st A is open holds A in F

        proof

          let A be Subset of T;

          assume A is open;

          then (A ` ) in F by A1;

          then ((A ` ) ` ) in F by A1;

          hence thesis;

        end;

        hence F is all-open-containing compl-closed by A1;

      end;

      assume

       A2: F is all-open-containing compl-closed;

      for A be Subset of T st A is closed holds A in F

      proof

        let A be Subset of T;

        assume A is closed;

        then (A ` ) in F by A2;

        then ((A ` ) ` ) in F by A2;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: TOPGEN_4:15

    for T be set, F be Subset-Family of T st F is compl-closed holds F = ( COMPLEMENT F)

    proof

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

      assume

       A1: F is compl-closed;

      thus F c= ( COMPLEMENT F)

      proof

        let x be object;

        assume

         A2: x in F;

        then

        reconsider x9 = x as Subset of T;

        (x9 ` ) in F by A1, A2;

        hence thesis by SETFAM_1:def 7;

      end;

      let x be object;

      assume

       A3: x in ( COMPLEMENT F);

      then

      reconsider x9 = x as Subset of T;

      (x9 ` ) in F by A3, SETFAM_1:def 7;

      then ((x9 ` ) ` ) in F by A1;

      hence thesis;

    end;

    theorem :: TOPGEN_4:16

    

     Th16: for T be set, F,G be Subset-Family of T st F c= G & G is compl-closed holds ( COMPLEMENT F) c= G

    proof

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

      assume

       A1: F c= G & G is compl-closed;

      let x be object;

      assume

       A2: x in ( COMPLEMENT F);

      then

      reconsider x9 = x as Subset of T;

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

      then ((x9 ` ) ` ) in G by A1;

      hence thesis;

    end;

    theorem :: TOPGEN_4:17

    

     Th17: for T be set, F be Subset-Family of T holds F is closed_for_countable_meets compl-closed iff F is closed_for_countable_unions compl-closed

    proof

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

      hereby

        assume

         A1: F is closed_for_countable_meets compl-closed;

        for G be countable Subset-Family of T st G c= F holds ( union G) in F

        proof

          let G be countable Subset-Family of T;

          assume

           A2: G c= F;

          per cases ;

            suppose G = {} ;

            hence thesis by A1, A2, SETFAM_1: 1, ZFMISC_1: 2;

          end;

            suppose G <> {} ;

            then

            reconsider G9 = G as non empty Subset-Family of T;

            ( COMPLEMENT G9) c= F & ( COMPLEMENT G9) is countable by A1, A2, Th1, Th16;

            then

             A3: ( meet ( COMPLEMENT G9)) in F by A1;

            (( meet ( COMPLEMENT G9)) ` ) = ((( union G9) ` ) ` ) by TOPS_2: 6

            .= ( union G9);

            hence thesis by A1, A3;

          end;

        end;

        hence F is closed_for_countable_unions compl-closed by A1;

      end;

      assume

       A4: F is closed_for_countable_unions compl-closed;

      for G be countable Subset-Family of T st G c= F holds ( meet G) in F

      proof

        let G be countable Subset-Family of T;

        assume

         A5: G c= F;

        per cases ;

          suppose G = {} ;

          hence thesis by A4, A5, SETFAM_1: 1, ZFMISC_1: 2;

        end;

          suppose G <> {} ;

          then

          reconsider G9 = G as non empty Subset-Family of T;

          ( COMPLEMENT G9) c= F & ( COMPLEMENT G9) is countable by A4, A5, Th1, Th16;

          then

           A6: ( union ( COMPLEMENT G9)) in F by A4;

          (( union ( COMPLEMENT G9)) ` ) = ((( meet G9) ` ) ` ) by TOPS_2: 7

          .= ( meet G9);

          hence thesis by A4, A6;

        end;

      end;

      hence thesis by A4;

    end;

    registration

      let T;

      cluster all-open-containing compl-closed closed_for_countable_unions -> all-closed-containing closed_for_countable_meets for Subset-Family of T;

      coherence by Th14, Th17;

      cluster all-closed-containing compl-closed closed_for_countable_meets -> all-open-containing closed_for_countable_unions for Subset-Family of T;

      coherence by Th14, Th17;

    end

    begin

    registration

      let T be set;

      let F be countable Subset-Family of T;

      cluster ( COMPLEMENT F) -> countable;

      coherence by Th1;

    end

    registration

      let T be TopSpace;

      cluster empty -> open closed for Subset-Family of T;

      coherence

      proof

        let F be Subset-Family of T;

        assume F is empty;

        then (for P be Subset of T holds P in F implies P is open) & for P be Subset of T holds P in F implies P is closed;

        hence thesis by TOPS_2:def 1, TOPS_2:def 2;

      end;

    end

    registration

      let T be TopSpace;

      cluster countable open closed for Subset-Family of T;

      existence

      proof

        ( {} ( bool the carrier of T)) is open;

        hence thesis;

      end;

    end

    theorem :: TOPGEN_4:18

    

     Th18: for T be set holds {} is empty Subset-Family of T

    proof

      let T be set;

      ( {} ( bool T)) = {} ;

      hence thesis;

    end;

    registration

      cluster empty -> countable for set;

      coherence ;

    end

    begin

    theorem :: TOPGEN_4:19

    

     Th19: F = {A} implies (A is open iff F is open)

    proof

      assume

       A1: F = {A};

      hereby

        assume A is open;

        then for A be Subset of T st A in F holds A is open by A1, TARSKI:def 1;

        hence F is open by TOPS_2:def 1;

      end;

      assume

       A2: F is open;

      A in F by A1, TARSKI:def 1;

      hence thesis by A2, TOPS_2:def 1;

    end;

    theorem :: TOPGEN_4:20

    

     Th20: F = {A} implies (A is closed iff F is closed)

    proof

      assume

       A1: F = {A};

      hereby

        assume A is closed;

        then for A be Subset of T st A in F holds A is closed by A1, TARSKI:def 1;

        hence F is closed by TOPS_2:def 2;

      end;

      assume

       A2: F is closed;

      A in F by A1, TARSKI:def 1;

      hence thesis by A2, TOPS_2:def 2;

    end;

    definition

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

      :: original: INTERSECTION

      redefine

      func INTERSECTION (F,G) -> Subset-Family of T ;

      coherence

      proof

        ( INTERSECTION (F,G)) c= ( bool T)

        proof

          let x be object;

          assume x in ( INTERSECTION (F,G));

          then

          consider X,Y be set such that

           A1: X in F and Y in G and

           A2: x = (X /\ Y) by SETFAM_1:def 5;

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

          then x is Subset of T by A1, A2, XBOOLE_1: 1;

          hence thesis;

        end;

        hence thesis;

      end;

      :: original: UNION

      redefine

      func UNION (F,G) -> Subset-Family of T ;

      coherence

      proof

        ( UNION (F,G)) c= ( bool T)

        proof

          let x be object;

          assume x in ( UNION (F,G));

          then

          consider X,Y be set such that

           A3: X in F & Y in G and

           A4: x = (X \/ Y) by SETFAM_1:def 4;

          (X \/ Y) c= T by A3, XBOOLE_1: 8;

          hence thesis by A4;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPGEN_4:21

    

     Th21: F is closed & G is closed implies ( INTERSECTION (F,G)) is closed

    proof

      assume

       A1: F is closed & G is closed;

      for A be Subset of T st A in ( INTERSECTION (F,G)) holds A is closed

      proof

        let A be Subset of T;

        assume A in ( INTERSECTION (F,G));

        then

        consider X,Y be set such that

         A2: X in F & Y in G and

         A3: A = (X /\ Y) by SETFAM_1:def 5;

        reconsider X, Y as Subset of T by A2;

        X is closed & Y is closed by A1, A2, TOPS_2:def 2;

        hence thesis by A3;

      end;

      hence thesis by TOPS_2:def 2;

    end;

    theorem :: TOPGEN_4:22

    

     Th22: F is closed & G is closed implies ( UNION (F,G)) is closed

    proof

      assume

       A1: F is closed & G is closed;

      for A be Subset of T st A in ( UNION (F,G)) holds A is closed

      proof

        let A be Subset of T;

        assume A in ( UNION (F,G));

        then

        consider X,Y be set such that

         A2: X in F & Y in G and

         A3: A = (X \/ Y) by SETFAM_1:def 4;

        reconsider X, Y as Subset of T by A2;

        X is closed & Y is closed by A1, A2, TOPS_2:def 2;

        hence thesis by A3;

      end;

      hence thesis by TOPS_2:def 2;

    end;

    theorem :: TOPGEN_4:23

    

     Th23: F is open & G is open implies ( INTERSECTION (F,G)) is open

    proof

      assume

       A1: F is open & G is open;

      for A be Subset of T st A in ( INTERSECTION (F,G)) holds A is open

      proof

        let A be Subset of T;

        assume A in ( INTERSECTION (F,G));

        then

        consider X,Y be set such that

         A2: X in F & Y in G and

         A3: A = (X /\ Y) by SETFAM_1:def 5;

        reconsider X, Y as Subset of T by A2;

        X is open & Y is open by A1, A2, TOPS_2:def 1;

        hence thesis by A3;

      end;

      hence thesis by TOPS_2:def 1;

    end;

    theorem :: TOPGEN_4:24

    

     Th24: F is open & G is open implies ( UNION (F,G)) is open

    proof

      assume

       A1: F is open & G is open;

      for A be Subset of T st A in ( UNION (F,G)) holds A is open

      proof

        let A be Subset of T;

        assume A in ( UNION (F,G));

        then

        consider X,Y be set such that

         A2: X in F & Y in G and

         A3: A = (X \/ Y) by SETFAM_1:def 4;

        reconsider X, Y as Subset of T by A2;

        X is open & Y is open by A1, A2, TOPS_2:def 1;

        hence thesis by A3;

      end;

      hence thesis by TOPS_2:def 1;

    end;

    theorem :: TOPGEN_4:25

    

     Th25: for T be set, F,G be Subset-Family of T holds ( card ( INTERSECTION (F,G))) c= ( card [:F, G:])

    proof

      deffunc F( set) = (($1 `1 ) /\ ($1 `2 ));

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

      set XX = [:F, G:];

      set IN = { F(X) where X be Element of [:( bool T), ( bool T):] : X in XX };

      set A = [:( bool T), ( bool T):];

      set AL = F, BL = G;

      set C = ( INTERSECTION (AL,BL));

      

       A1: IN c= C

      proof

        let a be object;

        assume a in IN;

        then

        consider X be Element of [:( bool T), ( bool T):] such that

         A2: a = F(X) and

         A3: X in XX;

        (X `1 ) in F & (X `2 ) in G by A3, MCART_1: 10;

        hence thesis by A2, SETFAM_1:def 5;

      end;

      

       A4: C c= IN

      proof

        let a be object;

        assume a in C;

        then

        consider X,Y be set such that

         A5: X in AL & Y in BL and

         A6: a = (X /\ Y) by SETFAM_1:def 5;

        reconsider X, Y as Subset of T by A5;

        set XY = [X, Y];

        

         A7: (XY `1 ) = X & (XY `2 ) = Y;

        XY in XX by A5, ZFMISC_1: 87;

        hence thesis by A6, A7;

      end;

      ( card { F(w) where w be Element of A : w in XX }) c= ( card XX) from TREES_2:sch 2;

      hence thesis by A1, A4, XBOOLE_0:def 10;

    end;

    theorem :: TOPGEN_4:26

    

     Th26: for T be set, F,G be Subset-Family of T holds ( card ( UNION (F,G))) c= ( card [:F, G:])

    proof

      deffunc F( set) = (($1 `1 ) \/ ($1 `2 ));

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

      set XX = [:F, G:];

      set IN = { F(X) where X be Element of [:( bool T), ( bool T):] : X in XX };

      set A = [:( bool T), ( bool T):];

      set AL = F, BL = G;

      set C = ( UNION (AL,BL));

      

       A1: IN = C

      proof

        thus IN c= C

        proof

          let a be object;

          assume a in IN;

          then

          consider X be Element of [:( bool T), ( bool T):] such that

           A2: a = F(X) and

           A3: X in XX;

          (X `1 ) in F & (X `2 ) in G by A3, MCART_1: 10;

          hence thesis by A2, SETFAM_1:def 4;

        end;

        let a be object;

        assume a in C;

        then

        consider X,Y be set such that

         A4: X in AL & Y in BL and

         A5: a = (X \/ Y) by SETFAM_1:def 4;

        reconsider X, Y as Subset of T by A4;

        set XY = [X, Y];

        

         A6: (XY `1 ) = X & (XY `2 ) = Y;

        XY in XX by A4, ZFMISC_1: 87;

        hence thesis by A5, A6;

      end;

      ( card { F(w) where w be Element of A : w in XX }) c= ( card XX) from TREES_2:sch 2;

      hence thesis by A1;

    end;

    theorem :: TOPGEN_4:27

    

     Th27: for F,G be set holds ( union ( UNION (F,G))) c= (( union F) \/ ( union G))

    proof

      let F,G be set;

      let x be object;

      assume x in ( union ( UNION (F,G)));

      then

      consider Y be set such that

       A1: x in Y and

       A2: Y in ( UNION (F,G)) by TARSKI:def 4;

      consider f,g be set such that

       A3: f in F and

       A4: g in G and

       A5: Y = (f \/ g) by A2, SETFAM_1:def 4;

      per cases by A1, A5, XBOOLE_0:def 3;

        suppose x in f;

        then x in ( union F) by A3, TARSKI:def 4;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose x in g;

        then x in ( union G) by A4, TARSKI:def 4;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: TOPGEN_4:28

    

     Th28: for F,G be set st F <> {} & G <> {} holds (( union F) \/ ( union G)) = ( union ( UNION (F,G)))

    proof

      let F,G be set;

      assume that

       A1: F <> {} and

       A2: G <> {} ;

      thus (( union F) \/ ( union G)) c= ( union ( UNION (F,G)))

      proof

        let x be object;

        assume

         A3: x in (( union F) \/ ( union G));

        per cases by A3, XBOOLE_0:def 3;

          suppose

           A4: x in ( union F);

          consider W be object such that

           A5: W in G by A2, XBOOLE_0:def 1;

          consider Y be set such that

           A6: x in Y and

           A7: Y in F by A4, TARSKI:def 4;

          reconsider Y, W as set by TARSKI: 1;

          set YW = (Y \/ W);

          Y c= YW & YW in ( UNION (F,G)) by A7, A5, SETFAM_1:def 4, XBOOLE_1: 7;

          hence thesis by A6, TARSKI:def 4;

        end;

          suppose

           A8: x in ( union G);

          consider W be object such that

           A9: W in F by A1, XBOOLE_0:def 1;

          consider Y be set such that

           A10: x in Y and

           A11: Y in G by A8, TARSKI:def 4;

          reconsider Y, W as set by TARSKI: 1;

          set YW = (W \/ Y);

          Y c= YW & YW in ( UNION (F,G)) by A11, A9, SETFAM_1:def 4, XBOOLE_1: 7;

          hence thesis by A10, TARSKI:def 4;

        end;

      end;

      thus thesis by Th27;

    end;

    theorem :: TOPGEN_4:29

    

     Th29: for F be set holds ( UNION ( {} ,F)) = {}

    proof

      let F be set;

      ( UNION ( {} ,F)) c= {}

      proof

        let x be object;

        assume x in ( UNION ( {} ,F));

        then ex x1,x2 be set st x1 in {} & x2 in F & x = (x1 \/ x2) by SETFAM_1:def 4;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_4:30

    for F,G be set holds ( UNION (F,G)) = {} implies F = {} or G = {}

    proof

      let F,G be set;

      assume

       A1: ( UNION (F,G)) = {} ;

      assume that

       A2: F <> {} and

       A3: G <> {} ;

      consider X be object such that

       A4: X in F by A2, XBOOLE_0:def 1;

      consider Y be object such that

       A5: Y in G by A3, XBOOLE_0:def 1;

      reconsider Y, X as set by TARSKI: 1;

      (X \/ Y) in ( UNION (F,G)) by A4, A5, SETFAM_1:def 4;

      hence thesis by A1;

    end;

    theorem :: TOPGEN_4:31

    for F,G be set st ( INTERSECTION (F,G)) = {} holds F = {} or G = {}

    proof

      let F,G be set;

      assume that

       A1: ( INTERSECTION (F,G)) = {} and

       A2: F <> {} and

       A3: G <> {} ;

      consider X be object such that

       A4: X in F by A2, XBOOLE_0:def 1;

      consider Y be object such that

       A5: Y in G by A3, XBOOLE_0:def 1;

      reconsider Y, X as set by TARSKI: 1;

      (X /\ Y) in ( INTERSECTION (F,G)) by A4, A5, SETFAM_1:def 5;

      hence thesis by A1;

    end;

    theorem :: TOPGEN_4:32

    

     Th32: for F,G be set holds ( meet ( UNION (F,G))) c= (( meet F) \/ ( meet G))

    proof

      let F,G be set;

      per cases ;

        suppose

         A1: F <> {} & G <> {} ;

        let x be object;

        assume

         A2: x in ( meet ( UNION (F,G)));

        assume

         A3: not x in (( meet F) \/ ( meet G));

        then not x in ( meet F) by XBOOLE_0:def 3;

        then

        consider Y be set such that

         A4: Y in F & not x in Y by A1, SETFAM_1:def 1;

         not x in ( meet G) by A3, XBOOLE_0:def 3;

        then

        consider Z be set such that

         A5: Z in G & not x in Z by A1, SETFAM_1:def 1;

        ( not x in (Y \/ Z)) & (Y \/ Z) in ( UNION (F,G)) by A4, A5, SETFAM_1:def 4, XBOOLE_0:def 3;

        hence thesis by A2, SETFAM_1:def 1;

      end;

        suppose F = {} or G = {} ;

        then ( UNION (F,G)) = {} by Th29;

        then ( meet ( UNION (F,G))) = {} by SETFAM_1:def 1;

        hence thesis;

      end;

    end;

    theorem :: TOPGEN_4:33

    for F,G be set st F <> {} & G <> {} holds ( meet ( UNION (F,G))) = (( meet F) \/ ( meet G)) by Th32, SETFAM_1: 29;

    theorem :: TOPGEN_4:34

    

     Th34: for F,G be set st F <> {} & G <> {} holds (( meet F) /\ ( meet G)) = ( meet ( INTERSECTION (F,G)))

    proof

      let F,G be set;

      assume that

       A1: F <> {} and

       A2: G <> {} ;

      consider y be object such that

       A3: y in F by A1, XBOOLE_0:def 1;

      reconsider y as set by TARSKI: 1;

      consider z be object such that

       A4: z in G by A2, XBOOLE_0:def 1;

      reconsider z as set by TARSKI: 1;

      

       A5: ( meet ( INTERSECTION (F,G))) c= (( meet F) /\ ( meet G))

      proof

        let x be object such that

         A6: x in ( meet ( INTERSECTION (F,G)));

        for Z be set st Z in G holds x in Z

        proof

          let Z be set;

          assume Z in G;

          then (y /\ Z) in ( INTERSECTION (F,G)) by A3, SETFAM_1:def 5;

          then x in (y /\ Z) by A6, SETFAM_1:def 1;

          hence thesis by XBOOLE_0:def 4;

        end;

        then

         A7: x in ( meet G) by A2, SETFAM_1:def 1;

        for Z be set st Z in F holds x in Z

        proof

          let Z be set;

          assume Z in F;

          then (Z /\ z) in ( INTERSECTION (F,G)) by A4, SETFAM_1:def 5;

          then x in (Z /\ z) by A6, SETFAM_1:def 1;

          hence thesis by XBOOLE_0:def 4;

        end;

        then x in ( meet F) by A1, SETFAM_1:def 1;

        hence thesis by A7, XBOOLE_0:def 4;

      end;

      

       A8: (y /\ z) in ( INTERSECTION (F,G)) by A3, A4, SETFAM_1:def 5;

      (( meet F) /\ ( meet G)) c= ( meet ( INTERSECTION (F,G)))

      proof

        let x be object;

        assume x in (( meet F) /\ ( meet G));

        then

         A9: x in ( meet F) & x in ( meet G) by XBOOLE_0:def 4;

        for Z be set st Z in ( INTERSECTION (F,G)) holds x in Z

        proof

          let Z be set;

          assume Z in ( INTERSECTION (F,G));

          then

          consider Z1,Z2 be set such that

           A10: Z1 in F & Z2 in G and

           A11: Z = (Z1 /\ Z2) by SETFAM_1:def 5;

          x in Z1 & x in Z2 by A9, A10, SETFAM_1:def 1;

          hence thesis by A11, XBOOLE_0:def 4;

        end;

        hence thesis by A8, SETFAM_1:def 1;

      end;

      hence thesis by A5;

    end;

    begin

    definition

      let T be TopSpace, A be Subset of T;

      :: TOPGEN_4:def6

      attr A is F_sigma means ex F be closed countable Subset-Family of T st A = ( union F);

    end

    definition

      let T be TopSpace, A be Subset of T;

      :: TOPGEN_4:def7

      attr A is G_delta means ex F be open countable Subset-Family of T st A = ( meet F);

    end

    registration

      let T;

      cluster empty -> F_sigma G_delta for Subset of T;

      coherence

      proof

        let S be Subset of T;

        assume S is empty;

        then

         A1: S = ( {} T);

        thus S is F_sigma

        proof

          reconsider E = {} as empty Subset-Family of T by Th18;

          ( {} T) = ( union E) by ZFMISC_1: 2;

          hence thesis by A1;

        end;

        reconsider F = {( {} T)} as Subset-Family of T;

        F is open & ( {} T) = ( meet F) by Th19, SETFAM_1: 10;

        hence thesis by A1;

      end;

    end

    theorem :: TOPGEN_4:35

    

     Th35: ( [#] T) is F_sigma

    proof

      reconsider F = {( [#] T)} as Subset-Family of T;

      F is closed & ( [#] T) = ( union F) by Th20, ZFMISC_1: 25;

      hence thesis;

    end;

    theorem :: TOPGEN_4:36

    

     Th36: ( [#] T) is G_delta

    proof

      reconsider F = {( [#] T)} as Subset-Family of T;

      F is open & ( [#] T) = ( meet F) by Th19, SETFAM_1: 10;

      hence thesis;

    end;

    registration

      let T;

      cluster ( [#] T) -> F_sigma G_delta;

      coherence by Th35, Th36;

    end

    theorem :: TOPGEN_4:37

    A is F_sigma implies (A ` ) is G_delta

    proof

      assume A is F_sigma;

      then

      consider F be closed countable Subset-Family of T such that

       A1: A = ( union F);

      per cases ;

        suppose

         A2: F <> {} ;

        set G = ( COMPLEMENT F);

        

         A3: G is open by TOPS_2: 9;

        (( union F) ` ) = ( meet ( COMPLEMENT F)) by A2, TOPS_2: 6;

        hence thesis by A1, A3;

      end;

        suppose F = {} ;

        then (A ` ) = ( [#] T) by A1, ZFMISC_1: 2;

        hence thesis;

      end;

    end;

    theorem :: TOPGEN_4:38

    A is G_delta implies (A ` ) is F_sigma

    proof

      assume A is G_delta;

      then

      consider F be open countable Subset-Family of T such that

       A1: A = ( meet F);

      per cases ;

        suppose

         A2: F <> {} ;

        set G = ( COMPLEMENT F);

        

         A3: G is closed by TOPS_2: 10;

        (( meet F) ` ) = ( union ( COMPLEMENT F)) by A2, TOPS_2: 7;

        hence thesis by A1, A3;

      end;

        suppose F = {} ;

        then (A ` ) = ( [#] T) by A1, SETFAM_1: 1;

        hence thesis;

      end;

    end;

    theorem :: TOPGEN_4:39

    A is F_sigma & B is F_sigma implies (A /\ B) is F_sigma

    proof

      assume that

       A1: A is F_sigma and

       A2: B is F_sigma;

      consider F be closed countable Subset-Family of T such that

       A3: A = ( union F) by A1;

      consider G be closed countable Subset-Family of T such that

       A4: B = ( union G) by A2;

      reconsider H = ( INTERSECTION (F,G)) as Subset-Family of T;

      

       A5: H is closed by Th21;

      ( card H) c= ( card [:F, G:]) & [:F, G:] is countable by Th25, CARD_4: 7;

      then

       A6: H is countable by WAYBEL12: 1;

      (A /\ B) = ( union H) by A3, A4, SETFAM_1: 28;

      hence thesis by A5, A6;

    end;

    theorem :: TOPGEN_4:40

    A is F_sigma & B is F_sigma implies (A \/ B) is F_sigma

    proof

      assume that

       A1: A is F_sigma and

       A2: B is F_sigma;

      consider F be closed countable Subset-Family of T such that

       A3: A = ( union F) by A1;

      consider G be closed countable Subset-Family of T such that

       A4: B = ( union G) by A2;

      reconsider H = ( UNION (F,G)) as Subset-Family of T;

      per cases ;

        suppose

         A5: A <> {} & B <> {} ;

        

         A6: H is closed by Th22;

        ( card H) c= ( card [:F, G:]) & [:F, G:] is countable by Th26, CARD_4: 7;

        then

         A7: H is countable by WAYBEL12: 1;

        (A \/ B) = ( union H) by A3, A4, A5, Th28, ZFMISC_1: 2;

        hence thesis by A6, A7;

      end;

        suppose A = {} ;

        hence thesis by A2;

      end;

        suppose B = {} ;

        hence thesis by A1;

      end;

    end;

    theorem :: TOPGEN_4:41

    A is G_delta & B is G_delta implies (A \/ B) is G_delta

    proof

      assume that

       A1: A is G_delta and

       A2: B is G_delta;

      consider F be open countable Subset-Family of T such that

       A3: A = ( meet F) by A1;

      consider G be open countable Subset-Family of T such that

       A4: B = ( meet G) by A2;

      reconsider H = ( UNION (F,G)) as Subset-Family of T;

      per cases ;

        suppose

         A5: F <> {} & G <> {} ;

        

         A6: ( meet ( UNION (F,G))) c= (( meet F) \/ ( meet G)) by Th32;

        (( meet F) \/ ( meet G)) c= ( meet ( UNION (F,G))) by A5, SETFAM_1: 29;

        then

         A7: (A \/ B) = ( meet H) by A3, A4, A6;

        ( card H) c= ( card [:F, G:]) & [:F, G:] is countable by Th26, CARD_4: 7;

        then

         A8: H is countable by WAYBEL12: 1;

        H is open by Th24;

        hence thesis by A7, A8;

      end;

        suppose F = {} or G = {} ;

        then A = {} or B = {} by A3, A4, SETFAM_1:def 1;

        hence thesis by A1, A2;

      end;

    end;

    theorem :: TOPGEN_4:42

    A is G_delta & B is G_delta implies (A /\ B) is G_delta

    proof

      assume that

       A1: A is G_delta and

       A2: B is G_delta;

      consider F be open countable Subset-Family of T such that

       A3: A = ( meet F) by A1;

      consider G be open countable Subset-Family of T such that

       A4: B = ( meet G) by A2;

      reconsider H = ( INTERSECTION (F,G)) as Subset-Family of T;

      per cases ;

        suppose

         A5: F <> {} & G <> {} ;

        

         A6: H is open by Th23;

        ( card H) c= ( card [:F, G:]) & [:F, G:] is countable by Th25, CARD_4: 7;

        then

         A7: H is countable by WAYBEL12: 1;

        (A /\ B) = ( meet H) by A3, A4, A5, Th34;

        hence thesis by A6, A7;

      end;

        suppose F = {} or G = {} ;

        then A = {} or B = {} by A3, A4, SETFAM_1:def 1;

        then (A /\ B) = ( {} T);

        hence thesis;

      end;

    end;

    theorem :: TOPGEN_4:43

    for A be Subset of T st A is closed holds A is F_sigma

    proof

      let A be Subset of T;

      assume A is closed;

      then

      reconsider F = {A} as closed countable Subset-Family of T by Th20;

      take F;

      thus thesis by ZFMISC_1: 25;

    end;

    theorem :: TOPGEN_4:44

    for A be Subset of T st A is open holds A is G_delta

    proof

      let A be Subset of T;

      assume A is open;

      then

      reconsider F = {A} as open countable Subset-Family of T by Th19;

      take F;

      thus thesis by SETFAM_1: 10;

    end;

    theorem :: TOPGEN_4:45

    for A be Subset of R^1 st A = RAT holds A is F_sigma

    proof

      defpred R[ object] means ex a be Element of RAT st a = $1;

      defpred P[ object] means ex a be Element of RAT st {a} = $1;

      let A be Subset of R^1 ;

      ex F be set st for x be set holds x in F iff x in ( bool RAT ) & P[x] from XFAMILY:sch 1;

      then

      consider F be set such that

       A1: for x be set holds x in F iff x in ( bool RAT ) & P[x];

      

       A2: ( bool RAT ) c= ( bool REAL ) by NUMBERS: 12, ZFMISC_1: 67;

      F c= ( bool the carrier of R^1 ) by A1, A2, TOPMETR: 17;

      then

      reconsider F as Subset-Family of R^1 ;

      assume

       A3: A = RAT ;

      ex F be Subset-Family of R^1 st F is closed countable & A = ( union F)

      proof

        take F;

        for B be Subset of R^1 st B in F holds B is closed

        proof

          let B be Subset of R^1 ;

          assume B in F;

          then ex a be Element of RAT st {a} = B by A1;

          hence thesis;

        end;

        hence F is closed by TOPS_2:def 2;

        

         A4: F = { {x} where x be Element of RAT : R[x] }

        proof

          thus F c= { {x} where x be Element of RAT : R[x] }

          proof

            let y be object;

            assume y in F;

            then P[y] by A1;

            hence thesis;

          end;

          let y be object;

          assume y in { {x} where x be Element of RAT : R[x] };

          then ex z be Element of RAT st y = {z} & R[z];

          hence thesis by A1;

        end;

        { {x} where x be Element of RAT : R[x] } is countable from FraenCoun11;

        hence F is countable by A4;

        thus A c= ( union F)

        proof

          let x be object;

          assume x in A;

          then

          reconsider x as Element of RAT by A3;

           {x} in F & x in {x} by A1, TARSKI:def 1;

          hence thesis by TARSKI:def 4;

        end;

        let x be object;

        assume x in ( union F);

        then

        consider Y be set such that

         A5: x in Y and

         A6: Y in F by TARSKI:def 4;

        ex a be Element of RAT st {a} = Y by A1, A6;

        hence thesis by A3, A5;

      end;

      hence thesis;

    end;

    begin

    definition

      let T be TopSpace;

      :: TOPGEN_4:def8

      attr T is T_1/2 means for A be Subset of T holds ( Der A) is closed;

    end

    theorem :: TOPGEN_4:46

    

     Th46: for T be TopSpace st T is T_1 holds T is T_1/2

    proof

      let T be TopSpace;

      assume

       A1: T is T_1;

      for A be Subset of T holds ( Der A) is closed

      proof

        let A be Subset of T;

        ( Der A) = ( Cl ( Der A)) by A1, TOPGEN_1: 33;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_4:47

    

     Th47: for T be non empty TopSpace st T is T_1/2 holds T is T_0

    proof

      let T be non empty TopSpace;

      assume

       A1: T is T_1/2;

      now

        let x,y be Point of T;

        assume

         A2: x <> y;

        assume that

         A3: x in ( Cl {y}) and

         A4: y in ( Cl {x});

         not for G be Subset of T st G is open holds y in G implies {x} meets G

        proof

          set X = (( Der {x}) ` );

           not x in ( Der {x})

          proof

            set U = the a_neighborhood of x;

            consider V be Subset of T such that

             A5: V is open and V c= U and

             A6: x in V by CONNSP_2: 6;

            assume x in ( Der {x});

            then

            consider z be Point of T such that

             A7: z in ( {x} /\ V) and

             A8: x <> z by A5, A6, TOPGEN_1: 17;

            z in {x} by A7, XBOOLE_0:def 4;

            hence thesis by A8, TARSKI:def 1;

          end;

          then

           A9: x in (( Der {x}) ` ) by SUBSET_1: 29;

          assume

           A10: for G be Subset of T st G is open holds y in G implies {x} meets G;

          for U be open Subset of T st y in U holds ex r be Point of T st r in ( {x} /\ U) & y <> r

          proof

            let U be open Subset of T;

            assume y in U;

            then {x} meets U by A10;

            then

             A11: x in U by ZFMISC_1: 50;

            x in {x} by TARSKI:def 1;

            then x in ( {x} /\ U) by A11, XBOOLE_0:def 4;

            hence thesis by A2;

          end;

          then y in ( Der {x}) by TOPGEN_1: 17;

          then

           A12: not y in X by XBOOLE_0:def 5;

          ( Der {x}) is closed by A1;

          then {y} meets X by A3, A9, PRE_TOPC: 24;

          hence thesis by A12, ZFMISC_1: 50;

        end;

        hence contradiction by A4, PRE_TOPC: 24;

      end;

      hence thesis by TSP_1:def 6;

    end;

    registration

      cluster T_1/2 -> T_0 for TopSpace;

      coherence

      proof

        let T be TopSpace;

        per cases ;

          suppose T is non empty;

          then

          reconsider T9 = T as non empty TopSpace;

          assume T is T_1/2;

          then T9 is T_1/2;

          hence thesis by Th47;

        end;

          suppose T is empty;

          then

          reconsider T9 = T as empty TopSpace;

          T9 is T_0;

          hence thesis;

        end;

      end;

      cluster T_1 -> T_1/2 for TopSpace;

      coherence by Th46;

    end

    begin

    definition

      let T, A;

      let x be Point of T;

      :: TOPGEN_4:def9

      pred x is_a_condensation_point_of A means for N be a_neighborhood of x holds not (N /\ A) is countable;

    end

    reserve x for Point of T;

    theorem :: TOPGEN_4:48

    

     Th48: x is_a_condensation_point_of A & A c= B implies x is_a_condensation_point_of B

    proof

      assume that

       A1: x is_a_condensation_point_of A and

       A2: A c= B;

      for N be a_neighborhood of x holds not (N /\ B) is countable

      proof

        let N be a_neighborhood of x;

        (N /\ A) c= (N /\ B) by A2, XBOOLE_1: 26;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    definition

      let T, A;

      :: TOPGEN_4:def10

      func A ^0 -> Subset of T means

      : Def10: for x be Point of T holds x in it iff x is_a_condensation_point_of A;

      existence

      proof

        defpred P[ Point of T] means $1 is_a_condensation_point_of A;

        ex X be Subset of T st for x be Element of T holds x in X iff P[x] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ Point of T] means $1 is_a_condensation_point_of A;

        let A1,A2 be Subset of T such that

         A1: for x be Element of T holds x in A1 iff P[x] and

         A2: for x be Element of T holds x in A2 iff P[x];

        thus A1 = A2 from SUBSET_1:sch 2( A1, A2);

      end;

    end

    theorem :: TOPGEN_4:49

    

     Th49: for p be Point of T st p is_a_condensation_point_of A holds p is_an_accumulation_point_of A

    proof

      let p be Point of T;

      assume

       A1: p is_a_condensation_point_of A;

      for U be open Subset of T st p in U holds ex q be Point of T st q <> p & q in A & q in U

      proof

        let U be open Subset of T;

        assume p in U;

        then

        reconsider N = U as a_neighborhood of p by CONNSP_2: 3;

        reconsider NU = (N /\ A) as non empty non countable set by A1;

        consider q be Element of NU such that

         A2: p <> q by SUBSET_1: 50;

        q in NU;

        then

        reconsider q as Point of T;

        q in A & q in U by XBOOLE_0:def 4;

        hence thesis by A2;

      end;

      hence thesis by TOPGEN_1: 21;

    end;

    theorem :: TOPGEN_4:50

    (A ^0 ) c= ( Der A)

    proof

      let x be object;

      assume

       A1: x in (A ^0 );

      then

      reconsider p = x as Point of T;

      p is_a_condensation_point_of A by A1, Def10;

      then p is_an_accumulation_point_of A by Th49;

      hence thesis by TOPGEN_1: 16;

    end;

    theorem :: TOPGEN_4:51

    (A ^0 ) = ( Cl (A ^0 ))

    proof

      thus (A ^0 ) c= ( Cl (A ^0 )) by PRE_TOPC: 18;

      let x be object;

      assume

       A1: x in ( Cl (A ^0 ));

      then

      reconsider p = x as Point of T;

      for N be a_neighborhood of p holds not (N /\ A) is countable

      proof

        let N be a_neighborhood of p;

        consider N1 be Subset of T such that

         A2: N1 is open and

         A3: N1 c= N and

         A4: p in N1 by CONNSP_2: 6;

        (A ^0 ) meets N1 by A1, A2, A4, PRE_TOPC: 24;

        then

        consider y be object such that

         A5: y in (A ^0 ) and

         A6: y in N1 by XBOOLE_0: 3;

        reconsider y9 = y as Point of T by A5;

        reconsider N1 as a_neighborhood of y9 by A2, A6, CONNSP_2: 6;

        

         A7: (N1 /\ A) c= (N /\ A) by A3, XBOOLE_1: 26;

        y9 is_a_condensation_point_of A by A5, Def10;

        hence thesis by A7;

      end;

      then p is_a_condensation_point_of A;

      hence thesis by Def10;

    end;

    theorem :: TOPGEN_4:52

    

     Th52: A c= B implies (A ^0 ) c= (B ^0 )

    proof

      assume

       A1: A c= B;

      let x be object;

      assume

       A2: x in (A ^0 );

      then

      reconsider x9 = x as Point of T;

      x9 is_a_condensation_point_of A by A2, Def10;

      then x9 is_a_condensation_point_of B by A1, Th48;

      hence thesis by Def10;

    end;

    theorem :: TOPGEN_4:53

    

     Th53: x is_a_condensation_point_of (A \/ B) implies x is_a_condensation_point_of A or x is_a_condensation_point_of B

    proof

      assume

       A1: x is_a_condensation_point_of (A \/ B);

      assume that

       A2: not x is_a_condensation_point_of A and

       A3: not x is_a_condensation_point_of B;

      consider N1 be a_neighborhood of x such that

       A4: (N1 /\ A) is countable by A2;

      consider N2 be a_neighborhood of x such that

       A5: (N2 /\ B) is countable by A3;

      reconsider N3 = (N1 /\ N2) as a_neighborhood of x by CONNSP_2: 2;

      (N3 /\ A) c= (N1 /\ A) & (N3 /\ B) c= (N2 /\ B) by XBOOLE_1: 17, XBOOLE_1: 26;

      then ((N3 /\ A) \/ (N3 /\ B)) is countable by A4, A5, CARD_2: 85;

      then (N3 /\ (A \/ B)) is countable by XBOOLE_1: 23;

      hence thesis by A1;

    end;

    theorem :: TOPGEN_4:54

    ((A \/ B) ^0 ) = ((A ^0 ) \/ (B ^0 ))

    proof

      thus ((A \/ B) ^0 ) c= ((A ^0 ) \/ (B ^0 ))

      proof

        let x be object;

        assume

         A1: x in ((A \/ B) ^0 );

        then

        reconsider x9 = x as Point of T;

        x9 is_a_condensation_point_of (A \/ B) by A1, Def10;

        then x9 is_a_condensation_point_of A or x9 is_a_condensation_point_of B by Th53;

        then x9 in (A ^0 ) or x9 in (B ^0 ) by Def10;

        hence thesis by XBOOLE_0:def 3;

      end;

      (A ^0 ) c= ((A \/ B) ^0 ) & (B ^0 ) c= ((A \/ B) ^0 ) by Th52, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: TOPGEN_4:55

    

     Th55: A is countable implies not ex x be Point of T st x is_a_condensation_point_of A

    proof

      assume

       A1: A is countable;

      given x be Point of T such that

       A2: x is_a_condensation_point_of A;

      set N = the a_neighborhood of x;

       not (N /\ A) is countable by A2;

      hence thesis by A1, CARD_3: 94;

    end;

    theorem :: TOPGEN_4:56

    

     Th56: A is countable implies (A ^0 ) = {}

    proof

      assume

       A1: A is countable;

      assume (A ^0 ) <> {} ;

      then

      consider x be object such that

       A2: x in (A ^0 ) by XBOOLE_0:def 1;

      reconsider x9 = x as Point of T by A2;

      x9 is_a_condensation_point_of A by A2, Def10;

      hence thesis by A1, Th55;

    end;

    registration

      let T;

      let A be countable Subset of T;

      cluster (A ^0 ) -> empty;

      coherence by Th56;

    end

    theorem :: TOPGEN_4:57

    T is second-countable implies ex B be Basis of T st B is countable

    proof

      set B = the Basis of T;

      consider B1 be Basis of T such that B1 c= B and

       A1: ( card B1) = ( weight T) by TOPGEN_2: 18;

      assume T is second-countable;

      then ( card B1) c= omega by A1, WAYBEL23:def 6;

      then ( card ( card B1)) c= ( card omega );

      then B1 is countable;

      hence thesis;

    end;

    registration

      cluster second-countable non empty for TopSpace;

      existence

      proof

        set T = the finite non empty TopSpace;

        take T;

        thus thesis;

      end;

    end

    begin

    registration

      let T;

      cluster ( TotFam T) -> non empty all-open-containing compl-closed closed_for_countable_unions;

      coherence ;

    end

    theorem :: TOPGEN_4:58

    for T be set, A be SetSequence of T holds ( rng A) is countable non empty Subset-Family of T

    proof

      let T be set, A be SetSequence of T;

      (A . 1) in ( rng A) by FUNCT_2: 4;

      then

      reconsider AA = ( rng A) as non empty Subset-Family of T;

      ( card ( rng A)) c= ( card ( dom A)) & ( dom A) is countable by CARD_2: 61, FUNCT_2:def 1;

      then AA is countable by WAYBEL12: 1;

      hence thesis;

    end;

    theorem :: TOPGEN_4:59

    

     Th59: for F,G be Subset-Family of T st F is all-open-containing & F c= G holds G is all-open-containing;

    theorem :: TOPGEN_4:60

    for F,G be Subset-Family of T st F is all-closed-containing & F c= G holds G is all-closed-containing;

    definition

      let T be 1-sorted;

      mode SigmaField of T is SigmaField of the carrier of T;

    end

    registration

      let T be non empty TopSpace;

      cluster compl-closed closed_for_countable_unions closed_for_countable_meets all-closed-containing all-open-containing for Subset-Family of T;

      existence

      proof

        take ( TotFam T);

        thus thesis;

      end;

    end

    theorem :: TOPGEN_4:61

    

     Th61: ( sigma ( TotFam T)) is all-open-containing compl-closed closed_for_countable_unions

    proof

      set E = ( sigma ( TotFam T));

      ( TotFam T) c= ( sigma ( TotFam T)) by PROB_1:def 9;

      hence E is all-open-containing;

      thus E is compl-closed;

      thus thesis;

    end;

    registration

      let T;

      cluster ( sigma ( TotFam T)) -> all-open-containing compl-closed closed_for_countable_unions;

      coherence by Th61;

    end

    registration

      let T be non empty 1-sorted;

      cluster sigma-additive compl-closed closed_for_countable_unions non empty for Subset-Family of T;

      existence

      proof

        take ( sigma ( TotFam T));

        thus thesis;

      end;

    end

    registration

      let T be non empty TopSpace;

      cluster -> closed_for_countable_unions for SigmaField of T;

      coherence ;

    end

    theorem :: TOPGEN_4:62

    for T be non empty TopSpace, F be Subset-Family of T st F is compl-closed closed_for_countable_unions holds F is SigmaField of T by Th13;

    registration

      let T be non empty TopSpace;

      cluster all-open-containing for SigmaField of T;

      existence

      proof

        take ( sigma ( TotFam T));

        thus thesis;

      end;

    end

    registration

      let T be non empty TopSpace;

      cluster ( Topology_of T) -> open all-open-containing;

      coherence by PRE_TOPC:def 2;

    end

    theorem :: TOPGEN_4:63

    

     Th63: for X be Subset-Family of T holds ex Y be all-open-containing compl-closed closed_for_countable_unions Subset-Family of T st X c= Y & for Z be all-open-containing compl-closed closed_for_countable_unions Subset-Family of T st X c= Z holds Y c= Z

    proof

      let X be Subset-Family of T;

      set V = { S where S be Subset-Family of T : X c= S & S is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T };

      set Y = ( meet V);

       A1:

      now

        let Z be set;

        assume Z in V;

        then ex S be Subset-Family of T st Z = S & X c= S & S is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T;

        hence X c= Z;

      end;

      

       A2: ( bool the carrier of T) in V

      proof

        set X1 = ( TotFam T);

        X1 in V;

        hence thesis;

      end;

      

       A3: for E be Subset of T st E in Y holds (E ` ) in Y

      proof

        let E be Subset of T such that

         A4: E in Y;

        now

          let Z be set;

          assume Z in V;

          then E in Z & ex S be Subset-Family of T st Z = S & X c= S & S is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T by A4, SETFAM_1:def 1;

          hence (E ` ) in Z by PROB_1:def 1;

        end;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      

       A5: for BSeq be SetSequence of the carrier of T st ( rng BSeq) c= Y holds ( Intersection BSeq) in Y

      proof

        let BSeq be SetSequence of the carrier of T such that

         A6: ( rng BSeq) c= Y;

        now

          let Z be set;

          assume

           A7: Z in V;

          then

          consider S be Subset-Family of T such that

           A8: Z = S and X c= S and

           A9: S is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T;

          now

            let n be Nat;

            (BSeq . n) in ( rng BSeq) by NAT_1: 51;

            hence (BSeq . n) in Z by A6, A7, SETFAM_1:def 1;

          end;

          then

           A10: ( rng BSeq) c= Z by NAT_1: 52;

          S is SigmaField of T by A9, Th13;

          hence ( Intersection BSeq) in Z by A8, A10, PROB_1:def 6;

        end;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      now

        let Z be set;

        assume Z in V;

        then ex S be Subset-Family of T st Z = S & X c= S & S is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T;

        then Z is Field_Subset of the carrier of T by Th13;

        hence {} in Z by PROB_1: 4;

      end;

      then {} in Y by A2, SETFAM_1:def 1;

      then

      reconsider Y as SigmaField of T by A2, A5, A3, PROB_1: 15, SETFAM_1: 3;

      for A be Subset of T st A is open holds A in Y

      proof

        let A be Subset of T;

        assume

         A11: A is open;

        for Y be set holds Y in V implies A in Y

        proof

          let Y be set;

          assume Y in V;

          then ex S be Subset-Family of the carrier of T st Y = S & X c= S & S is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T;

          hence thesis by A11, Def2;

        end;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      then

      reconsider Y as all-open-containing compl-closed closed_for_countable_unions Subset-Family of T by Def2;

      take Y;

      for Z be set st X c= Z & Z is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T holds Y c= Z

      proof

        let Z be set;

        assume that

         A12: X c= Z and

         A13: Z is all-open-containing compl-closed closed_for_countable_unions Subset-Family of T;

        reconsider Z as Subset-Family of T by A13;

        Z in V by A12, A13;

        hence thesis by SETFAM_1: 3;

      end;

      hence thesis by A2, A1, SETFAM_1: 5;

    end;

    definition

      let T;

      :: TOPGEN_4:def11

      func BorelSets T -> all-open-containing compl-closed closed_for_countable_unions Subset-Family of T means

      : Def11: for G be all-open-containing compl-closed closed_for_countable_unions Subset-Family of T holds it c= G;

      existence

      proof

        reconsider E = {} as Subset-Family of T by Th18;

        consider Y be all-open-containing compl-closed closed_for_countable_unions Subset-Family of T such that E c= Y and

         A1: for Z be all-open-containing compl-closed closed_for_countable_unions Subset-Family of T st E c= Z holds Y c= Z by Th63;

        take Y;

        let G be all-open-containing compl-closed closed_for_countable_unions Subset-Family of T;

        thus thesis by A1, XBOOLE_1: 2;

      end;

      uniqueness ;

    end

    theorem :: TOPGEN_4:64

    

     Th64: for F be closed Subset-Family of T holds F c= ( BorelSets T)

    proof

      let F be closed Subset-Family of T;

      F c= ( BorelSets T)

      proof

        let x be object;

        assume

         A1: x in F;

        then

        reconsider xx = x as Subset of T;

        xx is closed by A1, TOPS_2:def 2;

        hence thesis by Def3;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_4:65

    

     Th65: for F be open Subset-Family of T holds F c= ( BorelSets T)

    proof

      let F be open Subset-Family of T;

      F c= ( BorelSets T)

      proof

        let x be object;

        assume

         A1: x in F;

        then

        reconsider xx = x as Subset of T;

        xx is open by A1, TOPS_2:def 1;

        hence thesis by Def2;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_4:66

    ( BorelSets T) = ( sigma ( Topology_of T))

    proof

      reconsider BT = ( BorelSets T) as SigmaField of T by Th13;

      set X = ( Topology_of T);

      

       A1: for Z be set st X c= Z & Z is SigmaField of T holds BT c= Z

      proof

        let Z be set;

        assume that

         A2: X c= Z and

         A3: Z is SigmaField of T;

        reconsider Z9 = Z as SigmaField of T by A3;

        Z9 is all-open-containing by A2, Th59;

        hence thesis by Def11;

      end;

      X c= BT by Th65;

      hence thesis by A1, PROB_1:def 9;

    end;

    definition

      let T, A;

      :: TOPGEN_4:def12

      attr A is Borel means A in ( BorelSets T);

    end

    registration

      let T;

      cluster F_sigma -> Borel for Subset of T;

      coherence by Th64, Def4;

    end

    registration

      let T;

      cluster G_delta -> Borel for Subset of T;

      coherence by Th65, Def5;

    end