tex_3.miz



    begin

    reserve X for non empty TopSpace,

A,B for Subset of X;

    theorem :: TEX_3:1

    

     Th1: (A,B) constitute_a_decomposition implies (A is non empty iff B is proper)

    proof

      assume

       A1: (A,B) constitute_a_decomposition ;

      then

       A2: B = (A ` ) by TSEP_2: 3;

      thus A is non empty implies B is proper by A2, TOPS_3: 1, SUBSET_1:def 6;

      assume

       A3: B is proper;

      A = (B ` ) by A1, TSEP_2: 3;

      hence thesis by A3;

    end;

    

     Lm1: A is everywhere_dense & B is everywhere_dense implies A meets B

    proof

      assume A is everywhere_dense & B is everywhere_dense;

      then (A /\ B) <> {} by TOPS_3: 34, TOPS_3: 44;

      hence thesis by XBOOLE_0:def 7;

    end;

    

     Lm2: A is everywhere_dense & B is dense or A is dense & B is everywhere_dense implies A meets B

    proof

      assume A is everywhere_dense & B is dense or A is dense & B is everywhere_dense;

      then (A /\ B) <> {} by TOPS_3: 17, TOPS_3: 45;

      hence thesis by XBOOLE_0:def 7;

    end;

    theorem :: TEX_3:2

    

     Th2: (A,B) constitute_a_decomposition implies (A is dense iff B is boundary)

    proof

      assume

       A1: (A,B) constitute_a_decomposition ;

      then B = (A ` ) by TSEP_2: 3;

      hence A is dense implies B is boundary by TOPS_3: 18;

      assume

       A2: B is boundary;

      A = (B ` ) by A1, TSEP_2: 3;

      hence thesis by A2, TOPS_1:def 4;

    end;

    theorem :: TEX_3:3

    (A,B) constitute_a_decomposition implies (A is boundary iff B is dense) by Th2;

    theorem :: TEX_3:4

    

     Th4: (A,B) constitute_a_decomposition implies (A is everywhere_dense iff B is nowhere_dense)

    proof

      assume

       A1: (A,B) constitute_a_decomposition ;

      then B = (A ` ) by TSEP_2: 3;

      hence A is everywhere_dense implies B is nowhere_dense by TOPS_3: 39;

      assume

       A2: B is nowhere_dense;

      A = (B ` ) by A1, TSEP_2: 3;

      hence thesis by A2, TOPS_3: 40;

    end;

    theorem :: TEX_3:5

    (A,B) constitute_a_decomposition implies (A is nowhere_dense iff B is everywhere_dense) by Th4;

    reserve Y1,Y2 for non empty SubSpace of X;

    theorem :: TEX_3:6

    

     Th6: (Y1,Y2) constitute_a_decomposition implies Y1 is proper & Y2 is proper

    proof

      reconsider A1 = the carrier of Y1, A2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      assume (Y1,Y2) constitute_a_decomposition ;

      then (A1,A2) constitute_a_decomposition ;

      then A1 is proper & A2 is proper by Th1;

      hence thesis by TEX_2: 8;

    end;

    theorem :: TEX_3:7

    for X be non trivial TopSpace, D be non empty proper Subset of X holds ex Y0 be proper strict non empty SubSpace of X st D = the carrier of Y0

    proof

      let X be non trivial TopSpace, D be non empty proper Subset of X;

      consider Y0 be strict non empty SubSpace of X such that

       A1: D = the carrier of Y0 by TSEP_1: 10;

      reconsider Y0 as proper strict non empty SubSpace of X by A1, TEX_2: 8;

      take Y0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:8

    

     Th8: for X be non trivial TopSpace, Y1 be proper non empty SubSpace of X holds ex Y2 be proper strict non empty SubSpace of X st (Y1,Y2) constitute_a_decomposition

    proof

      let X be non trivial TopSpace, Y1 be proper non empty SubSpace of X;

      reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1: 1;

      A1 is proper by TEX_2: 8;

      then

      consider Y2 be strict non empty SubSpace of X such that

       A1: (A1 ` ) = the carrier of Y2 by TSEP_1: 10;

      

       A2: for P,Q be Subset of X st P = the carrier of Y1 & Q = the carrier of Y2 holds (P,Q) constitute_a_decomposition by A1, TSEP_2: 5;

      then (Y1,Y2) constitute_a_decomposition ;

      then

      reconsider Y2 as proper strict non empty SubSpace of X by Th6;

      take Y2;

      thus thesis by A2;

    end;

    begin

    definition

      let X be non empty TopSpace;

      let IT be SubSpace of X;

      :: TEX_3:def1

      attr IT is dense means

      : Def1: for A be Subset of X st A = the carrier of IT holds A is dense;

    end

    theorem :: TEX_3:9

    

     Th9: for X0 be SubSpace of X, A be Subset of X st A = the carrier of X0 holds X0 is dense iff A is dense;

    registration

      let X be non empty TopSpace;

      cluster dense closed -> non proper for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

        assume

         A1: X0 is dense closed;

        then A is closed by TSEP_1: 11;

        then

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

        A is dense by A1;

        then ( Cl A) = the carrier of X by TOPS_3:def 2;

        then A is non proper by A2, SUBSET_1:def 6;

        hence thesis by TEX_2: 8;

      end;

      cluster dense proper -> non closed for SubSpace of X;

      coherence ;

      cluster proper closed -> non dense for SubSpace of X;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      cluster dense strict non empty for SubSpace of X;

      existence

      proof

        X is SubSpace of X by TSEP_1: 2;

        then

        reconsider A0 = the carrier of X as Subset of X by TSEP_1: 1;

        consider X0 be strict non empty SubSpace of X such that

         A1: A0 = the carrier of X0 by TSEP_1: 10;

        take X0;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A = ( [#] X) by A1;

          hence A is dense;

        end;

        hence thesis;

      end;

    end

    theorem :: TEX_3:10

    

     Th10: for A0 be non empty Subset of X st A0 is dense holds ex X0 be dense strict non empty SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume A0 is dense;

      then

      reconsider Y0 = X0 as dense strict non empty SubSpace of X by A1, Th9;

      take Y0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:11

    for X0 be dense non empty SubSpace of X, A be Subset of X, B be Subset of X0 st A = B holds B is dense iff A is dense

    proof

      let X0 be dense non empty SubSpace of X, A be Subset of X, B be Subset of X0;

      assume

       A1: A = B;

      reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

      C is dense by Th9;

      hence thesis by A1, TOPS_3: 60;

    end;

    theorem :: TEX_3:12

    for X1 be dense SubSpace of X, X2 be SubSpace of X holds X1 is SubSpace of X2 implies X2 is dense

    proof

      let X1 be dense SubSpace of X, X2 be SubSpace of X;

      reconsider C = the carrier of X1 as Subset of X by BORSUK_1: 1;

      assume X1 is SubSpace of X2;

      then

       A1: the carrier of X1 c= the carrier of X2 by TSEP_1: 4;

      C is dense by Def1;

      then for A be Subset of X st A = the carrier of X2 holds A is dense by A1, TOPS_1: 44;

      hence thesis;

    end;

    theorem :: TEX_3:13

    for X1 be dense non empty SubSpace of X, X2 be non empty SubSpace of X holds X1 is SubSpace of X2 implies X1 is dense SubSpace of X2

    proof

      let X1 be dense non empty SubSpace of X, X2 be non empty SubSpace of X;

      reconsider C = the carrier of X1 as Subset of X by BORSUK_1: 1;

      C is dense by Def1;

      then

       A1: for A be Subset of X2 st A = the carrier of X1 holds A is dense by TOPS_3: 59;

      assume X1 is SubSpace of X2;

      hence thesis by A1, Def1;

    end;

    theorem :: TEX_3:14

    for X1 be dense non empty SubSpace of X, X2 be dense non empty SubSpace of X1 holds X2 is dense non empty SubSpace of X

    proof

      let X1 be dense non empty SubSpace of X, X2 be dense non empty SubSpace of X1;

      reconsider C = the carrier of X1 as Subset of X by BORSUK_1: 1;

      now

        let A be Subset of X;

        assume

         A1: A = the carrier of X2;

        then

        reconsider B = A as Subset of X1 by BORSUK_1: 1;

        

         A2: C is dense by Def1;

        B is dense by A1, Def1;

        hence A is dense by A2, TOPS_3: 60;

      end;

      hence thesis by Def1, TSEP_1: 7;

    end;

    theorem :: TEX_3:15

    for Y1,Y2 be non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X

    proof

      let X1,X2 be non empty TopSpace;

      assume

       A1: X2 = the TopStruct of X1;

      thus X1 is dense SubSpace of X implies X2 is dense SubSpace of X

      proof

        assume

         A2: X1 is dense SubSpace of X;

        then

        reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1: 7;

        for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is dense by A1, A2, Def1;

        hence thesis by Def1;

      end;

      assume

       A3: X2 is dense SubSpace of X;

      then

      reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1: 7;

      for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is dense by A1, A3, Def1;

      hence thesis by Def1;

    end;

    definition

      let X be non empty TopSpace;

      let IT be SubSpace of X;

      :: TEX_3:def2

      attr IT is everywhere_dense means

      : Def2: for A be Subset of X st A = the carrier of IT holds A is everywhere_dense;

    end

    theorem :: TEX_3:16

    

     Th16: for X0 be SubSpace of X, A be Subset of X st A = the carrier of X0 holds X0 is everywhere_dense iff A is everywhere_dense;

    registration

      let X be non empty TopSpace;

      cluster everywhere_dense -> dense for SubSpace of X;

      coherence by TOPS_3: 33;

      cluster non dense -> non everywhere_dense for SubSpace of X;

      coherence ;

      cluster non proper -> everywhere_dense for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        assume

         A1: X0 is non proper;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A is non proper by A1, TEX_2: 8;

          then A = ( [#] X) by SUBSET_1:def 6;

          hence A is everywhere_dense by TOPS_3: 31;

        end;

        hence thesis;

      end;

      cluster non everywhere_dense -> proper for SubSpace of X;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      cluster everywhere_dense strict non empty for SubSpace of X;

      existence

      proof

        X is SubSpace of X by TSEP_1: 2;

        then

        reconsider A0 = the carrier of X as Subset of X by TSEP_1: 1;

        consider X0 be strict non empty SubSpace of X such that

         A1: A0 = the carrier of X0 by TSEP_1: 10;

        take X0;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A = ( [#] X) by A1;

          hence A is everywhere_dense by TOPS_3: 31;

        end;

        hence thesis;

      end;

    end

    theorem :: TEX_3:17

    

     Th17: for A0 be non empty Subset of X st A0 is everywhere_dense holds ex X0 be everywhere_dense strict non empty SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume A0 is everywhere_dense;

      then

      reconsider Y0 = X0 as everywhere_dense strict non empty SubSpace of X by A1, Th16;

      take Y0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:18

    for X0 be everywhere_dense non empty SubSpace of X, A be Subset of X, B be Subset of X0 st A = B holds B is everywhere_dense iff A is everywhere_dense

    proof

      let X0 be everywhere_dense non empty SubSpace of X, A be Subset of X, B be Subset of X0;

      assume

       A1: A = B;

      reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

      C is everywhere_dense by Th16;

      hence thesis by A1, TOPS_3: 64;

    end;

    theorem :: TEX_3:19

    for X1 be everywhere_dense SubSpace of X, X2 be SubSpace of X holds X1 is SubSpace of X2 implies X2 is everywhere_dense

    proof

      let X1 be everywhere_dense SubSpace of X, X2 be SubSpace of X;

      reconsider C = the carrier of X1 as Subset of X by BORSUK_1: 1;

      assume X1 is SubSpace of X2;

      then

       A1: the carrier of X1 c= the carrier of X2 by TSEP_1: 4;

      C is everywhere_dense by Def2;

      then for A be Subset of X st A = the carrier of X2 holds A is everywhere_dense by A1, TOPS_3: 38;

      hence thesis;

    end;

    theorem :: TEX_3:20

    for X1 be everywhere_dense non empty SubSpace of X, X2 be non empty SubSpace of X holds X1 is SubSpace of X2 implies X1 is everywhere_dense SubSpace of X2

    proof

      let X1 be everywhere_dense non empty SubSpace of X, X2 be non empty SubSpace of X;

      reconsider C = the carrier of X1 as Subset of X by BORSUK_1: 1;

      C is everywhere_dense by Def2;

      then

       A1: for A be Subset of X2 st A = the carrier of X1 holds A is everywhere_dense by TOPS_3: 61;

      assume X1 is SubSpace of X2;

      hence thesis by A1, Def2;

    end;

    theorem :: TEX_3:21

    for X1 be everywhere_dense non empty SubSpace of X, X2 be everywhere_dense non empty SubSpace of X1 holds X2 is everywhere_dense SubSpace of X

    proof

      let X1 be everywhere_dense non empty SubSpace of X, X2 be everywhere_dense non empty SubSpace of X1;

      reconsider C = the carrier of X1 as Subset of X by BORSUK_1: 1;

      now

        let A be Subset of X;

        assume

         A1: A = the carrier of X2;

        then

        reconsider B = A as Subset of X1 by BORSUK_1: 1;

        

         A2: C is everywhere_dense by Def2;

        B is everywhere_dense by A1, Def2;

        hence A is everywhere_dense by A2, TOPS_3: 64;

      end;

      hence thesis by Def2, TSEP_1: 7;

    end;

    theorem :: TEX_3:22

    for Y1,Y2 be non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X

    proof

      let X1,X2 be non empty TopSpace;

      assume

       A1: X2 = the TopStruct of X1;

      thus X1 is everywhere_dense SubSpace of X implies X2 is everywhere_dense SubSpace of X

      proof

        assume

         A2: X1 is everywhere_dense SubSpace of X;

        then

        reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1: 7;

        for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is everywhere_dense by A1, A2, Def2;

        hence thesis by Def2;

      end;

      assume

       A3: X2 is everywhere_dense SubSpace of X;

      then

      reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1: 7;

      for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is everywhere_dense by A1, A3, Def2;

      hence thesis by Def2;

    end;

    registration

      let X be non empty TopSpace;

      cluster dense open -> everywhere_dense for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        assume

         A1: X0 is dense open;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A is dense & A is open by A1, TSEP_1: 16;

          hence A is everywhere_dense by TOPS_3: 36;

        end;

        hence thesis;

      end;

      cluster dense non everywhere_dense -> non open for SubSpace of X;

      coherence ;

      cluster open non everywhere_dense -> non dense for SubSpace of X;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      cluster dense open strict non empty for SubSpace of X;

      existence

      proof

        X is SubSpace of X by TSEP_1: 2;

        then

        reconsider A0 = the carrier of X as Subset of X by TSEP_1: 1;

        A0 = ( [#] X);

        then A0 is dense;

        then

        consider X0 be dense strict non empty SubSpace of X such that

         A1: A0 = the carrier of X0 by Th10;

        take X0;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A = ( [#] X) by A1;

          hence A is open;

        end;

        hence thesis by TSEP_1:def 1;

      end;

    end

    theorem :: TEX_3:23

    

     Th23: for A0 be non empty Subset of X st A0 is dense open holds ex X0 be dense open strict non empty SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume A0 is dense open;

      then

      reconsider Y0 = X0 as dense open strict non empty SubSpace of X by A1, Th9, TSEP_1: 16;

      take Y0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:24

    for X0 be SubSpace of X holds X0 is everywhere_dense iff ex X1 be dense open strict SubSpace of X st X1 is SubSpace of X0

    proof

      let X0 be SubSpace of X;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      thus X0 is everywhere_dense implies ex X1 be dense open strict SubSpace of X st X1 is SubSpace of X0

      proof

        assume X0 is everywhere_dense;

        then A is everywhere_dense;

        then

        consider C be Subset of X such that

         A1: C c= A and

         A2: C is open and

         A3: C is dense by TOPS_3: 41;

        C is non empty by A3, TOPS_3: 17;

        then

        consider X1 be dense open strict non empty SubSpace of X such that

         A4: C = the carrier of X1 by A2, A3, Th23;

        take X1;

        thus thesis by A1, A4, TSEP_1: 4;

      end;

      given X1 be dense open strict SubSpace of X such that

       A5: X1 is SubSpace of X0;

      reconsider C = the carrier of X1 as Subset of X by TSEP_1: 1;

      now

        take C;

        thus C c= A & C is open & C is dense by A5, Def1, TSEP_1: 4, TSEP_1: 16;

      end;

      then for A be Subset of X st A = the carrier of X0 holds A is everywhere_dense by TOPS_3: 41;

      hence thesis;

    end;

    reserve X1,X2 for non empty SubSpace of X;

    theorem :: TEX_3:25

    X1 is dense or X2 is dense implies (X1 union X2) is dense SubSpace of X

    proof

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider A = the carrier of (X1 union X2) as Subset of X by TSEP_1: 1;

      assume X1 is dense or X2 is dense;

      then A1 is dense or A2 is dense;

      then (A1 \/ A2) is dense by TOPS_3: 21;

      then A is dense by TSEP_1:def 2;

      hence thesis by Th9;

    end;

    theorem :: TEX_3:26

    X1 is everywhere_dense or X2 is everywhere_dense implies (X1 union X2) is everywhere_dense SubSpace of X

    proof

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider A = the carrier of (X1 union X2) as Subset of X by TSEP_1: 1;

      assume X1 is everywhere_dense or X2 is everywhere_dense;

      then A1 is everywhere_dense or A2 is everywhere_dense;

      then (A1 \/ A2) is everywhere_dense by TOPS_3: 43;

      then A is everywhere_dense by TSEP_1:def 2;

      hence thesis by Th16;

    end;

    theorem :: TEX_3:27

    X1 is everywhere_dense & X2 is everywhere_dense implies (X1 meet X2) is everywhere_dense SubSpace of X

    proof

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider A = the carrier of (X1 meet X2) as Subset of X by TSEP_1: 1;

      assume X1 is everywhere_dense & X2 is everywhere_dense;

      then

       A1: A1 is everywhere_dense & A2 is everywhere_dense;

      then A1 meets A2 by Lm1;

      then

       A2: X1 meets X2 by TSEP_1:def 3;

      (A1 /\ A2) is everywhere_dense by A1, TOPS_3: 44;

      then A is everywhere_dense by A2, TSEP_1:def 4;

      hence thesis by Th16;

    end;

    theorem :: TEX_3:28

    X1 is everywhere_dense & X2 is dense or X1 is dense & X2 is everywhere_dense implies (X1 meet X2) is dense SubSpace of X

    proof

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider A = the carrier of (X1 meet X2) as Subset of X by TSEP_1: 1;

      assume X1 is everywhere_dense & X2 is dense or X1 is dense & X2 is everywhere_dense;

      then

       A1: A1 is everywhere_dense & A2 is dense or A1 is dense & A2 is everywhere_dense;

      then A1 meets A2 by Lm2;

      then

       A2: X1 meets X2 by TSEP_1:def 3;

      (A1 /\ A2) is dense by A1, TOPS_3: 45;

      then A is dense by A2, TSEP_1:def 4;

      hence thesis by Th9;

    end;

    begin

    definition

      let X be non empty TopSpace;

      let IT be SubSpace of X;

      :: TEX_3:def3

      attr IT is boundary means

      : Def3: for A be Subset of X st A = the carrier of IT holds A is boundary;

    end

    theorem :: TEX_3:29

    

     Th29: for X0 be SubSpace of X, A be Subset of X st A = the carrier of X0 holds X0 is boundary iff A is boundary;

    registration

      let X be non empty TopSpace;

      cluster open -> non boundary for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X;

        assume

         A1: X0 is open;

        now

          reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

          assume X0 is boundary;

          then A is boundary;

          then

           A2: ( Int A) = {} ;

          A is open by A1, TSEP_1: 16;

          hence contradiction by A2, TOPS_1: 23;

        end;

        hence thesis;

      end;

      cluster boundary -> non open for non empty SubSpace of X;

      coherence ;

      cluster everywhere_dense -> non boundary for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        assume

         A3: X0 is everywhere_dense;

        now

          reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

          A is everywhere_dense by A3;

          then

           A4: not A is boundary by TOPS_3: 37;

          assume X0 is boundary;

          hence contradiction by A4;

        end;

        hence thesis;

      end;

      cluster boundary -> non everywhere_dense for SubSpace of X;

      coherence ;

    end

    theorem :: TEX_3:30

    

     Th30: for A0 be non empty Subset of X st A0 is boundary holds ex X0 be strict SubSpace of X st X0 is boundary & A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      assume

       A1: A0 is boundary;

      consider X0 be strict non empty SubSpace of X such that

       A2: A0 = the carrier of X0 by TSEP_1: 10;

      take X0;

      thus thesis by A1, A2;

    end;

    theorem :: TEX_3:31

    

     Th31: for X1,X2 be SubSpace of X st (X1,X2) constitute_a_decomposition holds X1 is dense iff X2 is boundary

    proof

      let X1,X2 be SubSpace of X;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) constitute_a_decomposition ;

      thus X1 is dense implies X2 is boundary

      proof

        assume

         A2: for A1 be Subset of X st A1 = the carrier of X1 holds A1 is dense;

        now

          let A2 be Subset of X;

          assume A2 = the carrier of X2;

          then

           A3: (A1,A2) constitute_a_decomposition by A1;

          A1 is dense by A2;

          hence A2 is boundary by A3, Th2;

        end;

        hence thesis;

      end;

      assume

       A4: for A2 be Subset of X st A2 = the carrier of X2 holds A2 is boundary;

      now

        let A1 be Subset of X;

        assume A1 = the carrier of X1;

        then

         A5: (A1,A2) constitute_a_decomposition by A1;

        A2 is boundary by A4;

        hence A1 is dense by A5, Th2;

      end;

      hence thesis;

    end;

    theorem :: TEX_3:32

    for X1,X2 be non empty SubSpace of X st (X1,X2) constitute_a_decomposition holds X1 is boundary iff X2 is dense by Th31;

    theorem :: TEX_3:33

    

     Th33: for X0 be SubSpace of X st X0 is boundary holds for A be Subset of X st A c= the carrier of X0 holds A is boundary

    proof

      let X0 be SubSpace of X;

      reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

      assume X0 is boundary;

      then

       A1: C is boundary;

      let A be Subset of X;

      assume A c= the carrier of X0;

      hence thesis by A1, TOPS_3: 11;

    end;

    theorem :: TEX_3:34

    

     Th34: for X1,X2 be SubSpace of X st X1 is boundary holds X2 is SubSpace of X1 implies X2 is boundary by TSEP_1: 4, Th33;

    definition

      let X be non empty TopSpace;

      let IT be SubSpace of X;

      :: TEX_3:def4

      attr IT is nowhere_dense means

      : Def4: for A be Subset of X st A = the carrier of IT holds A is nowhere_dense;

    end

    theorem :: TEX_3:35

    

     Th35: for X0 be SubSpace of X, A be Subset of X st A = the carrier of X0 holds X0 is nowhere_dense iff A is nowhere_dense;

    registration

      let X be non empty TopSpace;

      cluster nowhere_dense -> boundary for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        assume

         A1: X0 is nowhere_dense;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A is nowhere_dense by A1;

          hence A is boundary;

        end;

        hence thesis;

      end;

      cluster non boundary -> non nowhere_dense for SubSpace of X;

      coherence ;

      cluster nowhere_dense -> non dense for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

        assume X0 is nowhere_dense;

        then A is nowhere_dense;

        then

         A2: not A is dense by TOPS_3: 25;

        assume X0 is dense;

        hence contradiction by A2;

      end;

      cluster dense -> non nowhere_dense for SubSpace of X;

      coherence ;

    end

    reserve X for non empty TopSpace;

    theorem :: TEX_3:36

    for A0 be non empty Subset of X st A0 is nowhere_dense holds ex X0 be strict SubSpace of X st X0 is nowhere_dense & A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      assume

       A1: A0 is nowhere_dense;

      consider X0 be strict non empty SubSpace of X such that

       A2: A0 = the carrier of X0 by TSEP_1: 10;

      take X0;

      thus thesis by A1, A2;

    end;

    theorem :: TEX_3:37

    

     Th37: for X1,X2 be SubSpace of X st (X1,X2) constitute_a_decomposition holds X1 is everywhere_dense iff X2 is nowhere_dense

    proof

      let X1,X2 be SubSpace of X;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) constitute_a_decomposition ;

      thus X1 is everywhere_dense implies X2 is nowhere_dense

      proof

        assume

         A2: for A1 be Subset of X st A1 = the carrier of X1 holds A1 is everywhere_dense;

        now

          let A2 be Subset of X;

          assume A2 = the carrier of X2;

          then

           A3: (A1,A2) constitute_a_decomposition by A1;

          A1 is everywhere_dense by A2;

          hence A2 is nowhere_dense by A3, Th4;

        end;

        hence thesis;

      end;

      assume

       A4: for A2 be Subset of X st A2 = the carrier of X2 holds A2 is nowhere_dense;

      now

        let A1 be Subset of X;

        assume A1 = the carrier of X1;

        then

         A5: (A1,A2) constitute_a_decomposition by A1;

        A2 is nowhere_dense by A4;

        hence A1 is everywhere_dense by A5, Th4;

      end;

      hence thesis;

    end;

    theorem :: TEX_3:38

    for X1,X2 be non empty SubSpace of X st (X1,X2) constitute_a_decomposition holds X1 is nowhere_dense iff X2 is everywhere_dense by Th37;

    theorem :: TEX_3:39

    

     Th39: for X0 be SubSpace of X st X0 is nowhere_dense holds for A be Subset of X st A c= the carrier of X0 holds A is nowhere_dense

    proof

      let X0 be SubSpace of X;

      reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

      assume X0 is nowhere_dense;

      then

       A1: C is nowhere_dense;

      let A be Subset of X;

      assume A c= the carrier of X0;

      hence thesis by A1, TOPS_3: 26;

    end;

    theorem :: TEX_3:40

    

     Th40: for X1,X2 be SubSpace of X st X1 is nowhere_dense holds X2 is SubSpace of X1 implies X2 is nowhere_dense by TSEP_1: 4, Th39;

    registration

      let X be non empty TopSpace;

      cluster boundary closed -> nowhere_dense for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        assume

         A1: X0 is boundary closed;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A is boundary & A is closed by A1, TSEP_1: 11;

          hence A is nowhere_dense;

        end;

        hence thesis;

      end;

      cluster boundary non nowhere_dense -> non closed for SubSpace of X;

      coherence ;

      cluster closed non nowhere_dense -> non boundary for SubSpace of X;

      coherence ;

    end

    theorem :: TEX_3:41

    

     Th41: for A0 be non empty Subset of X st A0 is boundary closed holds ex X0 be closed strict non empty SubSpace of X st X0 is boundary & A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume

       A2: A0 is boundary closed;

      then

      reconsider Y0 = X0 as closed strict non empty SubSpace of X by A1, TSEP_1: 11;

      take Y0;

      thus thesis by A2, A1;

    end;

    theorem :: TEX_3:42

    for X0 be non empty SubSpace of X holds X0 is nowhere_dense iff ex X1 be closed strict non empty SubSpace of X st X1 is boundary & X0 is SubSpace of X1

    proof

      let X0 be non empty SubSpace of X;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      thus X0 is nowhere_dense implies ex X1 be closed strict non empty SubSpace of X st X1 is boundary & X0 is SubSpace of X1

      proof

        assume X0 is nowhere_dense;

        then A is nowhere_dense;

        then

        consider C be Subset of X such that

         A1: A c= C and

         A2: C is closed & C is boundary by TOPS_3: 27;

        C is non empty by A1, XBOOLE_1: 3;

        then

        consider X1 be closed strict non empty SubSpace of X such that

         A3: X1 is boundary & C = the carrier of X1 by A2, Th41;

        take X1;

        thus thesis by A1, A3, TSEP_1: 4;

      end;

      given X1 be closed strict non empty SubSpace of X such that

       A4: X1 is boundary & X0 is SubSpace of X1;

      reconsider C = the carrier of X1 as Subset of X by TSEP_1: 1;

      now

        take C;

        thus A c= C & C is boundary & C is closed by A4, TSEP_1: 4, TSEP_1: 11;

      end;

      then for A be Subset of X st A = the carrier of X0 holds A is nowhere_dense by TOPS_3: 27;

      hence thesis;

    end;

    reserve X1,X2 for non empty SubSpace of X;

    theorem :: TEX_3:43

    (X1 is boundary or X2 is boundary) & X1 meets X2 implies (X1 meet X2) is boundary

    proof

      assume

       A1: X1 is boundary or X2 is boundary;

      assume

       A2: X1 meets X2;

      hereby

        per cases by A1;

          suppose

           A3: X1 is boundary;

          (X1 meet X2) is SubSpace of X1 by A2, TSEP_1: 27;

          hence thesis by A3, Th34;

        end;

          suppose

           A4: X2 is boundary;

          (X1 meet X2) is SubSpace of X2 by A2, TSEP_1: 27;

          hence thesis by A4, Th34;

        end;

      end;

    end;

    theorem :: TEX_3:44

    X1 is nowhere_dense & X2 is nowhere_dense implies (X1 union X2) is nowhere_dense

    proof

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume X1 is nowhere_dense & X2 is nowhere_dense;

      then A1 is nowhere_dense & A2 is nowhere_dense;

      then (A1 \/ A2) is nowhere_dense by TOPS_1: 53;

      then for A be Subset of X st A = the carrier of (X1 union X2) holds A is nowhere_dense by TSEP_1:def 2;

      hence thesis;

    end;

    theorem :: TEX_3:45

    X1 is nowhere_dense & X2 is boundary or X1 is boundary & X2 is nowhere_dense implies (X1 union X2) is boundary

    proof

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume X1 is nowhere_dense & X2 is boundary or X1 is boundary & X2 is nowhere_dense;

      then A1 is nowhere_dense & A2 is boundary or A1 is boundary & A2 is nowhere_dense;

      then (A1 \/ A2) is boundary by TOPS_3: 30;

      then for A be Subset of X st A = the carrier of (X1 union X2) holds A is boundary by TSEP_1:def 2;

      hence thesis;

    end;

    theorem :: TEX_3:46

    (X1 is nowhere_dense or X2 is nowhere_dense) & X1 meets X2 implies (X1 meet X2) is nowhere_dense

    proof

      assume

       A1: X1 is nowhere_dense or X2 is nowhere_dense;

      assume

       A2: X1 meets X2;

      hereby

        per cases by A1;

          suppose

           A3: X1 is nowhere_dense;

          (X1 meet X2) is SubSpace of X1 by A2, TSEP_1: 27;

          hence thesis by A3, Th40;

        end;

          suppose

           A4: X2 is nowhere_dense;

          (X1 meet X2) is SubSpace of X2 by A2, TSEP_1: 27;

          hence thesis by A4, Th40;

        end;

      end;

    end;

    begin

    theorem :: TEX_3:47

    for X be non empty TopSpace holds (for X0 be SubSpace of X holds X0 is non boundary) implies X is discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for X0 be SubSpace of X holds X0 is non boundary;

      now

        let A be non empty Subset of X;

        consider X0 be strict non empty SubSpace of X such that

         A2: A = the carrier of X0 by TSEP_1: 10;

        X0 is non boundary by A1;

        hence not A is boundary by A2;

      end;

      hence thesis by TEX_1:def 5;

    end;

    theorem :: TEX_3:48

    for X be non trivial TopSpace holds (for X0 be proper SubSpace of X holds X0 is non dense) implies X is discrete

    proof

      let X be non trivial TopSpace;

      assume

       A1: for X0 be proper SubSpace of X holds X0 is non dense;

      now

        let A be Subset of X;

        assume

         A2: A <> the carrier of X;

        now

          per cases ;

            suppose A is empty;

            hence not A is dense by TOPS_3: 17;

          end;

            suppose A is non empty;

            then

            consider X0 be strict non empty SubSpace of X such that

             A3: A = the carrier of X0 by TSEP_1: 10;

            A is proper by A2, SUBSET_1:def 6;

            then

            reconsider X0 as proper strict SubSpace of X by A3, TEX_2: 8;

            X0 is non dense by A1;

            hence not A is dense by A3;

          end;

        end;

        hence not A is dense;

      end;

      hence thesis by TEX_1: 31;

    end;

    registration

      let X be discrete non empty TopSpace;

      cluster -> non boundary for non empty SubSpace of X;

      coherence ;

      cluster proper -> non dense for SubSpace of X;

      coherence ;

      cluster dense -> non proper for SubSpace of X;

      coherence ;

    end

    registration

      let X be discrete non empty TopSpace;

      cluster non boundary strict non empty for SubSpace of X;

      existence

      proof

        set X0 = the strict non empty SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    registration

      let X be discrete non trivial TopSpace;

      cluster non dense strict for SubSpace of X;

      existence

      proof

        set X0 = the proper strict SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    theorem :: TEX_3:49

    for X be non empty TopSpace holds (ex X0 be non empty SubSpace of X st X0 is boundary) implies X is non discrete;

    theorem :: TEX_3:50

    for X be non empty TopSpace holds (ex X0 be non empty SubSpace of X st X0 is dense proper) implies X is non discrete;

    registration

      let X be non discrete non empty TopSpace;

      cluster boundary strict non empty for SubSpace of X;

      existence

      proof

        consider A0 be non empty Subset of X such that

         A1: A0 is boundary by TEX_1:def 5;

        consider X0 be strict non empty SubSpace of X such that

         A2: A0 = the carrier of X0 by TSEP_1: 10;

        take X0;

        for A be Subset of X st A = the carrier of X0 holds A is boundary by A1, A2;

        hence thesis;

      end;

      cluster dense proper strict non empty for SubSpace of X;

      existence

      proof

        consider A0 be Subset of X such that

         A3: A0 <> the carrier of X and

         A4: A0 is dense by TEX_1: 31;

        A0 is non empty by A4, TOPS_3: 17;

        then

        consider X0 be dense strict non empty SubSpace of X such that

         A5: A0 = the carrier of X0 by A4, Th10;

        take X0;

        A0 is proper by A3, SUBSET_1:def 6;

        hence thesis by A5, TEX_2: 8;

      end;

    end

    reserve X for non discrete non empty TopSpace;

    theorem :: TEX_3:51

    for A0 be non empty Subset of X st A0 is boundary holds ex X0 be boundary strict SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      assume A0 is boundary;

      then ex X0 be strict SubSpace of X st X0 is boundary & A0 = the carrier of X0 by Th30;

      hence thesis;

    end;

    theorem :: TEX_3:52

    for A0 be non empty proper Subset of X st A0 is dense holds ex X0 be dense proper strict SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty proper Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume A0 is dense;

      then

      reconsider X0 as dense proper strict SubSpace of X by A1, Th9, TEX_2: 8;

      take X0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:53

    for X1 be boundary non empty SubSpace of X holds ex X2 be dense proper strict non empty SubSpace of X st (X1,X2) constitute_a_decomposition

    proof

      let X1 be boundary non empty SubSpace of X;

      consider X2 be proper strict non empty SubSpace of X such that

       A1: (X1,X2) constitute_a_decomposition by Th8;

      reconsider X2 as dense proper strict non empty SubSpace of X by A1, Th31;

      take X2;

      thus thesis by A1;

    end;

    theorem :: TEX_3:54

    for X1 be dense proper non empty SubSpace of X holds ex X2 be boundary strict non empty SubSpace of X st (X1,X2) constitute_a_decomposition

    proof

      let X1 be dense proper non empty SubSpace of X;

      consider X2 be proper strict non empty SubSpace of X such that

       A1: (X1,X2) constitute_a_decomposition by Th8;

      reconsider X2 as boundary strict non empty SubSpace of X by A1, Th31;

      take X2;

      thus thesis by A1;

    end;

    theorem :: TEX_3:55

    for Y1,Y2 be non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X

    proof

      let X1,X2 be non empty TopSpace;

      assume

       A1: X2 = the TopStruct of X1;

      thus X1 is boundary SubSpace of X implies X2 is boundary SubSpace of X

      proof

        assume

         A2: X1 is boundary SubSpace of X;

        then

        reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1: 7;

        for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is boundary by A1, A2, Def3;

        hence thesis by Def3;

      end;

      assume

       A3: X2 is boundary SubSpace of X;

      then

      reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1: 7;

      for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is boundary by A1, A3, Def3;

      hence thesis by Def3;

    end;

    begin

    theorem :: TEX_3:56

    for X be non empty TopSpace holds (for X0 be SubSpace of X holds X0 is non nowhere_dense) implies X is almost_discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for X0 be SubSpace of X holds X0 is non nowhere_dense;

      now

        let A be non empty Subset of X;

        consider X0 be strict non empty SubSpace of X such that

         A2: A = the carrier of X0 by TSEP_1: 10;

        X0 is non nowhere_dense by A1;

        hence not A is nowhere_dense by A2;

      end;

      hence thesis by TEX_1:def 6;

    end;

    theorem :: TEX_3:57

    for X be non trivial TopSpace holds (for X0 be proper SubSpace of X holds X0 is non everywhere_dense) implies X is almost_discrete

    proof

      let X be non trivial TopSpace;

      assume

       A1: for X0 be proper SubSpace of X holds X0 is non everywhere_dense;

      now

        let A be Subset of X;

        assume

         A2: A <> the carrier of X;

        now

          per cases ;

            suppose A is empty;

            hence not A is everywhere_dense by TOPS_3: 34;

          end;

            suppose A is non empty;

            then

            consider X0 be strict non empty SubSpace of X such that

             A3: A = the carrier of X0 by TSEP_1: 10;

            A is proper by A2, SUBSET_1:def 6;

            then

            reconsider X0 as proper strict SubSpace of X by A3, TEX_2: 8;

            X0 is non everywhere_dense by A1;

            hence not A is everywhere_dense by A3;

          end;

        end;

        hence not A is everywhere_dense;

      end;

      hence thesis by TEX_1: 32;

    end;

    registration

      let X be almost_discrete non empty TopSpace;

      cluster -> non nowhere_dense for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X;

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

         not A is nowhere_dense by TEX_1:def 6;

        hence thesis;

      end;

      cluster proper -> non everywhere_dense for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

        assume X0 is proper;

        then A is proper by TEX_2: 8;

        then A <> the carrier of X by SUBSET_1:def 6;

        then not A is everywhere_dense by TEX_1: 32;

        hence thesis;

      end;

      cluster everywhere_dense -> non proper for SubSpace of X;

      coherence ;

      cluster boundary -> non closed for non empty SubSpace of X;

      coherence ;

      cluster closed -> non boundary for non empty SubSpace of X;

      coherence ;

      cluster dense proper -> non open for SubSpace of X;

      coherence ;

      cluster dense open -> non proper for SubSpace of X;

      coherence ;

      cluster open proper -> non dense for SubSpace of X;

      coherence ;

    end

    registration

      let X be almost_discrete non empty TopSpace;

      cluster non nowhere_dense strict non empty for SubSpace of X;

      existence

      proof

        set X0 = the strict non empty SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    registration

      let X be almost_discrete non trivial TopSpace;

      cluster non everywhere_dense strict for SubSpace of X;

      existence

      proof

        set X0 = the proper strict SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    theorem :: TEX_3:58

    for X be non empty TopSpace holds (ex X0 be non empty SubSpace of X st X0 is nowhere_dense) implies X is non almost_discrete;

    theorem :: TEX_3:59

    for X be non empty TopSpace holds (ex X0 be non empty SubSpace of X st X0 is boundary closed) implies X is non almost_discrete;

    theorem :: TEX_3:60

    for X be non empty TopSpace holds (ex X0 be non empty SubSpace of X st X0 is everywhere_dense proper) implies X is non almost_discrete;

    theorem :: TEX_3:61

    for X be non empty TopSpace holds (ex X0 be non empty SubSpace of X st X0 is dense open proper) implies X is non almost_discrete;

    registration

      let X be non almost_discrete non empty TopSpace;

      cluster nowhere_dense strict non empty for SubSpace of X;

      existence

      proof

        consider A0 be non empty Subset of X such that

         A1: A0 is nowhere_dense by TEX_1:def 6;

        consider X0 be strict non empty SubSpace of X such that

         A2: A0 = the carrier of X0 by TSEP_1: 10;

        take X0;

        for A be Subset of X st A = the carrier of X0 holds A is nowhere_dense by A1, A2;

        hence thesis;

      end;

      cluster everywhere_dense proper strict non empty for SubSpace of X;

      existence

      proof

        consider A0 be Subset of X such that

         A3: A0 <> the carrier of X and

         A4: A0 is everywhere_dense by TEX_1: 32;

        A0 is non empty by A4, TOPS_3: 34;

        then

        consider X0 be everywhere_dense strict non empty SubSpace of X such that

         A5: A0 = the carrier of X0 by A4, Th17;

        take X0;

        A0 is proper by A3, SUBSET_1:def 6;

        hence thesis by A5, TEX_2: 8;

      end;

    end

    reserve X for non almost_discrete non empty TopSpace;

    theorem :: TEX_3:62

    

     Th62: for A0 be non empty Subset of X st A0 is nowhere_dense holds ex X0 be nowhere_dense strict non empty SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume A0 is nowhere_dense;

      then

      reconsider Y0 = X0 as nowhere_dense strict non empty SubSpace of X by A1, Th35;

      take Y0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:63

    for A0 be non empty proper Subset of X st A0 is everywhere_dense holds ex X0 be everywhere_dense proper strict SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty proper Subset of X;

      assume A0 is everywhere_dense;

      then

      consider X0 be everywhere_dense strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by Th17;

      reconsider X0 as everywhere_dense proper strict SubSpace of X by A1, TEX_2: 8;

      take X0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:64

    for X1 be nowhere_dense non empty SubSpace of X holds ex X2 be everywhere_dense proper strict non empty SubSpace of X st (X1,X2) constitute_a_decomposition

    proof

      let X1 be nowhere_dense non empty SubSpace of X;

      consider X2 be proper strict non empty SubSpace of X such that

       A1: (X1,X2) constitute_a_decomposition by Th8;

      reconsider X2 as everywhere_dense proper strict non empty SubSpace of X by A1, Th37;

      take X2;

      thus thesis by A1;

    end;

    theorem :: TEX_3:65

    for X1 be everywhere_dense proper non empty SubSpace of X holds ex X2 be nowhere_dense strict non empty SubSpace of X st (X1,X2) constitute_a_decomposition

    proof

      let X1 be everywhere_dense proper non empty SubSpace of X;

      consider X2 be proper strict non empty SubSpace of X such that

       A1: (X1,X2) constitute_a_decomposition by Th8;

      reconsider X2 as nowhere_dense strict non empty SubSpace of X by A1, Th37;

      take X2;

      thus thesis by A1;

    end;

    theorem :: TEX_3:66

    for Y1,Y2 be non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X

    proof

      let X1,X2 be non empty TopSpace;

      assume

       A1: X2 = the TopStruct of X1;

      thus X1 is nowhere_dense SubSpace of X implies X2 is nowhere_dense SubSpace of X

      proof

        assume

         A2: X1 is nowhere_dense SubSpace of X;

        then

        reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1: 7;

        for A2 be Subset of X st A2 = the carrier of Y2 holds A2 is nowhere_dense by A1, A2, Def4;

        hence thesis by Def4;

      end;

      assume

       A3: X2 is nowhere_dense SubSpace of X;

      then

      reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1: 7;

      for A1 be Subset of X st A1 = the carrier of Y1 holds A1 is nowhere_dense by A1, A3, Def4;

      hence thesis by Def4;

    end;

    registration

      let X be non almost_discrete non empty TopSpace;

      cluster boundary closed strict non empty for SubSpace of X;

      existence

      proof

        consider A be non empty Subset of X such that

         A1: A is nowhere_dense by TEX_1:def 6;

        consider C be Subset of X such that

         A2: A c= C and

         A3: C is closed & C is boundary by A1, TOPS_3: 27;

        C is non empty by A2, XBOOLE_1: 3;

        then

        consider X0 be strict non empty SubSpace of X such that

         A4: C = the carrier of X0 by TSEP_1: 10;

        take X0;

        (for C be Subset of X st C = the carrier of X0 holds C is boundary) & for C be Subset of X st C = the carrier of X0 holds C is closed by A3, A4;

        hence thesis by BORSUK_1:def 11;

      end;

      cluster dense open proper strict non empty for SubSpace of X;

      existence

      proof

        consider A0 be Subset of X such that

         A5: A0 <> the carrier of X and

         A6: A0 is dense open by TEX_1: 34;

        A0 is non empty by A6, TOPS_3: 17;

        then

        consider X0 be dense open strict non empty SubSpace of X such that

         A7: A0 = the carrier of X0 by A6, Th23;

        take X0;

        A0 is proper by A5, SUBSET_1:def 6;

        hence thesis by A7, TEX_2: 8;

      end;

    end

    theorem :: TEX_3:67

    

     Th67: for A0 be non empty Subset of X st A0 is boundary closed holds ex X0 be boundary closed strict non empty SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume A0 is boundary closed;

      then

      reconsider Y0 = X0 as boundary closed strict non empty SubSpace of X by A1, Th29, TSEP_1: 11;

      take Y0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:68

    for A0 be non empty proper Subset of X st A0 is dense open holds ex X0 be dense open proper strict SubSpace of X st A0 = the carrier of X0

    proof

      let A0 be non empty proper Subset of X;

      assume A0 is dense open;

      then

      consider X0 be dense open strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by Th23;

      reconsider X0 as dense open proper strict SubSpace of X by A1, TEX_2: 8;

      take X0;

      thus thesis by A1;

    end;

    theorem :: TEX_3:69

    for X1 be boundary closed non empty SubSpace of X holds ex X2 be dense open proper strict non empty SubSpace of X st (X1,X2) constitute_a_decomposition

    proof

      let X1 be boundary closed non empty SubSpace of X;

      consider X2 be proper strict non empty SubSpace of X such that

       A1: (X1,X2) constitute_a_decomposition by Th8;

      reconsider X2 as dense open proper strict non empty SubSpace of X by A1, Th31, TSEP_2: 34;

      take X2;

      thus thesis by A1;

    end;

    theorem :: TEX_3:70

    for X1 be dense open proper non empty SubSpace of X holds ex X2 be boundary closed strict non empty SubSpace of X st (X1,X2) constitute_a_decomposition

    proof

      let X1 be dense open proper non empty SubSpace of X;

      consider X2 be proper strict non empty SubSpace of X such that

       A1: (X1,X2) constitute_a_decomposition by Th8;

      reconsider X2 as boundary closed strict non empty SubSpace of X by A1, Th31, TSEP_2: 33;

      take X2;

      thus thesis by A1;

    end;

    theorem :: TEX_3:71

    for X0 be non empty SubSpace of X holds X0 is nowhere_dense iff ex X1 be boundary closed strict non empty SubSpace of X st X0 is SubSpace of X1

    proof

      let X0 be non empty SubSpace of X;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      thus X0 is nowhere_dense implies ex X1 be boundary closed strict non empty SubSpace of X st X0 is SubSpace of X1

      proof

        assume X0 is nowhere_dense;

        then A is nowhere_dense;

        then

        consider C be Subset of X such that

         A1: A c= C and

         A2: C is closed & C is boundary by TOPS_3: 27;

        C is non empty by A1, XBOOLE_1: 3;

        then

        consider X1 be boundary closed strict non empty SubSpace of X such that

         A3: C = the carrier of X1 by A2, Th67;

        take X1;

        thus thesis by A1, A3, TSEP_1: 4;

      end;

      given X1 be boundary closed strict non empty SubSpace of X such that

       A4: X0 is SubSpace of X1;

      reconsider C = the carrier of X1 as Subset of X by TSEP_1: 1;

      now

        take C;

        thus A c= C & C is boundary & C is closed by A4, Def3, TSEP_1: 4, TSEP_1: 11;

      end;

      then for A be Subset of X st A = the carrier of X0 holds A is nowhere_dense by TOPS_3: 27;

      hence thesis;

    end;

    theorem :: TEX_3:72

    for X0 be nowhere_dense non empty SubSpace of X holds X0 is boundary closed or ex X1 be everywhere_dense proper strict non empty SubSpace of X, X2 be boundary closed strict non empty SubSpace of X st (X1 meet X2) = the TopStruct of X0 & (X1 union X2) = the TopStruct of X

    proof

      let X0 be nowhere_dense non empty SubSpace of X;

      reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1: 1;

      

       A1: X is SubSpace of X by TSEP_1: 2;

      D is nowhere_dense by Th35;

      then

      consider C,B be Subset of X such that

       A2: C is closed boundary and

       A3: B is everywhere_dense and

       A4: (C /\ B) = D and

       A5: (C \/ B) = the carrier of X by TOPS_3: 51;

      B <> {} by A4;

      then

      consider X1 be everywhere_dense strict non empty SubSpace of X such that

       A6: B = the carrier of X1 by A3, Th17;

      assume

       A7: X0 is non boundary or X0 is non closed;

      now

        assume B is non proper;

        then B = the carrier of X by SUBSET_1:def 6;

        then D = C by A4, XBOOLE_1: 28;

        hence contradiction by A7, A2, TSEP_1: 11;

      end;

      then

      reconsider X1 as everywhere_dense proper strict non empty SubSpace of X by A6, TEX_2: 8;

      C <> {} by A4;

      then

      consider X2 be boundary closed strict non empty SubSpace of X such that

       A8: C = the carrier of X2 by A2, Th67;

      take X1, X2;

      C meets B by A4, XBOOLE_0:def 7;

      then X1 meets X2 by A8, A6, TSEP_1:def 3;

      then the carrier of (X1 meet X2) = D by A4, A8, A6, TSEP_1:def 4;

      hence (X1 meet X2) = the TopStruct of X0 by TSEP_1: 5;

      the carrier of (X1 union X2) = the carrier of X by A5, A8, A6, TSEP_1:def 2;

      hence thesis by A1, TSEP_1: 5;

    end;

    theorem :: TEX_3:73

    for X0 be everywhere_dense non empty SubSpace of X holds X0 is dense open or ex X1 be dense open proper strict non empty SubSpace of X, X2 be nowhere_dense strict non empty SubSpace of X st X1 misses X2 & (X1 union X2) = the TopStruct of X0

    proof

      let X0 be everywhere_dense non empty SubSpace of X;

      reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1: 1;

      D is everywhere_dense by Th16;

      then

      consider C,B be Subset of X such that

       A1: C is open dense and

       A2: B is nowhere_dense and

       A3: (C \/ B) = D and

       A4: C misses B by TOPS_3: 49;

      C <> {} by A1, TOPS_3: 17;

      then

      consider X1 be dense open strict non empty SubSpace of X such that

       A5: C = the carrier of X1 by A1, Th23;

      assume

       A6: X0 is non dense or X0 is non open;

      now

        assume C is non proper;

        then

         A7: C = the carrier of X by SUBSET_1:def 6;

        C c= D by A3, XBOOLE_1: 7;

        then D = ( [#] X) by A7, XBOOLE_0:def 10;

        then D is dense open;

        hence contradiction by A6, TSEP_1: 16;

      end;

      then

      reconsider X1 as dense open proper strict non empty SubSpace of X by A5, TEX_2: 8;

      now

        per cases by A6;

          suppose

           A8: X0 is non dense;

          assume B = {} ;

          thus contradiction by A8;

        end;

          suppose

           A9: X0 is non open;

          assume B = {} ;

          hence contradiction by A1, A3, A9, TSEP_1: 16;

        end;

      end;

      then

      consider X2 be nowhere_dense strict non empty SubSpace of X such that

       A10: B = the carrier of X2 by A2, Th62;

      take X1, X2;

      thus X1 misses X2 by A4, A5, A10, TSEP_1:def 3;

      the carrier of (X1 union X2) = the carrier of X0 by A3, A5, A10, TSEP_1:def 2;

      hence thesis by TSEP_1: 5;

    end;

    theorem :: TEX_3:74

    for X0 be nowhere_dense non empty SubSpace of X holds ex X1 be dense open proper strict non empty SubSpace of X, X2 be boundary closed strict non empty SubSpace of X st (X1,X2) constitute_a_decomposition & X0 is SubSpace of X2

    proof

      let X0 be nowhere_dense non empty SubSpace of X;

      reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1: 1;

      D is nowhere_dense by Th35;

      then

      consider C,B be Subset of X such that

       A1: C is closed boundary and

       A2: B is open dense and

       A3: (C /\ (D \/ B)) = D and

       A4: C misses B and

       A5: (C \/ B) = the carrier of X by TOPS_3: 52;

      B <> {} by A2, TOPS_3: 17;

      then

      consider X1 be dense open strict non empty SubSpace of X such that

       A6: B = the carrier of X1 by A2, Th23;

      

       A7: C <> {} by A3;

      then

      consider X2 be boundary closed strict non empty SubSpace of X such that

       A8: C = the carrier of X2 by A1, Th67;

      

       A9: (C /\ B) = {} by A4, XBOOLE_0:def 7;

      now

        assume B is non proper;

        then B = the carrier of X by SUBSET_1:def 6;

        hence contradiction by A7, A9, XBOOLE_1: 28;

      end;

      then

      reconsider X1 as dense open proper strict non empty SubSpace of X by A6, TEX_2: 8;

      take X1, X2;

      for P,Q be Subset of X st P = the carrier of X1 & Q = the carrier of X2 holds (P,Q) constitute_a_decomposition by A4, A5, A6, A8;

      hence (X1,X2) constitute_a_decomposition ;

      D c= C by A3, XBOOLE_1: 17;

      hence thesis by A8, TSEP_1: 4;

    end;

    theorem :: TEX_3:75

    for X0 be everywhere_dense proper SubSpace of X holds ex X1 be dense open proper strict SubSpace of X, X2 be boundary closed strict SubSpace of X st (X1,X2) constitute_a_decomposition & X1 is SubSpace of X0

    proof

      let X0 be everywhere_dense proper SubSpace of X;

      reconsider D = the carrier of X0 as Subset of X by TSEP_1: 1;

      D is everywhere_dense by Th16;

      then

      consider C,B be Subset of X such that

       A1: C is open dense and

       A2: B is closed boundary and

       A3: (C \/ (D /\ B)) = D and

       A4: C misses B and

       A5: (C \/ B) = the carrier of X by TOPS_3: 50;

      C <> {} by A1, TOPS_3: 17;

      then

      consider X1 be dense open strict non empty SubSpace of X such that

       A6: C = the carrier of X1 by A1, Th23;

       A7:

      now

        assume C is non proper;

        then C = the carrier of X by SUBSET_1:def 6;

        then the carrier of X c= D by A3, XBOOLE_1: 7;

        then D = the carrier of X by XBOOLE_0:def 10;

        then D is non proper by SUBSET_1:def 6;

        hence contradiction by TEX_2: 8;

      end;

      then B is non empty by A5, SUBSET_1:def 6;

      then

      consider X2 be boundary closed strict non empty SubSpace of X such that

       A8: B = the carrier of X2 by A2, Th67;

      reconsider X1 as dense open proper strict SubSpace of X by A6, A7, TEX_2: 8;

      take X1, X2;

      for P,Q be Subset of X st P = the carrier of X1 & Q = the carrier of X2 holds (P,Q) constitute_a_decomposition by A4, A5, A6, A8;

      hence (X1,X2) constitute_a_decomposition ;

      C c= D by A3, XBOOLE_1: 7;

      hence thesis by A6, TSEP_1: 4;

    end;