topgen_1.miz

    begin

    theorem :: TOPGEN_1:1



     Th1: for T be 1-sorted, A,B be Subset of T holds A meets (B ` ) iff (A \ B) <> {} by SUBSET_1: 13;

    theorem :: TOPGEN_1:2

    for T be 1-sorted holds T is countable iff ( card ( [#] T)) c= omega by CARD_3:def 14, ORDERS_4:def 2;

    registration

      let T be finite 1-sorted;

      cluster ( [#] T) -> finite;

      coherence ;

    end

    registration

      cluster finite -> countable for 1-sorted;

      coherence

      proof

        let T be 1-sorted;

        assume T is finite;

        then the carrier of T is countable by CARD_4: 1;

        hence thesis by ORDERS_4:def 2;

      end;

    end

    registration

      cluster countable non empty for 1-sorted;

      existence

      proof

        set T = the finite non empty 1-sorted;

        take T;

        thus thesis;

      end;

      cluster countable non empty for TopSpace;

      existence

      proof

        set T = the finite non empty TopSpace;

        take T;

        thus thesis;

      end;

    end

    registration

      let T be countable 1-sorted;

      cluster ( [#] T) -> countable;

      coherence by ORDERS_4:def 2;

    end

    registration

      cluster T_1 non empty for TopSpace;

      existence

      proof

        set T = the discrete non empty TopSpace;

        take T;

        thus thesis;

      end;

    end

    begin

    theorem :: TOPGEN_1:3



     Th3: for T be TopSpace, A be Subset of T holds ( Int A) = (( Cl (A ` )) ` )

    proof

      let T be TopSpace, A be Subset of T;

      ( Int A) = (( Cl (((A ` ) ` ) ` )) ` ) by TDLAT_3: 3

      .= (( Cl (A ` )) ` );

      hence thesis;

    end;

    definition

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

      :: TOPGEN_1:def1

      func Fr F -> Subset-Family of T means

      : Def1: for A be Subset of T holds A in it iff ex B be Subset of T st A = ( Fr B) & B in F;

      existence

      proof

        defpred P[ set] means ex W be Subset of T st $1 = ( Fr W) & W in F;

        thus ex S be Subset-Family of T st for Z be Subset of T holds Z in S iff P[Z] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        defpred P[ object] means ex W be Subset of T st $1 = ( Fr W) & W in F;

        let H,G be Subset-Family of T;

        assume that

         A1: for Z be Subset of T holds Z in H iff P[Z] and

         A2: for X be Subset of T holds X in G iff P[X];

        now

          let X be object;

          assume

           A3: X in G;

          then

          reconsider X9 = X as Subset of T;

           P[X9] by A2, A3;

          hence X in H by A1;

        end;

        then

         A4: G c= H;

        now

          let Z be object;

          assume Z in H;

          then P[Z] by A1;

          hence Z in G by A2;

        end;

        then H c= G;

        hence thesis by A4;

      end;

    end

    theorem :: TOPGEN_1:4

    for T be TopSpace, F be Subset-Family of T st F = {} holds ( Fr F) = {}

    proof

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

      assume

       A1: F = {} ;

      assume ( Fr F) <> {} ;

      then

      consider x be object such that

       A2: x in ( Fr F) by XBOOLE_0:def 1;

      ex B be Subset of T st x = ( Fr B) & B in F by A2, Def1;

      hence thesis by A1;

    end;

    theorem :: TOPGEN_1:5

    for T be TopSpace, F be Subset-Family of T, A be Subset of T st F = {A} holds ( Fr F) = {( Fr A)}

    proof

      let T be TopSpace, F be Subset-Family of T, A be Subset of T;

      assume

       A1: F = {A};

      thus ( Fr F) c= {( Fr A)}

      proof

        let x be object;

        assume

         A2: x in ( Fr F);

        then

        reconsider B = x as Subset of T;

        consider C be Subset of T such that

         A3: B = ( Fr C) and

         A4: C in F by A2, Def1;

        C = A by A1, A4, TARSKI:def 1;

        hence thesis by A3, TARSKI:def 1;

      end;

      let x be object;

      assume x in {( Fr A)};

      then

       A5: x = ( Fr A) by TARSKI:def 1;

      A in F by A1, TARSKI:def 1;

      hence thesis by A5, Def1;

    end;

    theorem :: TOPGEN_1:6



     Th6: for T be TopSpace, F,G be Subset-Family of T st F c= G holds ( Fr F) c= ( Fr G)

    proof

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

      assume

       A1: F c= G;

      ( Fr F) c= ( Fr G)

      proof

        let x be object;

        assume

         A2: x in ( Fr F);

        then

        reconsider A = x as Subset of T;

        ex B be Subset of T st A = ( Fr B) & B in F by A2, Def1;

        hence thesis by A1, Def1;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_1:7

    for T be TopSpace, F,G be Subset-Family of T holds ( Fr (F \/ G)) = (( Fr F) \/ ( Fr G))

    proof

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

      thus ( Fr (F \/ G)) c= (( Fr F) \/ ( Fr G))

      proof

        let x be object;

        assume

         A1: x in ( Fr (F \/ G));

        then

        reconsider A = x as Subset of T;

        consider B be Subset of T such that

         A2: A = ( Fr B) and

         A3: B in (F \/ G) by A1, Def1;

        per cases by A3, XBOOLE_0:def 3;

          suppose B in F;

          then A in ( Fr F) by A2, Def1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose B in G;

          then A in ( Fr G) by A2, Def1;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      ( Fr F) c= ( Fr (F \/ G)) & ( Fr G) c= ( Fr (F \/ G)) by Th6, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: TOPGEN_1:8



     Th8: for T be TopStruct, A be Subset of T holds ( Fr A) = (( Cl A) \ ( Int A))

    proof

      let T be TopStruct, A be Subset of T;

      ( Fr A) = (( Cl A) /\ ((( Cl (A ` )) ` ) ` )) by TOPS_1:def 2

      .= (( Cl A) \ (( Cl (A ` )) ` )) by SUBSET_1: 13

      .= (( Cl A) \ ( Int A)) by TOPS_1:def 1;

      hence thesis;

    end;

    theorem :: TOPGEN_1:9



     Th9: for T be non empty TopSpace, A be Subset of T, p be Point of T holds p in ( Fr A) iff for U be Subset of T st U is open & p in U holds A meets U & (U \ A) <> {}

    proof

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

      hereby

        assume

         A1: p in ( Fr A);

        let U be Subset of T;

        assume

         A2: U is open & p in U;

        then U meets (A ` ) by A1, TOPS_1: 28;

        hence A meets U & (U \ A) <> {} by A1, A2, Th1, TOPS_1: 28;

      end;

      assume

       A3: for U be Subset of T st U is open & p in U holds A meets U & (U \ A) <> {} ;

      for U be Subset of T st U is open & p in U holds A meets U & U meets (A ` )

      proof

        let U be Subset of T;

        assume

         A4: U is open & p in U;

        then (U \ A) <> {} by A3;

        hence thesis by A3, A4, Th1;

      end;

      hence thesis by TOPS_1: 28;

    end;

    theorem :: TOPGEN_1:10

    for T be non empty TopSpace, A be Subset of T, p be Point of T holds p in ( Fr A) iff for B be Basis of p, U be Subset of T st U in B holds A meets U & (U \ A) <> {}

    proof

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

      hereby

        assume

         A1: p in ( Fr A);

        let B be Basis of p, U be Subset of T;

        assume U in B;

        then U is open & p in U by YELLOW_8: 12;

        hence A meets U & (U \ A) <> {} by A1, Th9;

      end;

      assume

       A2: for B be Basis of p, U be Subset of T st U in B holds A meets U & (U \ A) <> {} ;

      for U be Subset of T st U is open & p in U holds A meets U & U meets (A ` )

      proof

        set B = the Basis of p;

        let U be Subset of T;

        assume U is open & p in U;

        then

        consider V be Subset of T such that

         A3: V in B and

         A4: V c= U by YELLOW_8:def 1;

        (V \ A) <> {} by A2, A3;

        then

         A5: (U \ A) <> {} by A4, XBOOLE_1: 3, XBOOLE_1: 33;

        A meets V by A2, A3;

        hence thesis by A4, A5, Th1, XBOOLE_1: 63;

      end;

      hence thesis by TOPS_1: 28;

    end;

    theorem :: TOPGEN_1:11

    for T be non empty TopSpace, A be Subset of T, p be Point of T holds p in ( Fr A) iff ex B be Basis of p st for U be Subset of T st U in B holds A meets U & (U \ A) <> {}

    proof

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

      hereby

        set B = the Basis of p;

        assume

         A1: p in ( Fr A);

        take B;

        let U be Subset of T;

        assume U in B;

        then U is open & p in U by YELLOW_8: 12;

        hence A meets U & (U \ A) <> {} by A1, Th9;

      end;

      given B be Basis of p such that

       A2: for U be Subset of T st U in B holds A meets U & (U \ A) <> {} ;

      for U be Subset of T st U is open & p in U holds A meets U & U meets (A ` )

      proof

        let U be Subset of T;

        assume U is open & p in U;

        then

        consider V be Subset of T such that

         A3: V in B and

         A4: V c= U by YELLOW_8:def 1;

        (V \ A) <> {} by A2, A3;

        then

         A5: (U \ A) <> {} by A4, XBOOLE_1: 3, XBOOLE_1: 33;

        A meets V by A2, A3;

        hence thesis by A4, A5, Th1, XBOOLE_1: 63;

      end;

      hence thesis by TOPS_1: 28;

    end;

    theorem :: TOPGEN_1:12

    for T be TopSpace, A,B be Subset of T holds ( Fr (A /\ B)) c= ((( Cl A) /\ ( Fr B)) \/ (( Fr A) /\ ( Cl B)))

    proof

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



       A1: ((( Cl A) /\ ( Cl B)) /\ (( Cl (A ` )) \/ ( Cl (B ` )))) = (((( Cl A) /\ ( Cl B)) /\ ( Cl (A ` ))) \/ ((( Cl A) /\ ( Cl B)) /\ ( Cl (B ` )))) by XBOOLE_1: 23

      .= (((( Cl A) /\ ( Cl (A ` ))) /\ ( Cl B)) \/ ((( Cl A) /\ ( Cl B)) /\ ( Cl (B ` )))) by XBOOLE_1: 16

      .= ((( Fr A) /\ ( Cl B)) \/ ((( Cl A) /\ ( Cl B)) /\ ( Cl (B ` )))) by TOPS_1:def 2

      .= ((( Fr A) /\ ( Cl B)) \/ (( Cl A) /\ (( Cl B) /\ ( Cl (B ` ))))) by XBOOLE_1: 16

      .= ((( Fr A) /\ ( Cl B)) \/ (( Cl A) /\ ( Fr B))) by TOPS_1:def 2;

      ( Fr (A /\ B)) = (( Cl (A /\ B)) /\ ( Cl ((A /\ B) ` ))) by TOPS_1:def 2

      .= (( Cl (A /\ B)) /\ ( Cl ((A ` ) \/ (B ` )))) by XBOOLE_1: 54

      .= (( Cl (A /\ B)) /\ (( Cl (A ` )) \/ ( Cl (B ` )))) by PRE_TOPC: 20;

      hence thesis by A1, PRE_TOPC: 21, XBOOLE_1: 26;

    end;

    theorem :: TOPGEN_1:13

    for T be TopSpace, A be Subset of T holds the carrier of T = ((( Int A) \/ ( Fr A)) \/ ( Int (A ` )))

    proof

      let T be TopSpace, A be Subset of T;

      ((( Int A) \/ ( Fr A)) \/ ( Int (A ` ))) = ((( Int A) \/ ( Int (A ` ))) \/ ( Fr A)) by XBOOLE_1: 4

      .= ((( Int A) \/ ( Int (A ` ))) \/ (( Cl A) /\ ( Cl (A ` )))) by TOPS_1:def 2

      .= (((( Int A) \/ ( Int (A ` ))) \/ ( Cl A)) /\ ((( Int A) \/ ( Int (A ` ))) \/ ( Cl (A ` )))) by XBOOLE_1: 24

      .= (((( Int A) \/ (( Cl A) ` )) \/ ( Cl A)) /\ ((( Int A) \/ ( Int (A ` ))) \/ ( Cl (A ` )))) by TDLAT_3: 3

      .= ((( Int A) \/ ((( Cl A) ` ) \/ ( Cl A))) /\ ((( Int A) \/ ( Int (A ` ))) \/ ( Cl (A ` )))) by XBOOLE_1: 4

      .= ((( Int A) \/ ( [#] T)) /\ ((( Int A) \/ ( Int (A ` ))) \/ ( Cl (A ` )))) by PRE_TOPC: 2

      .= ((( Int A) \/ ( [#] T)) /\ ((( Int A) \/ ( Int (A ` ))) \/ (( Int A) ` ))) by TDLAT_3: 2

      .= ((( Int A) \/ ( [#] T)) /\ ((( Int A) \/ (( Int A) ` )) \/ ( Int (A ` )))) by XBOOLE_1: 4

      .= ((( Int A) \/ ( [#] T)) /\ (( [#] T) \/ ( Int (A ` )))) by PRE_TOPC: 2

      .= (( [#] T) /\ (( [#] T) \/ ( Int (A ` )))) by XBOOLE_1: 12

      .= (( [#] T) /\ ( [#] T)) by XBOOLE_1: 12

      .= ( [#] T);

      hence thesis;

    end;

    theorem :: TOPGEN_1:14



     Th14: for T be TopSpace, A be Subset of T holds A is open closed iff ( Fr A) = {}

    proof

      let T be TopSpace, A be Subset of T;

      hereby

        assume

         A1: A is open closed;

        then

         A2: ( Int A) = A by TOPS_1: 23;

        ( Fr A) = (A \ ( Int A)) by A1, TOPS_1: 43

        .= {} by A2, XBOOLE_1: 37;

        hence ( Fr A) = {} ;

      end;

      assume

       A3: ( Fr A) = {} ;

      ( Fr A) = (( Cl A) \ ( Int A)) by Th8;

      then

       A4: ( Cl A) c= ( Int A) by A3, XBOOLE_1: 37;



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

      then A c= ( Cl A) & ( Cl A) c= A by A4, PRE_TOPC: 18;

      then ( Cl A) = A;

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

    end;

    begin

    definition

      let T be TopStruct, A be Subset of T, x be object;

      :: TOPGEN_1:def2

      pred x is_an_accumulation_point_of A means x in ( Cl (A \ {x}));

    end

    theorem :: TOPGEN_1:15

    for T be TopSpace, A be Subset of T, x be object st x is_an_accumulation_point_of A holds x is Point of T;

    definition

      let T be TopStruct, A be Subset of T;

      :: TOPGEN_1:def3

      func Der A -> Subset of T means

      : Def3: for x be set st x in the carrier of T holds x in it iff x is_an_accumulation_point_of A;

      existence

      proof

        defpred P[ set] means $1 is_an_accumulation_point_of A;

        consider D be Subset of T such that

         A1: for x be set holds x in D iff x in the carrier of T & P[x] from SUBSET_1:sch 1;

        take D;

        thus thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 is_an_accumulation_point_of A;

        let A1,A2 be Subset of T;

        assume that

         A2: for x be set st x in the carrier of T holds x in A1 iff P[x] and

         A3: for x be set st x in the carrier of T holds x in A2 iff P[x];



         A4: A2 c= A1

        proof

          let x be object;

          assume

           A5: x in A2;

          then P[x] by A3;

          hence thesis by A2, A5;

        end;

        A1 c= A2

        proof

          let x be object;

          assume

           A6: x in A1;

          then P[x] by A2;

          hence thesis by A3, A6;

        end;

        hence thesis by A4;

      end;

    end

    theorem :: TOPGEN_1:16



     Th16: for T be non empty TopSpace, A be Subset of T, x be object holds x in ( Der A) iff x is_an_accumulation_point_of A by Def3;

    theorem :: TOPGEN_1:17



     Th17: for T be non empty TopSpace, A be Subset of T, x be Point of T holds x in ( Der A) iff for U be open Subset of T st x in U holds ex y be Point of T st y in (A /\ U) & x <> y

    proof

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

      hereby

        assume x in ( Der A);

        then x is_an_accumulation_point_of A by Th16;

        then

         A1: x in ( Cl (A \ {x}));

        let U be open Subset of T;

        assume x in U;

        then (A \ {x}) meets U by A1, PRE_TOPC: 24;

        then

        consider y be object such that

         A2: y in (A \ {x}) and

         A3: y in U by XBOOLE_0: 3;

        reconsider y as Point of T by A2;

        take y;

        y in A by A2, ZFMISC_1: 56;

        hence y in (A /\ U) & x <> y by A2, A3, XBOOLE_0:def 4, ZFMISC_1: 56;

      end;

      assume

       A4: for U be open Subset of T st x in U holds ex y be Point of T st y in (A /\ U) & x <> y;

      for G be Subset of T st G is open holds x in G implies (A \ {x}) meets G

      proof

        let G be Subset of T;

        assume

         A5: G is open;

        assume x in G;

        then

        consider y be Point of T such that

         A6: y in (A /\ G) and

         A7: x <> y by A4, A5;

        y in A by A6, XBOOLE_0:def 4;

        then

         A8: y in (A \ {x}) by A7, ZFMISC_1: 56;

        y in G by A6, XBOOLE_0:def 4;

        hence thesis by A8, XBOOLE_0: 3;

      end;

      then x in ( Cl (A \ {x})) by PRE_TOPC: 24;

      then x is_an_accumulation_point_of A;

      hence thesis by Th16;

    end;

    theorem :: TOPGEN_1:18

    for T be non empty TopSpace, A be Subset of T, x be Point of T holds x in ( Der A) iff for B be Basis of x, U be Subset of T st U in B holds ex y be Point of T st y in (A /\ U) & x <> y

    proof

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

      hereby

        assume x in ( Der A);

        then x is_an_accumulation_point_of A by Th16;

        then

         A1: x in ( Cl (A \ {x}));

        let B be Basis of x, U be Subset of T;

        assume U in B;

        then U is open & x in U by YELLOW_8: 12;

        then (A \ {x}) meets U by A1, PRE_TOPC: 24;

        then

        consider y be object such that

         A2: y in (A \ {x}) and

         A3: y in U by XBOOLE_0: 3;

        reconsider y as Point of T by A2;

        take y;

        y in A by A2, ZFMISC_1: 56;

        hence y in (A /\ U) & x <> y by A2, A3, XBOOLE_0:def 4, ZFMISC_1: 56;

      end;

      assume

       A4: for B be Basis of x, U be Subset of T st U in B holds ex y be Point of T st y in (A /\ U) & x <> y;

      for G be Subset of T st G is open holds x in G implies (A \ {x}) meets G

      proof

        set B = the Basis of x;

        let G be Subset of T;

        assume

         A5: G is open;

        assume x in G;

        then

        consider V be Subset of T such that

         A6: V in B & V c= G by A5, YELLOW_8: 13;

        (ex y be Point of T st y in (A /\ V) & x <> y) & (A /\ V) c= (A /\ G) by A4, A6, XBOOLE_1: 26;

        then

        consider y be Point of T such that

         A7: y in (A /\ G) and

         A8: x <> y;

        y in A by A7, XBOOLE_0:def 4;

        then

         A9: y in (A \ {x}) by A8, ZFMISC_1: 56;

        y in G by A7, XBOOLE_0:def 4;

        hence thesis by A9, XBOOLE_0: 3;

      end;

      then x in ( Cl (A \ {x})) by PRE_TOPC: 24;

      then x is_an_accumulation_point_of A;

      hence thesis by Th16;

    end;

    theorem :: TOPGEN_1:19

    for T be non empty TopSpace, A be Subset of T, x be Point of T holds x in ( Der A) iff ex B be Basis of x st for U be Subset of T st U in B holds ex y be Point of T st y in (A /\ U) & x <> y

    proof

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

      hereby

        set B = the Basis of x;

        assume x in ( Der A);

        then x is_an_accumulation_point_of A by Th16;

        then

         A1: x in ( Cl (A \ {x}));

        take B;

        let U be Subset of T;

        assume U in B;

        then U is open & x in U by YELLOW_8: 12;

        then (A \ {x}) meets U by A1, PRE_TOPC: 24;

        then

        consider y be object such that

         A2: y in (A \ {x}) and

         A3: y in U by XBOOLE_0: 3;

        reconsider y as Point of T by A2;

        take y;

        y in A by A2, ZFMISC_1: 56;

        hence y in (A /\ U) & x <> y by A2, A3, XBOOLE_0:def 4, ZFMISC_1: 56;

      end;

      given B be Basis of x such that

       A4: for U be Subset of T st U in B holds ex y be Point of T st y in (A /\ U) & x <> y;

      for G be Subset of T st G is open holds x in G implies (A \ {x}) meets G

      proof

        let G be Subset of T;

        assume

         A5: G is open;

        assume x in G;

        then

        consider V be Subset of T such that

         A6: V in B & V c= G by A5, YELLOW_8: 13;

        (ex y be Point of T st y in (A /\ V) & x <> y) & (A /\ V) c= (A /\ G) by A4, A6, XBOOLE_1: 26;

        then

        consider y be Point of T such that

         A7: y in (A /\ G) and

         A8: x <> y;

        y in A by A7, XBOOLE_0:def 4;

        then

         A9: y in (A \ {x}) by A8, ZFMISC_1: 56;

        y in G by A7, XBOOLE_0:def 4;

        hence thesis by A9, XBOOLE_0: 3;

      end;

      then x in ( Cl (A \ {x})) by PRE_TOPC: 24;

      then x is_an_accumulation_point_of A;

      hence thesis by Th16;

    end;

    begin

    definition

      let T be TopSpace, A be Subset of T, x be set;

      :: TOPGEN_1:def4

      pred x is_isolated_in A means x in A & not x is_an_accumulation_point_of A;

    end

    theorem :: TOPGEN_1:20

    for T be non empty TopSpace, A be Subset of T, p be set holds p in (A \ ( Der A)) iff p is_isolated_in A

    proof

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

      hereby

        assume

         A1: p in (A \ ( Der A));

        then not p in ( Der A) by XBOOLE_0:def 5;

        then

         A2: not p is_an_accumulation_point_of A by Th16;

        p in A by A1, XBOOLE_0:def 5;

        hence p is_isolated_in A by A2;

      end;

      assume

       A3: p is_isolated_in A;

      then not p is_an_accumulation_point_of A;

      then

       A4: not p in ( Der A) by Th16;

      p in A by A3;

      hence thesis by A4, XBOOLE_0:def 5;

    end;

    theorem :: TOPGEN_1:21



     Th21: for T be non empty TopSpace, A be Subset of T, p be Point of T holds p is_an_accumulation_point_of A iff 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 T be non empty TopSpace, A be Subset of T, p be Point of T;

      hereby

        assume p is_an_accumulation_point_of A;

        then

         A1: p in ( Der A) by Th16;

        let U be open Subset of T;

        assume p in U;

        then

        consider q be Point of T such that

         A2: q in (A /\ U) & p <> q by A1, Th17;

        take q;

        thus q <> p & q in A & q in U by A2, XBOOLE_0:def 4;

      end;

      assume

       A3: 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;

      for U be open Subset of T st p in U holds ex y be Point of T st y in (A /\ U) & p <> y

      proof

        let U be open Subset of T;

        assume p in U;

        then

        consider q be Point of T such that

         A4: q <> p & q in A & q in U by A3;

        take q;

        thus thesis by A4, XBOOLE_0:def 4;

      end;

      then p in ( Der A) by Th17;

      hence thesis by Th16;

    end;

    theorem :: TOPGEN_1:22



     Th22: for T be non empty TopSpace, A be Subset of T, p be Point of T holds p is_isolated_in A iff ex G be open Subset of T st (G /\ A) = {p}

    proof

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

      hereby

        assume

         A1: p is_isolated_in A;

        then not p is_an_accumulation_point_of A;

        then

        consider U be open Subset of T such that

         A2: p in U and

         A3: not ex q be Point of T st q <> p & q in A & q in U by Th21;

        take U;



         A4: p in A by A1;

        (U /\ A) = {p}

        proof

          thus (U /\ A) c= {p}

          proof

            let x be object;

            assume x in (U /\ A);

            then x in U & x in A by XBOOLE_0:def 4;

            then x = p by A3;

            hence thesis by TARSKI:def 1;

          end;

          let x be object;

          assume x in {p};

          then x = p by TARSKI:def 1;

          hence thesis by A4, A2, XBOOLE_0:def 4;

        end;

        hence (U /\ A) = {p};

      end;

      given G be open Subset of T such that

       A5: (G /\ A) = {p};



       A6: p in (G /\ A) by A5, TARSKI:def 1;

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

      proof

        take G;

        for q be Point of T holds q = p or not q in A or not q in G

        proof

          given q be Point of T such that

           A7: q <> p and

           A8: q in A & q in G;

          q in (A /\ G) by A8, XBOOLE_0:def 4;

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

        end;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      then

       A9: not p is_an_accumulation_point_of A by Th21;

      p in A by A6, XBOOLE_0:def 4;

      hence thesis by A9;

    end;

    definition

      let T be TopSpace, p be Point of T;

      :: TOPGEN_1:def5

      attr p is isolated means p is_isolated_in ( [#] T);

    end

    theorem :: TOPGEN_1:23

    for T be non empty TopSpace, p be Point of T holds p is isolated iff {p} is open

    proof

      let T be non empty TopSpace, p be Point of T;



       A1: ( {p} /\ ( [#] T)) = {p} by XBOOLE_1: 28;

      hereby

        assume p is isolated;

        then p is_isolated_in ( [#] T);

        then ex G be open Subset of T st (G /\ ( [#] T)) = {p} by Th22;

        hence {p} is open;

      end;

      assume {p} is open;

      then p is_isolated_in ( [#] T) by A1, Th22;

      hence thesis;

    end;

    begin

    definition

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

      :: TOPGEN_1:def6

      func Der F -> Subset-Family of T means

      : Def6: for A be Subset of T holds A in it iff ex B be Subset of T st A = ( Der B) & B in F;

      existence

      proof

        defpred P[ object] means ex W be Subset of T st $1 = ( Der W) & W in F;

        thus ex S be Subset-Family of T st for Z be Subset of T holds Z in S iff P[Z] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        defpred P[ object] means ex W be Subset of T st $1 = ( Der W) & W in F;

        let H,G be Subset-Family of T;

        assume that

         A1: for Z be Subset of T holds Z in H iff P[Z] and

         A2: for X be Subset of T holds X in G iff P[X];

        now

          let X be object;

          assume

           A3: X in G;

          then

          reconsider X9 = X as Subset of T;

           P[X9] by A2, A3;

          hence X in H by A1;

        end;

        then

         A4: G c= H;

        now

          let Z be object;

          assume Z in H;

          then P[Z] by A1;

          hence Z in G by A2;

        end;

        then H c= G;

        hence thesis by A4;

      end;

    end

    reserve T for non empty TopSpace,

A,B for Subset of T,

F,G for Subset-Family of T,

x for set;

    theorem :: TOPGEN_1:24

    F = {} implies ( Der F) = {}

    proof

      assume

       A1: F = {} ;

      assume ( Der F) <> {} ;

      then

      consider x be object such that

       A2: x in ( Der F) by XBOOLE_0:def 1;

      ex B be Subset of T st x = ( Der B) & B in F by A2, Def6;

      hence thesis by A1;

    end;

    theorem :: TOPGEN_1:25

    F = {A} implies ( Der F) = {( Der A)}

    proof

      assume

       A1: F = {A};

      thus ( Der F) c= {( Der A)}

      proof

        let x be object;

        assume

         A2: x in ( Der F);

        then

        reconsider B = x as Subset of T;

        consider C be Subset of T such that

         A3: B = ( Der C) and

         A4: C in F by A2, Def6;

        C = A by A1, A4, TARSKI:def 1;

        hence thesis by A3, TARSKI:def 1;

      end;

      let x be object;

      assume x in {( Der A)};

      then

       A5: x = ( Der A) by TARSKI:def 1;

      A in F by A1, TARSKI:def 1;

      hence thesis by A5, Def6;

    end;

    theorem :: TOPGEN_1:26



     Th26: F c= G implies ( Der F) c= ( Der G)

    proof

      assume

       A1: F c= G;

      ( Der F) c= ( Der G)

      proof

        let x be object;

        assume

         A2: x in ( Der F);

        then

        reconsider A = x as Subset of T;

        ex B be Subset of T st A = ( Der B) & B in F by A2, Def6;

        hence thesis by A1, Def6;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_1:27

    ( Der (F \/ G)) = (( Der F) \/ ( Der G))

    proof

      thus ( Der (F \/ G)) c= (( Der F) \/ ( Der G))

      proof

        let x be object;

        assume

         A1: x in ( Der (F \/ G));

        then

        reconsider A = x as Subset of T;

        consider B be Subset of T such that

         A2: A = ( Der B) and

         A3: B in (F \/ G) by A1, Def6;

        per cases by A3, XBOOLE_0:def 3;

          suppose B in F;

          then A in ( Der F) by A2, Def6;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose B in G;

          then A in ( Der G) by A2, Def6;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      ( Der F) c= ( Der (F \/ G)) & ( Der G) c= ( Der (F \/ G)) by Th26, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: TOPGEN_1:28



     Th28: for T be non empty TopSpace, A be Subset of T holds ( Der A) c= ( Cl A)

    proof

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

      let x be object;

      assume

       A1: x in ( Der A);

      then

      reconsider x9 = x as Point of T;

      for G be Subset of T st G is open holds x9 in G implies A meets G

      proof

        let G be Subset of T;

        assume

         A2: G is open;

        assume x9 in G;

        then ex y be Point of T st y in (A /\ G) & x <> y by A1, A2, Th17;

        hence thesis;

      end;

      hence thesis by PRE_TOPC: 24;

    end;

    theorem :: TOPGEN_1:29



     Th29: for T be TopSpace, A be Subset of T holds ( Cl A) = (A \/ ( Der A))

    proof

      let T be TopSpace, A be Subset of T;

      per cases ;

        suppose

         A1: T is non empty;

        then

         A2: ( Der A) c= ( Cl A) by Th28;

        thus ( Cl A) c= (A \/ ( Der A))

        proof

          let x be object;

          assume

           A3: x in ( Cl A);

          then

          reconsider x9 = x as Point of T;

          per cases ;

            suppose x in A;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose

             A4: not x in A;

            for U be open Subset of T st x9 in U holds ex y be Point of T st y in (A /\ U) & x9 <> y

            proof

              let U be open Subset of T;

              assume x9 in U;

              then A meets U by A3, PRE_TOPC: 24;

              then

              consider y be object such that

               A5: y in A and

               A6: y in U by XBOOLE_0: 3;

              reconsider y as Point of T by A5;

              take y;

              thus thesis by A4, A5, A6, XBOOLE_0:def 4;

            end;

            then x9 in ( Der A) by A1, Th17;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        let x be object;

        assume

         A7: x in (A \/ ( Der A));

        per cases by A7, XBOOLE_0:def 3;

          suppose

           A8: x in A;

          A c= ( Cl A) by PRE_TOPC: 18;

          hence thesis by A8;

        end;

          suppose x in ( Der A);

          hence thesis by A2;

        end;

      end;

        suppose

         A9: T is empty;

        then the carrier of T is empty;



        then ( Cl A) = ( {} \/ {} )

        .= (A \/ ( Der A)) by A9;

        hence thesis;

      end;

    end;

    theorem :: TOPGEN_1:30



     Th30: for T be non empty TopSpace, A,B be Subset of T st A c= B holds ( Der A) c= ( Der B)

    proof

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

      assume

       A1: A c= B;

      let x be object;

      assume

       A2: x in ( Der A);

      then

      reconsider x9 = x as Point of T;

      for U be open Subset of T st x9 in U holds ex y be Point of T st y in (B /\ U) & x9 <> y

      proof

        let U be open Subset of T;

        assume x9 in U;

        then

         A3: ex y be Point of T st y in (A /\ U) & x9 <> y by A2, Th17;

        (A /\ U) c= (B /\ U) by A1, XBOOLE_1: 26;

        hence thesis by A3;

      end;

      hence thesis by Th17;

    end;

    theorem :: TOPGEN_1:31



     Th31: for T be non empty TopSpace, A,B be Subset of T holds ( Der (A \/ B)) = (( Der A) \/ ( Der B))

    proof

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

      thus ( Der (A \/ B)) c= (( Der A) \/ ( Der B))

      proof

        let x be object;

        assume x in ( Der (A \/ B));

        then x is_an_accumulation_point_of (A \/ B) by Th16;

        then

         A1: x in ( Cl ((A \/ B) \ {x}));

        ((A \/ B) \ {x}) = ((A \ {x}) \/ (B \ {x})) by XBOOLE_1: 42;

        then ( Cl ((A \/ B) \ {x})) = (( Cl (A \ {x})) \/ ( Cl (B \ {x}))) by PRE_TOPC: 20;

        then x in ( Cl (A \ {x})) or x in ( Cl (B \ {x})) by A1, XBOOLE_0:def 3;

        then x is_an_accumulation_point_of A or x is_an_accumulation_point_of B;

        then x in ( Der A) or x in ( Der B) by Th16;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in (( Der A) \/ ( Der B));

      then x in ( Der A) or x in ( Der B) by XBOOLE_0:def 3;

      then

       A2: x is_an_accumulation_point_of A or x is_an_accumulation_point_of B by Th16;

      x in ( Cl ((A \/ B) \ {x}))

      proof

        (B \ {x}) c= ((A \/ B) \ {x}) by XBOOLE_1: 7, XBOOLE_1: 33;

        then

         A3: ( Cl (B \ {x})) c= ( Cl ((A \/ B) \ {x})) by PRE_TOPC: 19;

        (A \ {x}) c= ((A \/ B) \ {x}) by XBOOLE_1: 7, XBOOLE_1: 33;

        then

         A4: ( Cl (A \ {x})) c= ( Cl ((A \/ B) \ {x})) by PRE_TOPC: 19;

        per cases by A2;

          suppose x in ( Cl (A \ {x}));

          hence thesis by A4;

        end;

          suppose x in ( Cl (B \ {x}));

          hence thesis by A3;

        end;

      end;

      then x is_an_accumulation_point_of (A \/ B);

      hence thesis by Th16;

    end;

    theorem :: TOPGEN_1:32



     Th32: for T be non empty TopSpace, A be Subset of T st T is T_1 holds ( Der ( Der A)) c= ( Der A)

    proof

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

      assume

       A1: T is T_1;

      let x be object;

      assume

       A2: x in ( Der ( Der A));

      then

      reconsider x9 = x as Point of T;

      assume not x in ( Der A);

      then

      consider G be open Subset of T such that

       A3: x9 in G and

       A4: not ex y be Point of T st y in (A /\ G) & x9 <> y by Th17;

      ( Cl {x9}) = {x9} by A1, YELLOW_8: 26;

      then

       A5: (G \ {x9}) is open by FRECHET: 4;

      consider y be Point of T such that

       A6: y in (( Der A) /\ G) and

       A7: x <> y by A2, A3, Th17;

      y in ( Der A) by A6, XBOOLE_0:def 4;

      then

       A8: y in (( Der A) \ {x}) by A7, ZFMISC_1: 56;

      y in G by A6, XBOOLE_0:def 4;

      then

      consider q be set such that

       A9: q in G and

       A10: q in (( Der A) \ {x}) by A8;

      reconsider q as Point of T by A9;

       not q in {x} by A10, XBOOLE_0:def 5;

      then

       A11: q in (G \ {x}) by A9, XBOOLE_0:def 5;

      set U = (G \ {x9});



       A12: G misses (A \ {x})

      proof

        assume G meets (A \ {x});

        then

        consider g be object such that

         A13: g in G and

         A14: g in (A \ {x}) by XBOOLE_0: 3;

        g in A by A14, XBOOLE_0:def 5;

        then g in (A /\ G) by A13, XBOOLE_0:def 4;

        then x9 = g by A4;

        hence thesis by A14, ZFMISC_1: 56;

      end;

      q in ( Der A) by A10, XBOOLE_0:def 5;

      then

      consider y be Point of T such that

       A15: y in (A /\ U) and

       A16: q <> y by A11, A5, Th17;

      y in A by A15, XBOOLE_0:def 4;

      then

       A17: y in (A \ {q}) by A16, ZFMISC_1: 56;

      y in U by A15, XBOOLE_0:def 4;

      then

      consider f be set such that

       A18: f in (G \ {x9}) and

       A19: f in (A \ {q}) by A17;

      f <> x9 & f in A by A18, A19, ZFMISC_1: 56;

      then

       A20: f in (A \ {x9}) by ZFMISC_1: 56;

      f in G by A18, ZFMISC_1: 56;

      hence thesis by A12, A20, XBOOLE_0: 3;

    end;

    theorem :: TOPGEN_1:33



     Th33: for T be TopSpace, A be Subset of T st T is T_1 holds ( Cl ( Der A)) = ( Der A)

    proof

      let T be TopSpace, A be Subset of T;

      assume

       A1: T is T_1;

      per cases ;

        suppose

         A2: T is non empty;

        ( Cl ( Der A)) = (( Der A) \/ ( Der ( Der A))) by Th29;

        then

         A3: ( Cl ( Der A)) c= (( Der A) \/ ( Der A)) by A1, A2, Th32, XBOOLE_1: 9;

        ( Der A) c= ( Cl ( Der A)) by PRE_TOPC: 18;

        hence thesis by A3;

      end;

        suppose

         A4: T is empty;

        then ( Cl ( Der A)) = {} ;

        hence thesis by A4;

      end;

    end;

    registration

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

      cluster ( Der A) -> closed;

      coherence

      proof

        ( Der A) = ( Cl ( Der A)) by Th33;

        hence thesis;

      end;

    end

    theorem :: TOPGEN_1:34



     Th34: for T be non empty TopSpace, F be Subset-Family of T holds ( union ( Der F)) c= ( Der ( union F))

    proof

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

      let x be object;

      assume x in ( union ( Der F));

      then

      consider Y be set such that

       A1: x in Y and

       A2: Y in ( Der F) by TARSKI:def 4;

      reconsider Y as Subset of T by A2;

      consider B be Subset of T such that

       A3: Y = ( Der B) and

       A4: B in F by A2, Def6;

      ( Der B) c= ( Der ( union F)) by A4, Th30, ZFMISC_1: 74;

      hence thesis by A1, A3;

    end;

    theorem :: TOPGEN_1:35

    A c= B & x is_an_accumulation_point_of A implies x is_an_accumulation_point_of B

    proof

      assume A c= B;

      then

       A1: ( Der A) c= ( Der B) by Th30;

      assume x is_an_accumulation_point_of A;

      then x in ( Der A) by Th16;

      hence thesis by A1, Th16;

    end;

    begin

    definition

      let T be TopSpace, A be Subset of T;

      :: TOPGEN_1:def7

      attr A is dense-in-itself means A c= ( Der A);

    end

    definition

      let T be non empty TopSpace;

      :: TOPGEN_1:def8

      attr T is dense-in-itself means ( [#] T) is dense-in-itself;

    end

    theorem :: TOPGEN_1:36



     Th36: T is T_1 & A is dense-in-itself implies ( Cl A) is dense-in-itself

    proof

      assume

       A1: T is T_1;

      assume A is dense-in-itself;

      then A c= ( Der A);



      then

       A2: ( Der A) = (A \/ ( Der A)) by XBOOLE_1: 12

      .= ( Cl A) by Th29;

      ( Der ( Cl A)) = ( Der (A \/ ( Der A))) by Th29

      .= (( Der A) \/ ( Der ( Der A))) by Th31

      .= ( Cl A) by A1, A2, Th32, XBOOLE_1: 12;

      hence thesis;

    end;

    definition

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

      :: TOPGEN_1:def9

      attr F is dense-in-itself means for A be Subset of T st A in F holds A is dense-in-itself;

    end

    theorem :: TOPGEN_1:37



     Th37: for F be Subset-Family of T st F is dense-in-itself holds ( union F) c= ( union ( Der F))

    proof

      let F be Subset-Family of T;

      assume

       A1: F is dense-in-itself;

      thus ( union F) c= ( union ( Der F))

      proof

        let x be object;

        assume x in ( union F);

        then

        consider A be set such that

         A2: x in A and

         A3: A in F by TARSKI:def 4;

        reconsider A as Subset of T by A3;

        A is dense-in-itself by A1, A3;

        then

         A4: A c= ( Der A);

        ( Der A) in ( Der F) by A3, Def6;

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

      end;

    end;

    theorem :: TOPGEN_1:38



     Th38: F is dense-in-itself implies ( union F) is dense-in-itself

    proof

      assume F is dense-in-itself;

      then

       A1: ( union F) c= ( union ( Der F)) by Th37;

      ( union ( Der F)) c= ( Der ( union F)) by Th34;

      then ( union F) c= ( Der ( union F)) by A1;

      hence thesis;

    end;

    theorem :: TOPGEN_1:39

    ( Fr ( {} T)) = {}

    proof

      ( Fr ( {} T)) = (( Cl ( {} T)) /\ ( Cl (( {} T) ` ))) by TOPS_1:def 2

      .= ( {} /\ ( Cl (( {} T) ` )));

      hence thesis;

    end;

    registration

      let T be TopSpace, A be open closed Subset of T;

      cluster ( Fr A) -> empty;

      coherence by Th14;

    end

    registration

      let T be non empty non discrete TopSpace;

      cluster non open for Subset of T;

      existence by TDLAT_3: 15;

      cluster non closed for Subset of T;

      existence by TDLAT_3: 16;

    end

    registration

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

      cluster ( Fr A) -> non empty;

      coherence by Th14;

    end

    registration

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

      cluster ( Fr A) -> non empty;

      coherence by Th14;

    end

    begin

    definition

      let T be TopSpace, A be Subset of T;

      :: TOPGEN_1:def10

      attr A is perfect means A is closed dense-in-itself;

    end

    registration

      let T be TopSpace;

      cluster perfect -> closed dense-in-itself for Subset of T;

      coherence ;

      cluster closed dense-in-itself -> perfect for Subset of T;

      coherence ;

    end

    theorem :: TOPGEN_1:40



     Th40: for T be TopSpace holds ( Der ( {} T)) = ( {} T)

    proof

      let T be TopSpace;

      ( Cl ( {} T)) is empty;



      then {} = (( {} T) \/ ( Der ( {} T))) by Th29

      .= ( Der ( {} T));

      hence thesis;

    end;



     Lm1: for T be TopSpace, A be Subset of T st A is closed dense-in-itself holds ( Der A) = A

    proof

      let T be TopSpace, A be Subset of T;

      assume

       A1: A is closed dense-in-itself;



      then A = ( Cl A) by PRE_TOPC: 22

      .= (( Der A) \/ A) by Th29;

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

      thus thesis by A1;

    end;

    theorem :: TOPGEN_1:41



     Th41: for T be TopSpace, A be Subset of T holds A is perfect iff ( Der A) = A

    proof

      let T be TopSpace, A be Subset of T;

      thus A is perfect implies ( Der A) = A by Lm1;

      assume

       A1: ( Der A) = A;



       A2: ( Cl A) = (( Der A) \/ A) by Th29

      .= A by A1;

      A is dense-in-itself by A1;

      hence thesis by A2;

    end;

    theorem :: TOPGEN_1:42



     Th42: for T be TopSpace holds ( {} T) is perfect

    proof

      let T be TopSpace;

      ( Der ( {} T)) = ( {} T) by Th40;

      hence thesis by Th41;

    end;

    registration

      let T be TopSpace;

      cluster empty -> perfect for Subset of T;

      coherence

      proof

        let A be Subset of T;

        assume A is empty;

        then A = ( {} T);

        hence thesis by Th42;

      end;

    end

    registration

      let T be TopSpace;

      cluster perfect for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    begin

    definition

      let T be TopSpace, A be Subset of T;

      :: TOPGEN_1:def11

      attr A is scattered means not ex B be Subset of T st B is non empty & B c= A & B is dense-in-itself;

    end

    registration

      let T be non empty TopSpace;

      cluster non empty scattered -> non dense-in-itself for Subset of T;

      coherence ;

      cluster dense-in-itself non empty -> non scattered for Subset of T;

      coherence ;

    end

    theorem :: TOPGEN_1:43

    for T be TopSpace holds ( {} T) is scattered;

    registration

      let T be TopSpace;

      cluster empty -> scattered for Subset of T;

      coherence ;

    end

    theorem :: TOPGEN_1:44

    for T be non empty TopSpace st T is T_1 holds ex A,B be Subset of T st (A \/ B) = ( [#] T) & A misses B & A is perfect & B is scattered

    proof

      let T be non empty TopSpace;

      defpred P[ Subset of T] means $1 is dense-in-itself;

      consider CC be Subset-Family of T such that

       A1: for A be Subset of T holds A in CC iff P[A] from SUBSET_1:sch 3;

      set C = ( union CC);



       A2: ( [#] T) = (C \/ (C ` )) & C misses (C ` ) by PRE_TOPC: 2, XBOOLE_1: 79;



       A3: CC is dense-in-itself by A1;

      assume T is T_1;

      then ( Cl C) is dense-in-itself by A3, Th36, Th38;

      then ( Cl C) in CC by A1;

      then

       A4: ( Cl C) c= C by ZFMISC_1: 74;

      C c= ( Cl C) by PRE_TOPC: 18;

      then

       A5: ( Cl C) = C by A4;

       not ex B be Subset of T st B is non empty & B c= (C ` ) & B is dense-in-itself

      proof

        given B be Subset of T such that

         A6: B is non empty and

         A7: B c= (C ` ) & B is dense-in-itself;

        B misses ( union CC) & B in CC by A1, A7, SUBSET_1: 23;

        hence thesis by A6, XBOOLE_1: 69, ZFMISC_1: 74;

      end;

      then

       A8: (C ` ) is scattered;

      C is dense-in-itself by A3, Th38;

      hence thesis by A5, A8, A2;

    end;

    registration

      let T be discrete TopSpace, A be Subset of T;

      cluster ( Fr A) -> empty;

      coherence

      proof

        A is open closed by TDLAT_3: 15, TDLAT_3: 16;

        hence thesis;

      end;

    end

    registration

      let T be discrete TopSpace;

      cluster -> closed open for Subset of T;

      coherence by TDLAT_3: 15, TDLAT_3: 16;

    end

    theorem :: TOPGEN_1:45



     Th45: for T be discrete TopSpace, A be Subset of T holds ( Der A) = {}

    proof

      let T be discrete TopSpace, A be Subset of T;

      per cases ;

        suppose

         A1: T is non empty;

        assume ( Der A) <> {} ;

        then

        consider x be object such that

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

        x is_an_accumulation_point_of A by A1, A2, Th16;

        then x in ( Cl (A \ {x}));

        then x in (A \ {x}) by PRE_TOPC: 22;

        hence thesis by ZFMISC_1: 56;

      end;

        suppose T is empty;

        then the carrier of T is empty;

        hence thesis;

      end;

    end;

    registration

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

      cluster ( Der A) -> empty;

      coherence by Th45;

    end

    begin

    definition

      let T be TopSpace;

      :: TOPGEN_1:def12

      func density T -> cardinal number means

      : Def12: (ex A be Subset of T st A is dense & it = ( card A)) & for B be Subset of T st B is dense holds it c= ( card B);

      existence

      proof

        set B0 = ( [#] T);

        defpred P[ Ordinal] means ex A be Subset of T st A is dense & $1 = ( card A);

        ( card B0) is ordinal;

        then

         A1: ex A be Ordinal st P[A];

        consider A be Ordinal such that

         A2: P[A] and

         A3: for B be Ordinal st P[B] holds A c= B from ORDINAL1:sch 1( A1);

        consider B1 be Subset of T such that

         A4: B1 is dense & A = ( card B1) by A2;

        take ( card B1);

        thus thesis by A3, A4;

      end;

      uniqueness ;

    end

    definition

      let T be TopSpace;

      :: TOPGEN_1:def13

      attr T is separable means ( density T) c= omega ;

    end

    theorem :: TOPGEN_1:46



     Th46: for T be countable TopSpace holds T is separable

    proof

      let T be countable TopSpace;

      ( card ( [#] T)) c= omega & ( density T) c= ( card ( [#] T)) by Def12, CARD_3:def 14;

      then ( density T) c= omega ;

      hence thesis;

    end;

    registration

      cluster countable -> separable for TopSpace;

      coherence by Th46;

    end

    begin

    theorem :: TOPGEN_1:47

    for A be Subset of R^1 st A = RAT holds (A ` ) = IRRAT by BORSUK_5:def 1, TOPMETR: 17;



     Lm2: RAT = ( REAL \ IRRAT )

    proof

      ( REAL \ IRRAT ) = ( REAL /\ RAT ) by BORSUK_5:def 1, XBOOLE_1: 48;

      hence thesis by NUMBERS: 12, XBOOLE_1: 28;

    end;

    theorem :: TOPGEN_1:48

    for A be Subset of R^1 st A = IRRAT holds (A ` ) = RAT by Lm2, TOPMETR: 17;

    theorem :: TOPGEN_1:49

    for A be Subset of R^1 st A = RAT holds ( Int A) = {}

    proof

      let A be Subset of R^1 ;

      assume A = RAT ;

      then ( Cl (A ` )) = ( [#] R^1 ) by BORSUK_5: 28, BORSUK_5:def 1, TOPMETR: 17;

      then (( Cl (A ` )) ` ) = ( {} R^1 ) by XBOOLE_1: 37;

      hence thesis by Th3;

    end;

    theorem :: TOPGEN_1:50

    for A be Subset of R^1 st A = IRRAT holds ( Int A) = {}

    proof

      let A be Subset of R^1 ;

      assume A = IRRAT ;

      then ( Cl (A ` )) = ( [#] R^1 ) by Lm2, BORSUK_5: 15, TOPMETR: 17;

      then (( Cl (A ` )) ` ) = ( {} R^1 ) by XBOOLE_1: 37;

      hence thesis by Th3;

    end;

    reconsider B = RAT as Subset of R^1 by NUMBERS: 12, TOPMETR: 17;

    theorem :: TOPGEN_1:51



     Th51: RAT is dense Subset of R^1

    proof

      ( Cl B) = the carrier of R^1 by BORSUK_5: 15;

      hence thesis by TOPS_3:def 2;

    end;

    reconsider A = IRRAT as Subset of R^1 by TOPMETR: 17;

    theorem :: TOPGEN_1:52



     Th52: IRRAT is dense Subset of R^1

    proof

      ( Cl A) = the carrier of R^1 by BORSUK_5: 28;

      hence thesis by TOPS_3:def 2;

    end;

    theorem :: TOPGEN_1:53



     Th53: RAT is boundary Subset of R^1

    proof

      (B ` ) is dense by Th52, BORSUK_5:def 1, TOPMETR: 17;

      hence thesis by TOPS_1:def 4;

    end;

    theorem :: TOPGEN_1:54



     Th54: IRRAT is boundary Subset of R^1

    proof

      (A ` ) is dense by Lm2, Th51, TOPMETR: 17;

      hence thesis by TOPS_1:def 4;

    end;

    theorem :: TOPGEN_1:55



     Th55: REAL is non boundary Subset of R^1

    proof

      reconsider A = ( [#] REAL ) as Subset of R^1 by TOPMETR: 17;

      ( [#] R^1 ) = REAL by TOPMETR: 17;

      hence thesis;

    end;

    theorem :: TOPGEN_1:56

    ex A,B be Subset of R^1 st A is boundary & B is boundary & (A \/ B) is non boundary

    proof

      reconsider B = IRRAT as Subset of R^1 by TOPMETR: 17;

      reconsider A = RAT as Subset of R^1 by NUMBERS: 12, TOPMETR: 17;

      take A, B;

      (A \/ B) = ( RAT \/ REAL ) by BORSUK_5:def 1, XBOOLE_1: 39

      .= REAL by NUMBERS: 12, XBOOLE_1: 12;

      hence thesis by Th53, Th54, Th55;

    end;