tops_1.miz



    begin

    reserve TS for 1-sorted,

K,Q for Subset of TS;

    theorem :: TOPS_1:1

    (K ` ) = (Q ` ) implies K = Q by SUBSET_1: 42;

    reserve TS for TopSpace,

GX for TopStruct,

x for set,

P,Q for Subset of TS,

K,L for Subset of TS,

R,S for Subset of GX,

T,W for Subset of GX;

    theorem :: TOPS_1:2

    

     Th2: ( Cl ( [#] GX)) = ( [#] GX) by PRE_TOPC: 18;

    registration

      let T be TopSpace, P be Subset of T;

      cluster ( Cl P) -> closed;

      coherence

      proof

        ( Cl ( Cl P)) = ( Cl P);

        hence thesis by PRE_TOPC: 22;

      end;

    end

    theorem :: TOPS_1:3

    

     Th3: R is closed iff (R ` ) is open

    proof

      R is closed iff (( [#] GX) \ R) is open by PRE_TOPC:def 3;

      hence thesis;

    end;

    registration

      let T be TopSpace, R be closed Subset of T;

      cluster (R ` ) -> open;

      coherence by Th3;

    end

    theorem :: TOPS_1:4

    

     Th4: R is open iff (R ` ) is closed

    proof

      (R ` ) is closed iff ((R ` ) ` ) is open by Th3;

      hence thesis;

    end;

    registration

      let T be TopSpace;

      cluster open for Subset of T;

      existence

      proof

        take (( {} T) ` );

        thus thesis;

      end;

    end

    registration

      let T be TopSpace, R be open Subset of T;

      cluster (R ` ) -> closed;

      coherence by Th4;

    end

    theorem :: TOPS_1:5

    S is closed & T c= S implies ( Cl T) c= S

    proof

      assume that

       A1: S is closed and

       A2: T c= S;

      ( Cl S) = S by A1, PRE_TOPC: 22;

      hence thesis by A2, PRE_TOPC: 19;

    end;

    theorem :: TOPS_1:6

    

     Th6: (( Cl K) \ ( Cl L)) c= ( Cl (K \ L))

    proof

      let x be object;

      (( Cl K) \/ ( Cl L)) = ( Cl (K \/ L)) by PRE_TOPC: 20

      .= ( Cl ((K \ L) \/ L)) by XBOOLE_1: 39

      .= (( Cl (K \ L)) \/ ( Cl L)) by PRE_TOPC: 20;

      then

       A1: x in (( Cl K) \/ ( Cl L)) iff x in ( Cl (K \ L)) or x in ( Cl L) by XBOOLE_0:def 3;

      assume

       A2: x in (( Cl K) \ ( Cl L));

      then x in ( Cl K) by XBOOLE_0:def 5;

      hence thesis by A2, A1, XBOOLE_0:def 3, XBOOLE_0:def 5;

    end;

    theorem :: TOPS_1:7

    

     Th7: R is closed & S is closed implies ( Cl (R /\ S)) = (( Cl R) /\ ( Cl S))

    proof

      assume that

       A1: R is closed and

       A2: S is closed;

      

       A3: S = ( Cl S) by A2, PRE_TOPC: 22;

      

       A4: ( Cl (R /\ S)) c= (( Cl R) /\ ( Cl S)) by PRE_TOPC: 21;

      R = ( Cl R) by A1, PRE_TOPC: 22;

      then (( Cl R) /\ ( Cl S)) c= ( Cl (R /\ S)) by A3, PRE_TOPC: 18;

      hence thesis by A4;

    end;

    registration

      let TS;

      let P,Q be closed Subset of TS;

      cluster (P /\ Q) -> closed;

      coherence

      proof

        

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

        P = ( Cl P) by PRE_TOPC: 22;

        then ( Cl (P /\ Q)) = (P /\ Q) by A1, Th7;

        hence thesis;

      end;

      cluster (P \/ Q) -> closed;

      coherence

      proof

        

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

        P = ( Cl P) by PRE_TOPC: 22;

        then ( Cl (P \/ Q)) = (P \/ Q) by A2, PRE_TOPC: 20;

        hence thesis;

      end;

    end

    theorem :: TOPS_1:8

    P is closed & Q is closed implies (P /\ Q) is closed;

    theorem :: TOPS_1:9

    P is closed & Q is closed implies (P \/ Q) is closed;

    registration

      let TS;

      let P,Q be open Subset of TS;

      cluster (P /\ Q) -> open;

      coherence

      proof

        ((P ` ) \/ (Q ` )) = ((P /\ Q) ` ) by XBOOLE_1: 54;

        hence thesis by Th4;

      end;

      cluster (P \/ Q) -> open;

      coherence

      proof

        ((P ` ) /\ (Q ` )) = ((P \/ Q) ` ) by XBOOLE_1: 53;

        hence thesis by Th4;

      end;

    end

    theorem :: TOPS_1:10

    P is open & Q is open implies (P \/ Q) is open;

    theorem :: TOPS_1:11

    P is open & Q is open implies (P /\ Q) is open;

    theorem :: TOPS_1:12

    

     Th12: for GX be non empty TopSpace, R be Subset of GX, p be Point of GX holds p in ( Cl R) iff for T be Subset of GX st T is open & p in T holds R meets T

    proof

      let GX be non empty TopSpace, R be Subset of GX, p be Point of GX;

      hereby

        assume

         A1: p in ( Cl R);

        given T be Subset of GX such that

         A2: T is open and

         A3: p in T and

         A4: R misses T;

        

         A5: ((R ` ) \/ (T ` )) = ((R /\ T) ` ) by XBOOLE_1: 54;

        

         A6: (R /\ T) = ( {} GX) by A4;

        

         A7: R c= (T ` )

        proof

          let x be object;

          assume

           A8: x in R;

          then x in (R ` ) or x in (T ` ) by A5, A6, XBOOLE_0:def 3;

          hence thesis by A8, XBOOLE_0:def 5;

        end;

        ( Cl (T ` )) = (T ` ) by A2, PRE_TOPC: 22;

        then ( Cl R) c= (T ` ) by A7, PRE_TOPC: 19;

        hence contradiction by A1, A3, XBOOLE_0:def 5;

      end;

      assume

       A9: for T be Subset of GX st T is open & p in T holds R meets T;

      assume not p in ( Cl R);

      then p in (( Cl R) ` ) by SUBSET_1: 29;

      then

       A10: R meets (( Cl R) ` ) by A9;

      R misses (R ` ) by XBOOLE_1: 79;

      then

       A11: (R /\ (R ` )) = {} ;

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

      then (( Cl R) ` ) c= (R ` ) by SUBSET_1: 12;

      then (R /\ (( Cl R) ` )) = {} by A11, XBOOLE_1: 3, XBOOLE_1: 26;

      hence contradiction by A10;

    end;

    theorem :: TOPS_1:13

    

     Th13: Q is open implies (Q /\ ( Cl K)) c= ( Cl (Q /\ K))

    proof

      assume

       A1: Q is open;

      let x be object;

      assume

       A2: x in (Q /\ ( Cl K));

      then

       A3: x in ( Cl K) by XBOOLE_0:def 4;

      reconsider p99 = x as Point of TS by A2;

      

       A4: TS is non empty by A2;

      

       A5: x in Q by A2, XBOOLE_0:def 4;

      for Q1 be Subset of TS holds Q1 is open implies (p99 in Q1 implies (Q /\ K) meets Q1)

      proof

        let Q1 be Subset of TS;

        assume

         A6: Q1 is open;

        assume p99 in Q1;

        then p99 in (Q1 /\ Q) by A5, XBOOLE_0:def 4;

        then K meets (Q1 /\ Q) by A1, A3, A4, A6, Th12;

        then

         A7: (K /\ (Q1 /\ Q)) <> {} ;

        (K /\ (Q1 /\ Q)) = ((Q /\ K) /\ Q1) by XBOOLE_1: 16;

        hence thesis by A7;

      end;

      hence thesis by A4, Th12;

    end;

    theorem :: TOPS_1:14

    Q is open implies ( Cl (Q /\ ( Cl K))) = ( Cl (Q /\ K))

    proof

      

       A1: ( Cl (Q /\ K)) c= ( Cl (Q /\ ( Cl K)))

      proof

        let x be object;

        assume

         A2: x in ( Cl (Q /\ K));

        then

        reconsider p99 = x as Point of TS;

        

         A3: TS is non empty by A2;

        for Q1 be Subset of TS holds Q1 is open implies (p99 in Q1 implies (Q /\ ( Cl K)) meets Q1)

        proof

          let Q1 be Subset of TS;

          assume

           A4: Q1 is open;

          assume p99 in Q1;

          then (Q /\ K) meets Q1 by A2, A3, A4, Th12;

          then

           A5: ((Q /\ K) /\ Q1) <> {} ;

          (Q /\ K) c= (Q /\ ( Cl K)) by PRE_TOPC: 18, XBOOLE_1: 26;

          then ((Q /\ ( Cl K)) /\ Q1) <> {} by A5, XBOOLE_1: 3, XBOOLE_1: 26;

          hence thesis;

        end;

        hence thesis by A3, Th12;

      end;

      assume Q is open;

      then ( Cl (Q /\ ( Cl K))) c= ( Cl ( Cl (Q /\ K))) by Th13, PRE_TOPC: 19;

      hence thesis by A1;

    end;

    definition

      let GX be TopStruct, R be Subset of GX;

      :: TOPS_1:def1

      func Int R -> Subset of GX equals (( Cl (R ` )) ` );

      coherence ;

      projectivity ;

    end

    theorem :: TOPS_1:15

    

     Th15: ( Int ( [#] TS)) = ( [#] TS)

    proof

      ( Int ( [#] TS)) = (( {} TS) ` ) by PRE_TOPC: 22;

      hence thesis;

    end;

    theorem :: TOPS_1:16

    

     Th16: ( Int T) c= T

    proof

      let x be object;

      assume

       A1: x in ( Int T);

      then

      reconsider x99 = x as Point of GX;

      (T ` ) c= ( Cl (T ` )) by PRE_TOPC: 18;

      then not x99 in (T ` ) by A1, XBOOLE_0:def 5;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: TOPS_1:17

    

     Th17: (( Int K) /\ ( Int L)) = ( Int (K /\ L))

    proof

      (( Int K) /\ ( Int L)) = ((( Cl (K ` )) \/ ( Cl (L ` ))) ` ) by XBOOLE_1: 53

      .= (( Cl ((K ` ) \/ (L ` ))) ` ) by PRE_TOPC: 20

      .= (( Cl ((K /\ L) ` )) ` ) by XBOOLE_1: 54;

      hence thesis;

    end;

    registration

      let GX;

      cluster ( Int ( {} GX)) -> empty;

      coherence

      proof

        ( {} GX) = (( [#] GX) ` ) by XBOOLE_1: 37

        .= (( Cl (( {} GX) ` )) ` ) by Th2;

        hence thesis;

      end;

    end

    theorem :: TOPS_1:18

    ( Int ( {} GX)) = ( {} GX);

    theorem :: TOPS_1:19

    

     Th19: T c= W implies ( Int T) c= ( Int W)

    proof

      assume T c= W;

      then (W ` ) c= (T ` ) by SUBSET_1: 12;

      then ( Cl (W ` )) c= ( Cl (T ` )) by PRE_TOPC: 19;

      hence thesis by SUBSET_1: 12;

    end;

    theorem :: TOPS_1:20

    

     Th20: (( Int T) \/ ( Int W)) c= ( Int (T \/ W))

    proof

      

       A1: ( Cl ((T ` ) /\ (W ` ))) c= (( Cl (T ` )) /\ ( Cl (W ` ))) by PRE_TOPC: 21;

      (( Int T) \/ ( Int W)) = ((( Cl (T ` )) /\ ( Cl (W ` ))) ` ) by XBOOLE_1: 54;

      then (( Int T) \/ ( Int W)) c= (( Cl ((T ` ) /\ (W ` ))) ` ) by A1, SUBSET_1: 12;

      hence thesis by XBOOLE_1: 53;

    end;

    theorem :: TOPS_1:21

    ( Int (K \ L)) c= (( Int K) \ ( Int L))

    proof

      

       A1: ( Int (K \ L)) = (( Cl ((K /\ (L ` )) ` )) ` ) by SUBSET_1: 13

      .= (( Cl ((K ` ) \/ ((L ` ) ` ))) ` ) by XBOOLE_1: 54

      .= ((( Cl (K ` )) \/ ( Cl L)) ` ) by PRE_TOPC: 20

      .= ((( Cl L) ` ) /\ ( Int K)) by XBOOLE_1: 53;

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

      then

       A2: (( Cl L) ` ) c= (L ` ) by SUBSET_1: 12;

      ( Int L) c= L by Th16;

      then (L ` ) c= (( Int L) ` ) by SUBSET_1: 12;

      then (( Cl L) ` ) c= (( Int L) ` ) by A2;

      then ( Int (K \ L)) c= (( Int K) /\ (( Int L) ` )) by A1, XBOOLE_1: 26;

      hence thesis by SUBSET_1: 13;

    end;

    registration

      let T be TopSpace, K be Subset of T;

      cluster ( Int K) -> open;

      coherence ;

    end

    registration

      let T be TopSpace;

      cluster empty -> open for Subset of T;

      coherence

      proof

        let S be Subset of T;

        ( Int ( {} T)) = ( {} T);

        hence thesis;

      end;

      cluster ( [#] T) -> open;

      coherence

      proof

        ( Int ( [#] T)) = ( [#] T) by Th15;

        hence thesis;

      end;

    end

    registration

      let T be TopSpace;

      cluster open closed for Subset of T;

      existence

      proof

        take ( [#] T);

        thus thesis;

      end;

    end

    registration

      let T be non empty TopSpace;

      cluster non empty open closed for Subset of T;

      existence

      proof

        take ( [#] T);

        thus thesis;

      end;

    end

    theorem :: TOPS_1:22

    

     Th22: x in ( Int K) iff ex Q st Q is open & Q c= K & x in Q

    proof

      thus x in ( Int K) implies ex Q st Q is open & Q c= K & x in Q by Th16;

      given Q such that

       A1: Q is open and

       A2: Q c= K and

       A3: x in Q;

      (K ` ) c= (Q ` ) by A2, SUBSET_1: 12;

      then ( Cl (K ` )) c= ( Cl (Q ` )) by PRE_TOPC: 19;

      then ( Cl (K ` )) c= (Q ` ) by A1, PRE_TOPC: 22;

      then ((Q ` ) ` ) c= (( Cl (K ` )) ` ) by SUBSET_1: 12;

      hence thesis by A3;

    end;

    theorem :: TOPS_1:23

    

     Th23: (R is open implies ( Int R) = R) & (( Int P) = P implies P is open)

    proof

      hereby

        assume R is open;

        then (R ` ) is closed by Th4;

        then ( Cl (R ` )) = (R ` ) by PRE_TOPC: 22;

        hence ( Int R) = R;

      end;

      thus thesis;

    end;

    theorem :: TOPS_1:24

    S is open & S c= T implies S c= ( Int T)

    proof

      assume that

       A1: S is open and

       A2: S c= T;

      ( Int S) = S by A1, Th23;

      hence thesis by A2, Th19;

    end;

    theorem :: TOPS_1:25

    P is open iff for x holds x in P iff ex Q st Q is open & Q c= P & x in Q

    proof

      thus P is open implies for x holds x in P iff ex Q st Q is open & Q c= P & x in Q;

      assume

       A1: for x holds x in P iff ex Q st Q is open & Q c= P & x in Q;

      now

        let x be object;

        x in P iff ex Q st Q is open & Q c= P & x in Q by A1;

        hence x in P iff x in ( Int P) by Th22;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPS_1:26

    

     Th26: ( Cl ( Int T)) = ( Cl ( Int ( Cl ( Int T))))

    proof

      ( Int ( Int T)) c= ( Int ( Cl ( Int T))) by Th19, PRE_TOPC: 18;

      then

       A1: ( Cl ( Int T)) c= ( Cl ( Int ( Cl ( Int T)))) by PRE_TOPC: 19;

      ( Cl ( Int ( Cl ( Int T)))) c= ( Cl ( Cl ( Int T))) by Th16, PRE_TOPC: 19;

      hence thesis by A1;

    end;

    theorem :: TOPS_1:27

    R is open implies ( Cl ( Int ( Cl R))) = ( Cl R)

    proof

      assume

       A1: R is open;

      

      then ( Cl ( Int ( Cl R))) = ( Cl ( Int ( Cl ( Int R)))) by Th23

      .= ( Cl ( Int R)) by Th26

      .= ( Cl R) by A1, Th23;

      hence thesis;

    end;

    definition

      let GX be TopStruct, R be Subset of GX;

      :: TOPS_1:def2

      func Fr R -> Subset of GX equals (( Cl R) /\ ( Cl (R ` )));

      coherence ;

    end

    registration

      let T be TopSpace, A be Subset of T;

      cluster ( Fr A) -> closed;

      coherence ;

    end

    theorem :: TOPS_1:28

    

     Th28: for GX be non empty TopSpace, R be Subset of GX, p be Point of GX holds p in ( Fr R) iff for S be Subset of GX st S is open & p in S holds R meets S & (R ` ) meets S

    proof

      let GX be non empty TopSpace, R be Subset of GX, p be Point of GX;

      hereby

        assume

         A1: p in ( Fr R);

        then

         A2: p in ( Cl (R ` )) by XBOOLE_0:def 4;

        let S be Subset of GX;

        assume that

         A3: S is open and

         A4: p in S;

        p in ( Cl R) by A1, XBOOLE_0:def 4;

        hence R meets S & (R ` ) meets S by A3, A4, A2, Th12;

      end;

      assume

       A5: for S be Subset of GX st S is open & p in S holds R meets S & (R ` ) meets S;

      then for S be Subset of GX st S is open & p in S holds (R ` ) meets S;

      then

       A6: p in ( Cl (R ` )) by Th12;

      for S be Subset of GX st S is open & p in S holds R meets S by A5;

      then p in ( Cl R) by Th12;

      hence thesis by A6, XBOOLE_0:def 4;

    end;

    theorem :: TOPS_1:29

    ( Fr T) = ( Fr (T ` ));

    theorem :: TOPS_1:30

    ( Fr T) = ((( Cl (T ` )) /\ T) \/ (( Cl T) \ T))

    proof

      for x be object holds x in ( Fr T) iff x in ((( Cl (T ` )) /\ T) \/ (( Cl T) \ T))

      proof

        let x be object;

        

         A1: (T ` ) c= ( Cl (T ` )) by PRE_TOPC: 18;

        thus x in ( Fr T) implies x in ((( Cl (T ` )) /\ T) \/ (( Cl T) \ T))

        proof

          assume

           A2: x in ( Fr T);

          then

          reconsider x99 = x as Point of GX;

          x99 in ( Cl T) & x99 in ( Cl (T ` )) & x99 in T or x99 in ( Cl T) & x99 in ( Cl (T ` )) & x99 in (T ` ) by A2, SUBSET_1: 29, XBOOLE_0:def 4;

          then x99 in (( Cl (T ` )) /\ T) or not x99 in T & x99 in ( Cl T) by XBOOLE_0:def 4;

          then x99 in (( Cl (T ` )) /\ T) or x99 in (( Cl T) \ T) by XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

        

         A3: T c= ( Cl T) by PRE_TOPC: 18;

        thus x in ((( Cl (T ` )) /\ T) \/ (( Cl T) \ T)) implies x in ( Fr T)

        proof

          assume

           A4: x in ((( Cl (T ` )) /\ T) \/ (( Cl T) \ T));

          then

          reconsider x99 = x as Point of GX;

          x99 in (( Cl (T ` )) /\ T) or x99 in (( Cl T) \ T) by A4, XBOOLE_0:def 3;

          then x99 in ( Cl (T ` )) & x99 in T or x99 in ( Cl T) & not x99 in T by XBOOLE_0:def 4, XBOOLE_0:def 5;

          then x99 in ( Cl (T ` )) & x99 in T or x99 in ( Cl T) & x99 in (T ` ) by SUBSET_1: 29;

          hence thesis by A3, A1, XBOOLE_0:def 4;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPS_1:31

    

     Th31: ( Cl T) = (T \/ ( Fr T))

    proof

      

       A1: ((T \/ ( Cl T)) /\ (T \/ ( Cl (T ` )))) = (( Cl T) /\ (T \/ ( Cl (T ` )))) by PRE_TOPC: 18, XBOOLE_1: 12;

      (T \/ (( Cl T) \ T)) c= (T \/ (( Cl T) /\ ( Cl (T ` ))))

      proof

        let x be object;

        assume

         A2: x in (T \/ (( Cl T) \ T));

        then

        reconsider x99 = x as Point of GX;

        x99 in T or x99 in (( Cl T) \ T) by A2, XBOOLE_0:def 3;

        then

         A3: x99 in T or x99 in ( Cl T) & x99 in (T ` ) by XBOOLE_0:def 5;

        (T ` ) c= ( Cl (T ` )) by PRE_TOPC: 18;

        then x99 in T or x99 in (( Cl T) /\ ( Cl (T ` ))) by A3, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 3;

      end;

      then

       A4: ( Cl T) c= (T \/ ( Fr T)) by PRE_TOPC: 18, XBOOLE_1: 45;

      (T \/ ( Fr T)) = ((T \/ ( Cl T)) /\ (T \/ ( Cl (T ` )))) by XBOOLE_1: 24;

      then (T \/ ( Fr T)) c= ( Cl T) by A1, XBOOLE_1: 17;

      hence thesis by A4;

    end;

    theorem :: TOPS_1:32

    

     Th32: ( Fr (K /\ L)) c= (( Fr K) \/ ( Fr L))

    proof

      ( Cl (K /\ L)) c= ( Cl K) by PRE_TOPC: 19, XBOOLE_1: 17;

      then

       A1: (( Cl (K /\ L)) /\ ( Cl (K ` ))) c= (( Cl K) /\ ( Cl (K ` ))) by XBOOLE_1: 26;

      ( Cl (K /\ L)) c= ( Cl L) by PRE_TOPC: 19, XBOOLE_1: 17;

      then

       A2: (( Cl (K /\ L)) /\ ( Cl (L ` ))) c= (( Cl L) /\ ( Cl (L ` ))) by XBOOLE_1: 26;

      ( Fr (K /\ L)) = (( Cl (K /\ L)) /\ ( Cl ((K ` ) \/ (L ` )))) by XBOOLE_1: 54

      .= (( Cl (K /\ L)) /\ (( Cl (K ` )) \/ ( Cl (L ` )))) by PRE_TOPC: 20

      .= ((( Cl (K /\ L)) /\ ( Cl (K ` ))) \/ (( Cl (K /\ L)) /\ ( Cl (L ` )))) by XBOOLE_1: 23;

      hence thesis by A1, A2, XBOOLE_1: 13;

    end;

    theorem :: TOPS_1:33

    

     Th33: ( Fr (K \/ L)) c= (( Fr K) \/ ( Fr L))

    proof

      ( Cl ((K ` ) /\ (L ` ))) c= ( Cl (K ` )) by PRE_TOPC: 19, XBOOLE_1: 17;

      then

       A1: (( Cl ((K ` ) /\ (L ` ))) /\ ( Cl K)) c= (( Cl (K ` )) /\ ( Cl K)) by XBOOLE_1: 26;

      ( Cl ((K ` ) /\ (L ` ))) c= ( Cl (L ` )) by PRE_TOPC: 19, XBOOLE_1: 17;

      then

       A2: (( Cl ((K ` ) /\ (L ` ))) /\ ( Cl L)) c= (( Cl (L ` )) /\ ( Cl L)) by XBOOLE_1: 26;

      ( Fr (K \/ L)) = ((( Cl K) \/ ( Cl L)) /\ ( Cl ((K \/ L) ` ))) by PRE_TOPC: 20

      .= (( Cl ((K ` ) /\ (L ` ))) /\ (( Cl K) \/ ( Cl L))) by XBOOLE_1: 53

      .= ((( Cl ((K ` ) /\ (L ` ))) /\ ( Cl K)) \/ (( Cl ((K ` ) /\ (L ` ))) /\ ( Cl L))) by XBOOLE_1: 23;

      hence thesis by A1, A2, XBOOLE_1: 13;

    end;

    theorem :: TOPS_1:34

    

     Th34: ( Fr ( Fr T)) c= ( Fr T)

    proof

      let x be object;

      assume x in ( Fr ( Fr T));

      then

       A1: x in ( Cl (( Cl T) /\ ( Cl (T ` )))) by XBOOLE_0:def 4;

      ( Cl (( Cl T) /\ ( Cl (T ` )))) c= (( Cl ( Cl T)) /\ ( Cl ( Cl (T ` )))) by PRE_TOPC: 21;

      hence thesis by A1;

    end;

    theorem :: TOPS_1:35

    R is closed implies ( Fr R) c= R

    proof

      assume

       A1: R is closed;

      let x be object;

      ( Cl R) = R by A1, PRE_TOPC: 22;

      hence thesis by XBOOLE_0:def 4;

    end;

    

     Lm1: ( Fr K) c= ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L)))

    proof

      let x be object;

      

       A1: ((L ` ) /\ (K ` )) = ((K \/ L) ` ) by XBOOLE_1: 53;

      assume

       A2: x in ( Fr K);

      then

      reconsider x99 = x as Point of TS;

      

       A3: TS is non empty by A2;

      assume

       A4: not x in ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L)));

      then

       A5: not x99 in (( Fr (K \/ L)) \/ ( Fr (K /\ L))) by XBOOLE_0:def 3;

      then not x99 in ( Fr (K \/ L)) by XBOOLE_0:def 3;

      then

      consider Q1 be Subset of TS such that

       A6: Q1 is open and

       A7: x99 in Q1 and

       A8: (K \/ L) misses Q1 or ((K \/ L) ` ) misses Q1 by A3, Th28;

      ((K \/ L) /\ Q1) = {} or (((K \/ L) ` ) /\ Q1) = {} by A8;

      then

       A9: ((K /\ Q1) \/ (Q1 /\ L)) = {} or ((L ` ) /\ ((K ` ) /\ Q1)) = {} by A1, XBOOLE_1: 16, XBOOLE_1: 23;

       not x99 in (( Fr K) /\ ( Fr L)) by A4, XBOOLE_0:def 3;

      then not x99 in ( Fr L) by A2, XBOOLE_0:def 4;

      then

      consider Q3 be Subset of TS such that

       A10: Q3 is open and

       A11: x99 in Q3 and

       A12: L misses Q3 or (L ` ) misses Q3 by A3, Th28;

      K meets Q1 by A2, A3, A6, A7, Th28;

      then

       A13: (K /\ Q1) <> {} ;

       A14:

      now

        assume (L /\ Q3) = {} ;

        then Q3 misses ((L ` ) ` );

        then

         A15: Q3 c= (L ` ) by SUBSET_1: 24;

        (((K ` ) /\ Q1) /\ ((L ` ) /\ Q3)) = ( {} /\ Q3) by A9, A13, XBOOLE_1: 16;

        then (((K ` ) /\ Q1) /\ Q3) = {} by A15, XBOOLE_1: 28;

        hence ((K ` ) /\ (Q1 /\ Q3)) = {} by XBOOLE_1: 16;

      end;

      

       A16: ((L ` ) \/ (K ` )) = ((K /\ L) ` ) by XBOOLE_1: 54;

       not x99 in ( Fr (K /\ L)) by A5, XBOOLE_0:def 3;

      then

      consider Q2 be Subset of TS such that

       A17: Q2 is open and

       A18: x99 in Q2 and

       A19: (K /\ L) misses Q2 or ((K /\ L) ` ) misses Q2 by A3, Th28;

      ((K /\ L) /\ Q2) = {} or (((K /\ L) ` ) /\ Q2) = {} by A19;

      then

       A20: ((K /\ Q2) /\ L) = {} or (((K ` ) /\ Q2) \/ (Q2 /\ (L ` ))) = {} by A16, XBOOLE_1: 16, XBOOLE_1: 23;

      x99 in (Q1 /\ Q3) by A7, A11, XBOOLE_0:def 4;

      then (K ` ) meets (Q1 /\ Q3) by A2, A3, A6, A10, Th28;

      then

       A21: Q3 c= L by A12, A14, SUBSET_1: 24;

      (K ` ) meets Q2 by A2, A3, A17, A18, Th28;

      then ((K ` ) /\ Q2) <> {} ;

      then ((K /\ (Q2 /\ L)) /\ Q3) = ( {} /\ Q3) by A20, XBOOLE_1: 16;

      then (K /\ ((Q2 /\ L) /\ Q3)) = {} by XBOOLE_1: 16;

      then (K /\ (Q2 /\ (L /\ Q3))) = {} by XBOOLE_1: 16;

      then (K /\ (Q2 /\ Q3)) = {} by A21, XBOOLE_1: 28;

      then

       A22: K misses (Q2 /\ Q3);

      x99 in (Q2 /\ Q3) by A18, A11, XBOOLE_0:def 4;

      hence contradiction by A2, A3, A17, A10, A22, Th28;

    end;

    theorem :: TOPS_1:36

    (( Fr K) \/ ( Fr L)) = ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L)))

    proof

      

       A1: ( Fr L) c= ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L))) by Lm1;

      

       A2: ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L))) c= (( Fr K) \/ ( Fr L))

      proof

        let x be object;

         A3:

        now

          assume x in (( Fr K) /\ ( Fr L));

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

          hence thesis by XBOOLE_0:def 3;

        end;

         A4:

        now

          assume

           A5: x in ( Fr (K \/ L));

          ( Fr (K \/ L)) c= (( Fr K) \/ ( Fr L)) by Th33;

          hence thesis by A5;

        end;

         A6:

        now

          assume

           A7: x in ( Fr (K /\ L));

          ( Fr (K /\ L)) c= (( Fr K) \/ ( Fr L)) by Th32;

          hence thesis by A7;

        end;

        assume x in ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L)));

        then x in (( Fr (K \/ L)) \/ ( Fr (K /\ L))) or x in (( Fr K) /\ ( Fr L)) by XBOOLE_0:def 3;

        hence thesis by A4, A6, A3, XBOOLE_0:def 3;

      end;

      ( Fr K) c= ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L))) by Lm1;

      then (( Fr K) \/ ( Fr L)) c= ((( Fr (K \/ L)) \/ ( Fr (K /\ L))) \/ (( Fr K) /\ ( Fr L))) by A1, XBOOLE_1: 8;

      hence thesis by A2;

    end;

    theorem :: TOPS_1:37

    ( Fr ( Int T)) c= ( Fr T)

    proof

      let x be object;

      assume

       A1: x in ( Fr ( Int T));

      then

       A2: x in ( Cl (T ` )) by XBOOLE_0:def 4;

      ( Int T) = (( Cl (T ` )) ` );

      then

       A3: ( Cl (( Cl (T ` )) ` )) c= ( Cl T) by Th16, PRE_TOPC: 19;

      x in ( Cl (( Cl (T ` )) ` )) by A1, XBOOLE_0:def 4;

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

    end;

    theorem :: TOPS_1:38

    ( Fr ( Cl T)) c= ( Fr T)

    proof

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

      then (( Cl T) ` ) c= (T ` ) by SUBSET_1: 12;

      then ( Cl (( Cl T) ` )) c= ( Cl (T ` )) by PRE_TOPC: 19;

      hence thesis by XBOOLE_1: 26;

    end;

    theorem :: TOPS_1:39

    

     Th39: ( Int T) misses ( Fr T)

    proof

      ( Fr T) = (( Cl T) /\ ((( Cl (T ` )) ` ) ` ))

      .= (( Cl T) \ (( Cl (T ` )) ` )) by SUBSET_1: 13;

      hence thesis by XBOOLE_1: 79;

    end;

    theorem :: TOPS_1:40

    

     Th40: ( Int T) = (T \ ( Fr T))

    proof

      ((( Cl (T ` )) ` ) \/ (( Cl T) ` )) = ((( Cl T) /\ ( Cl (T ` ))) ` ) by XBOOLE_1: 54;

      

      then

       A1: (T \ ( Fr T)) = (T /\ ((( Cl (T ` )) ` ) \/ (( Cl T) ` ))) by SUBSET_1: 13

      .= ((T /\ (( Cl T) ` )) \/ (T /\ ( Int T))) by XBOOLE_1: 23;

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

      then

       A2: T misses (( Cl T) ` ) by SUBSET_1: 24;

      ( Int T) = (T /\ ( Int T)) by Th16, XBOOLE_1: 28;

      then (T \ ( Fr T)) = ( {} \/ ( Int T)) by A1, A2;

      hence thesis;

    end;

    

     Lm2: ( Fr T) = (( Cl T) \ ( Int T))

    proof

      ( Fr T) = (( Cl T) /\ (( Int T) ` ))

      .= (( Cl T) \ ( Int T)) by SUBSET_1: 13;

      hence thesis;

    end;

    

     Lm3: ( Cl ( Fr K)) = ( Fr K)

    proof

      

       A1: ( Cl ( Cl (K ` ))) = ( Cl (K ` ));

      ( Cl ( Cl K)) = ( Cl K);

      hence thesis by A1, Th7;

    end;

    

     Lm4: ( Int ( Fr ( Fr K))) = {}

    proof

      set x9 = the Element of ( Int ( Fr ( Fr K)));

      assume

       A1: ( Int ( Fr ( Fr K))) <> {} ;

      then

      reconsider x = x9 as Point of TS by TARSKI:def 3;

      

       A2: TS is non empty by A1;

      

       A3: ( Int ( Fr ( Fr K))) c= ( Fr ( Fr K)) by Th16;

      then x in ( Fr ( Fr K)) by A1;

      then (( Fr K) ` ) meets ( Int ( Fr ( Fr K))) by A1, A2, Th28;

      then

       A4: ((( Fr K) ` ) /\ ( Int ( Fr ( Fr K)))) <> {} ;

      ( Fr ( Fr K)) c= ( Fr K) by Th34;

      then ( Int ( Fr ( Fr K))) c= ( Fr K) by A3;

      then

       A5: ((( Fr K) ` ) /\ ( Fr K)) <> {} by A4, XBOOLE_1: 3, XBOOLE_1: 26;

      ( Fr K) misses (( Fr K) ` ) by XBOOLE_1: 79;

      hence contradiction by A5;

    end;

    theorem :: TOPS_1:41

    ( Fr ( Fr ( Fr K))) = ( Fr ( Fr K))

    proof

      

       A1: ( Int ( Fr ( Fr K))) = {} by Lm4;

      ( Fr ( Fr ( Fr K))) = (( Cl ( Fr ( Fr K))) \ ( Int ( Fr ( Fr K)))) by Lm2

      .= ( Fr ( Fr K)) by A1, Lm3;

      hence thesis;

    end;

    

     Lm5: for X,Y,Z be set holds X c= Z & Y = (Z \ X) implies X c= (Z \ Y)

    proof

      let X,Y,Z be set;

      assume that

       A1: X c= Z and

       A2: Y = (Z \ X);

      let x be object;

      assume

       A3: x in X;

      then not x in Y by A2, XBOOLE_0:def 5;

      hence thesis by A1, A3, XBOOLE_0:def 5;

    end;

    theorem :: TOPS_1:42

    

     Th42: P is open iff ( Fr P) = (( Cl P) \ P)

    proof

      

       A1: ( Fr P) misses (( Fr P) ` ) by XBOOLE_1: 79;

      

       A2: ( Int P) c= P by Th16;

      hereby

        assume P is open;

        then P = ( Int P) by Th23;

        hence ( Fr P) = (( Cl P) \ P) by Lm2;

      end;

      assume

       A3: ( Fr P) = (( Cl P) \ P);

      (( Cl P) \ ( Fr P)) = ((P \/ ( Fr P)) \ ( Fr P)) by Th31

      .= ((( Fr P) ` ) /\ (P \/ ( Fr P))) by SUBSET_1: 13

      .= ((P /\ (( Fr P) ` )) \/ ((( Fr P) ` ) /\ ( Fr P))) by XBOOLE_1: 23

      .= ((P \ ( Fr P)) \/ (( Fr P) /\ (( Fr P) ` ))) by SUBSET_1: 13

      .= (( Int P) \/ (( Fr P) /\ (( Fr P) ` ))) by Th40

      .= (( Int P) \/ ( {} TS)) by A1

      .= ( Int P);

      then P c= ( Int P) by A3, Lm5, PRE_TOPC: 18;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: TOPS_1:43

    

     Th43: P is closed iff ( Fr P) = (P \ ( Int P))

    proof

      

       A1: (P ` ) misses P by XBOOLE_1: 79;

      ((P ` ) /\ ( Int P)) c= ((P ` ) /\ P) by Th16, XBOOLE_1: 26;

      then

       A2: ((P ` ) /\ ( Int P)) c= ( {} TS) by A1;

      thus P is closed implies ( Fr P) = (P \ ( Int P))

      proof

        assume P is closed;

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

        hence thesis by Lm2;

      end;

      

       A3: (((P ` ) ` ) \/ (( Int P) ` )) = (((P ` ) /\ ( Int P)) ` ) by XBOOLE_1: 54;

      assume ( Fr P) = (P \ ( Int P));

      

      then ( Cl P) = (P \/ (P \ ( Int P))) by Th31

      .= (P \/ ((( Int P) ` ) /\ P)) by SUBSET_1: 13

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

      .= ((( {} TS) ` ) /\ P) by A2, A3

      .= P by XBOOLE_1: 28;

      hence thesis;

    end;

    definition

      let GX be TopStruct, R be Subset of GX;

      :: TOPS_1:def3

      attr R is dense means ( Cl R) = ( [#] GX);

    end

    registration

      let GX;

      cluster ( [#] GX) -> dense;

      coherence by Th2;

      cluster dense for Subset of GX;

      existence

      proof

        take ( [#] GX);

        thus thesis;

      end;

    end

    theorem :: TOPS_1:44

    R is dense & R c= S implies S is dense

    proof

      assume that

       A1: R is dense and

       A2: R c= S;

      ( Cl R) = ( [#] GX) by A1;

      then ( [#] GX) c= ( Cl S) by A2, PRE_TOPC: 19;

      then ( [#] GX) = ( Cl S);

      hence thesis;

    end;

    theorem :: TOPS_1:45

    

     Th45: P is dense iff for Q st Q <> {} & Q is open holds P meets Q

    proof

      hereby

        assume P is dense;

        then

         A1: ( Cl P) = ( [#] TS);

        let Q;

        assume that

         A2: Q <> {} and

         A3: Q is open;

        set x = the Element of Q;

        x in Q by A2;

        then

         A4: TS is non empty;

        x in ( Cl P) by A2, A1, TARSKI:def 3;

        hence P meets Q by A2, A3, A4, Th12;

      end;

      assume

       A5: for Q st Q <> {} & Q is open holds P meets Q;

      ( [#] TS) c= ( Cl P)

      proof

        let x be object;

        

         A6: for C be Subset of TS st C is open & x in C holds P meets C by A5;

        assume

         A7: x in ( [#] TS);

        then TS is non empty;

        hence thesis by A7, A6, Th12;

      end;

      then ( Cl P) = ( [#] TS);

      hence thesis;

    end;

    theorem :: TOPS_1:46

    

     Th46: P is dense implies for Q holds Q is open implies ( Cl Q) = ( Cl (Q /\ P))

    proof

      assume

       A1: P is dense;

      let Q;

      assume

       A2: Q is open;

      thus ( Cl Q) c= ( Cl (Q /\ P))

      proof

        let x be object;

        assume

         A3: x in ( Cl Q);

        then

         A4: TS is non empty;

        now

          let Q1 be Subset of TS;

          assume

           A5: Q1 is open;

          assume x in Q1;

          then Q meets Q1 by A3, A4, A5, Th12;

          then (Q /\ Q1) <> {} ;

          then P meets (Q /\ Q1) by A1, A2, A5, Th45;

          then

           A6: (P /\ (Q /\ Q1)) <> {} ;

          (P /\ (Q /\ Q1)) = ((Q /\ P) /\ Q1) by XBOOLE_1: 16;

          hence (Q /\ P) meets Q1 by A6;

        end;

        hence thesis by A3, A4, Th12;

      end;

      thus thesis by PRE_TOPC: 19, XBOOLE_1: 17;

    end;

    theorem :: TOPS_1:47

    P is dense & Q is dense & Q is open implies (P /\ Q) is dense by Th46;

    definition

      let GX be TopStruct, R be Subset of GX;

      :: TOPS_1:def4

      attr R is boundary means (R ` ) is dense;

    end

    registration

      let GX;

      cluster empty -> boundary for Subset of GX;

      coherence

      proof

        let A be Subset of GX;

        assume A is empty;

        hence ( Cl (A ` )) = ( [#] GX) by Th2;

      end;

    end

    theorem :: TOPS_1:48

    

     Th48: R is boundary iff ( Int R) = {}

    proof

      R is boundary iff (R ` ) is dense;

      then R is boundary iff ( Cl (R ` )) = ( [#] GX);

      then R is boundary iff (( Cl (R ` )) ` ) = (( [#] GX) ` ) by SUBSET_1: 42;

      hence thesis by XBOOLE_1: 37;

    end;

    registration

      let GX;

      cluster boundary for Subset of GX;

      existence

      proof

        take ( {} GX);

        thus thesis;

      end;

    end

    registration

      let GX;

      let R be boundary Subset of GX;

      cluster ( Int R) -> empty;

      coherence by Th48;

    end

    theorem :: TOPS_1:49

    

     Th49: P is boundary & Q is boundary & Q is closed implies (P \/ Q) is boundary

    proof

      assume that

       A1: P is boundary and

       A2: Q is boundary and

       A3: Q is closed;

      

       A4: ( Cl ((P ` ) \ Q)) = ( Cl ((P ` ) /\ (Q ` ))) by SUBSET_1: 13;

      (P ` ) is dense by A1;

      then

       A5: (( [#] TS) \ Q) = (( Cl (P ` )) \ Q);

      

       A6: (( Cl (P ` )) \ ( Cl Q)) c= ( Cl ((P ` ) \ Q)) by Th6;

      (Q ` ) is dense by A2;

      then

       A7: ( Cl (Q ` )) = ( [#] TS);

      (( Cl (P ` )) \ Q) = (( Cl (P ` )) \ ( Cl Q)) by A3, PRE_TOPC: 22;

      then (( [#] TS) \ Q) c= ( Cl ((P \/ Q) ` )) by A5, A6, A4, XBOOLE_1: 53;

      then ( Cl (Q ` )) c= ( Cl ( Cl ((P \/ Q) ` ))) by PRE_TOPC: 19;

      then ( [#] TS) = ( Cl ((P \/ Q) ` )) by A7;

      then ((P \/ Q) ` ) is dense;

      hence thesis;

    end;

    theorem :: TOPS_1:50

    P is boundary iff for Q st Q c= P & Q is open holds Q = {}

    proof

      hereby

        assume P is boundary;

        then

         A1: (P ` ) is dense;

        let Q;

        assume that

         A2: Q c= P and

         A3: Q is open and

         A4: Q <> {} ;

        Q meets (P ` ) by A1, A3, A4, Th45;

        hence contradiction by A2, SUBSET_1: 24;

      end;

      assume

       A5: for Q st Q c= P & Q is open holds Q = {} ;

      assume not P is boundary;

      then not (P ` ) is dense;

      then

      consider C be Subset of TS such that

       A6: C <> {} and

       A7: C is open and

       A8: (P ` ) misses C by Th45;

      C c= P by A8, SUBSET_1: 24;

      hence contradiction by A5, A6, A7;

    end;

    theorem :: TOPS_1:51

    P is closed implies (P is boundary iff for Q st Q <> {} & Q is open holds ex G be Subset of TS st G c= Q & G <> {} & G is open & P misses G)

    proof

      assume

       A1: P is closed;

      hereby

        assume P is boundary;

        then

         A2: (P ` ) is dense;

        

         A3: P misses (P ` ) by XBOOLE_1: 79;

        let Q such that

         A4: Q <> {} and

         A5: Q is open;

        (P /\ ((P ` ) /\ Q)) = ((P /\ (P ` )) /\ Q) by XBOOLE_1: 16

        .= (( {} TS) /\ Q) by A3

        .= {} ;

        then

         A6: P misses ((P ` ) /\ Q);

        (P ` ) meets Q by A2, A4, A5, Th45;

        then ((P ` ) /\ Q) <> {} ;

        hence ex G be Subset of TS st G c= Q & G <> {} & G is open & P misses G by A1, A5, A6, XBOOLE_1: 17;

      end;

      assume

       A7: for Q st Q <> {} & Q is open holds ex G be Subset of TS st G c= Q & G <> {} & G is open & P misses G;

      now

        let Q such that

         A8: Q <> {} and

         A9: Q is open;

        consider G be Subset of TS such that

         A10: G c= Q and

         A11: G <> {} and G is open and

         A12: P misses G by A7, A8, A9;

        G misses ((P ` ) ` ) by A12;

        then G c= (P ` ) by SUBSET_1: 24;

        hence (P ` ) meets Q by A10, A11, XBOOLE_1: 67;

      end;

      then (P ` ) is dense by Th45;

      hence thesis;

    end;

    theorem :: TOPS_1:52

    R is boundary iff R c= ( Fr R)

    proof

      

       A1: (( Cl R) /\ ( Cl (R ` ))) c= ( Cl (R ` )) by XBOOLE_1: 17;

      hereby

        assume R is boundary;

        then (R ` ) is dense;

        then (( Cl R) /\ ( Cl (R ` ))) = (( Cl R) /\ ( [#] GX));

        then ( Cl R) = (( Cl R) /\ ( Cl (R ` ))) by XBOOLE_1: 28;

        hence R c= ( Fr R) by PRE_TOPC: 18;

      end;

      

       A2: (R ` ) c= ( Cl (R ` )) by PRE_TOPC: 18;

      assume R c= ( Fr R);

      then R c= ( Cl (R ` )) by A1;

      then (R \/ (R ` )) c= ( Cl (R ` )) by A2, XBOOLE_1: 8;

      then ( [#] GX) c= ( Cl (R ` )) by PRE_TOPC: 2;

      then ( [#] GX) = ( Cl (R ` ));

      then (R ` ) is dense;

      hence thesis;

    end;

    registration

      let GX be non empty TopSpace;

      cluster ( [#] GX) -> non boundary;

      coherence

      proof

        ( Int ( [#] GX)) <> {} by Th15;

        hence thesis;

      end;

      cluster non boundary non empty for Subset of GX;

      existence

      proof

        take ( [#] GX);

        thus thesis;

      end;

    end

    definition

      let GX be TopStruct, R be Subset of GX;

      :: TOPS_1:def5

      attr R is nowhere_dense means ( Cl R) is boundary;

    end

    registration

      let TS;

      cluster empty -> nowhere_dense for Subset of TS;

      coherence by PRE_TOPC: 22;

    end

    registration

      let TS;

      cluster nowhere_dense for Subset of TS;

      existence

      proof

        take ( {} TS);

        thus thesis;

      end;

    end

    theorem :: TOPS_1:53

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

    proof

      assume that

       A1: P is nowhere_dense and

       A2: Q is nowhere_dense;

      

       A3: ( Cl Q) is boundary by A2;

      ( Cl P) is boundary by A1;

      then (( Cl P) \/ ( Cl Q)) is boundary by A3, Th49;

      then ( Cl (P \/ Q)) is boundary by PRE_TOPC: 20;

      hence thesis;

    end;

    theorem :: TOPS_1:54

    

     Th54: R is nowhere_dense implies (R ` ) is dense

    proof

      assume R is nowhere_dense;

      then ( Cl R) is boundary;

      then (( Cl R) ` ) is dense;

      then

       A1: ( Cl (( Cl R) ` )) = ( [#] GX);

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

      then (( Cl R) ` ) c= (R ` ) by SUBSET_1: 12;

      then ( [#] GX) c= ( Cl (R ` )) by A1, PRE_TOPC: 19;

      then ( [#] GX) = ( Cl (R ` ));

      hence thesis;

    end;

    registration

      let TS;

      let R be nowhere_dense Subset of TS;

      cluster (R ` ) -> dense;

      coherence by Th54;

    end

    theorem :: TOPS_1:55

    R is nowhere_dense implies R is boundary by Th54;

    registration

      let TS;

      cluster nowhere_dense -> boundary for Subset of TS;

      coherence ;

    end

    theorem :: TOPS_1:56

    

     Th56: S is boundary & S is closed implies S is nowhere_dense by PRE_TOPC: 22;

    registration

      let TS;

      cluster boundary closed -> nowhere_dense for Subset of TS;

      coherence by Th56;

    end

    theorem :: TOPS_1:57

    R is closed implies (R is nowhere_dense iff R = ( Fr R))

    proof

      assume R is closed;

      then

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

      hereby

        assume R is nowhere_dense;

        then ( Cl R) is boundary;

        then (( Cl R) ` ) is dense;

        then ( Fr R) = (R /\ ( [#] GX)) by A1;

        hence R = ( Fr R) by XBOOLE_1: 28;

      end;

      assume R = ( Fr R);

      then R = (R \ ( Int R)) by A1, Lm2;

      then ( Int ( Cl R)) = {} by A1, Th16, XBOOLE_1: 38;

      then ( Cl R) is boundary by Th48;

      hence thesis;

    end;

    theorem :: TOPS_1:58

    

     Th58: P is open implies ( Fr P) is nowhere_dense

    proof

      

       A1: ( Int ( Cl P)) c= ( Cl P) by Th16;

      assume P is open;

      then

       A2: ( Int P) = P by Th23;

      then P misses ( Fr P) by Th39;

      then

       A3: (P /\ ( Fr P)) = ( {} TS);

      ( Int (P /\ ( Fr P))) = (P /\ ( Int ( Fr P))) by A2, Th17;

      then (P /\ ( Int ( Fr P))) = {} by A3;

      then

       A4: P misses ( Int ( Fr P));

      ( Int ( Fr P)) c= ( Int ( Cl P)) by Th19, XBOOLE_1: 17;

      then

       A5: ( Int ( Fr P)) c= ( Cl P) by A1;

      ( Fr P) is boundary

      proof

        set x = the Element of ( Int ( Fr P));

        assume

         A6: not ( Fr P) is boundary;

        then

         A7: TS is non empty;

        

         A8: ( Int ( Fr P)) <> {} by A6, Th48;

        then x in ( Cl P) by A5;

        hence contradiction by A4, A8, A7, Th12;

      end;

      hence thesis;

    end;

    registration

      let TS;

      let P be open Subset of TS;

      cluster ( Fr P) -> nowhere_dense;

      coherence by Th58;

    end

    theorem :: TOPS_1:59

    

     Th59: P is closed implies ( Fr P) is nowhere_dense

    proof

      assume P is closed;

      then ( Fr (P ` )) is nowhere_dense;

      hence thesis;

    end;

    registration

      let TS;

      let P be closed Subset of TS;

      cluster ( Fr P) -> nowhere_dense;

      coherence by Th59;

    end

    theorem :: TOPS_1:60

    

     Th60: P is open & P is nowhere_dense implies P = {}

    proof

      assume that

       A1: P is open and

       A2: P is nowhere_dense and

       A3: P <> {} ;

      P meets (P ` ) by A1, A2, A3, Th45;

      hence contradiction by XBOOLE_1: 79;

    end;

    registration

      let TS;

      cluster open nowhere_dense -> empty for Subset of TS;

      coherence by Th60;

    end

    definition

      let GX be TopStruct, R be Subset of GX;

      :: TOPS_1:def6

      attr R is condensed means ( Int ( Cl R)) c= R & R c= ( Cl ( Int R));

      :: TOPS_1:def7

      attr R is closed_condensed means R = ( Cl ( Int R));

      :: TOPS_1:def8

      attr R is open_condensed means R = ( Int ( Cl R));

    end

    theorem :: TOPS_1:61

    R is open_condensed iff (R ` ) is closed_condensed;

    theorem :: TOPS_1:62

    R is closed_condensed implies ( Fr ( Int R)) = ( Fr R);

    theorem :: TOPS_1:63

    R is closed_condensed implies ( Fr R) c= ( Cl ( Int R)) by XBOOLE_1: 17;

    theorem :: TOPS_1:64

    

     Th64: R is open_condensed implies ( Fr R) = ( Fr ( Cl R)) & ( Fr ( Cl R)) = (( Cl R) \ R) by Lm2;

    theorem :: TOPS_1:65

    R is open & R is closed implies (R is closed_condensed iff R is open_condensed) by PRE_TOPC: 22, Th23;

    theorem :: TOPS_1:66

    (R is closed & R is condensed implies R is closed_condensed) & (P is closed_condensed implies P is closed & P is condensed)

    proof

      hereby

        assume that

         A1: R is closed and

         A2: R is condensed;

        

         A3: R = ( Cl R) by A1, PRE_TOPC: 22;

        then ( Int R) c= R by A2;

        then

         A4: ( Cl ( Int R)) c= R by A3, PRE_TOPC: 19;

        R c= ( Cl ( Int R)) by A2;

        then ( Cl ( Int R)) = R by A4;

        hence R is closed_condensed;

      end;

      assume

       A5: P is closed_condensed;

      ( Fr ( Int P)) = (( Cl ( Int P)) \ ( Int ( Int P))) by Lm2;

      

      then ( Fr P) = (( Cl ( Int P)) \ ( Int ( Int P))) by A5

      .= (P \ ( Int P)) by A5;

      then P is closed by Th43;

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

      then

       A6: ( Int ( Cl P)) c= P by Th16;

      ( Cl ( Int P)) = P by A5;

      hence thesis by A6;

    end;

    theorem :: TOPS_1:67

    (R is open & R is condensed implies R is open_condensed) & (P is open_condensed implies P is open & P is condensed)

    proof

      hereby

        assume that

         A1: R is open and

         A2: R is condensed;

        R = ( Int R) by A1, Th23;

        then

         A3: R c= ( Int ( Cl R)) by Th19, PRE_TOPC: 18;

        ( Int ( Cl R)) c= R by A2;

        then ( Int ( Cl R)) = R by A3;

        hence R is open_condensed;

      end;

      assume

       A4: P is open_condensed;

      then

       A5: ( Fr ( Cl P)) = (( Cl P) \ P) by Th64;

      ( Fr P) = ( Fr ( Cl P)) by A4;

      then P is open by A5, Th42;

      then ( Int P) = P by Th23;

      then

       A6: P c= ( Cl ( Int P)) by PRE_TOPC: 18;

      P = ( Int ( Cl P)) by A4;

      hence thesis by A6;

    end;

    theorem :: TOPS_1:68

    

     Th68: P is closed_condensed & Q is closed_condensed implies (P \/ Q) is closed_condensed

    proof

      assume that

       A1: P is closed_condensed and

       A2: Q is closed_condensed;

      

       A3: Q = ( Cl ( Int Q)) by A2;

      P = ( Cl ( Int P)) by A1;

      then (P \/ Q) = ( Cl (( Int P) \/ ( Int Q))) by A3, PRE_TOPC: 20;

      then

       A4: (P \/ Q) c= ( Cl ( Int (P \/ Q))) by Th20, PRE_TOPC: 19;

      

       A5: ( Cl ( Int (P \/ Q))) c= ( Cl (P \/ Q)) by Th16, PRE_TOPC: 19;

      

       A6: Q is closed by A2;

      P is closed by A1;

      then ( Cl ( Int (P \/ Q))) c= (P \/ Q) by A5, A6, PRE_TOPC: 22;

      then (P \/ Q) = ( Cl ( Int (P \/ Q))) by A4;

      hence thesis;

    end;

    theorem :: TOPS_1:69

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

    proof

      

       A1: ((P ` ) \/ (Q ` )) = ((P /\ Q) ` ) by XBOOLE_1: 54;

      assume that

       A2: P is open_condensed and

       A3: Q is open_condensed;

      

       A4: (Q ` ) is closed_condensed by A3;

      (P ` ) is closed_condensed by A2;

      then ((P ` ) \/ (Q ` )) is closed_condensed by A4, Th68;

      hence thesis by A1;

    end;

    theorem :: TOPS_1:70

    P is condensed implies ( Int ( Fr P)) = {}

    proof

      set x = the Element of ( Int ( Fr P));

      assume

       A1: P is condensed;

      then P c= ( Cl ( Int P));

      then

       A2: (( Cl ( Int P)) ` ) c= (P ` ) by SUBSET_1: 12;

      assume

       A3: ( Int ( Fr P)) <> {} ;

      then

      reconsider x99 = x as Point of TS by TARSKI:def 3;

      

       A4: ( Int ( Fr P)) = (( Cl ((( Cl P) ` ) \/ (( Cl (P ` )) ` ))) ` ) by XBOOLE_1: 54

      .= ((( Cl (( Cl P) ` )) \/ ( Cl (( Cl (P ` )) ` ))) ` ) by PRE_TOPC: 20

      .= (( Int ( Cl P)) /\ (( Cl ( Int P)) ` )) by XBOOLE_1: 53;

      then

       A5: x99 in ( Int ( Cl P)) by A3, XBOOLE_0:def 4;

      

       A6: x99 in (( Cl ( Int P)) ` ) by A4, A3, XBOOLE_0:def 4;

      ( Int ( Cl P)) c= P by A1;

      hence contradiction by A2, A5, A6, XBOOLE_0:def 5;

    end;

    theorem :: TOPS_1:71

    R is condensed implies ( Int R) is condensed & ( Cl R) is condensed

    proof

      ( Cl ( Int R)) c= ( Cl R) by Th16, PRE_TOPC: 19;

      then

       A1: ( Int ( Cl ( Int R))) c= ( Int ( Cl R)) by Th19;

      

       A2: R c= ( Cl R) by PRE_TOPC: 18;

      then (( Cl R) ` ) c= (R ` ) by SUBSET_1: 12;

      then ( Cl (( Cl R) ` )) c= ( Cl (R ` )) by PRE_TOPC: 19;

      then (( Cl (R ` )) ` ) c= (( Cl (( Cl R) ` )) ` ) by SUBSET_1: 12;

      then

       A3: ( Cl ( Int R)) c= ( Cl (( Cl (( Cl R) ` )) ` )) by PRE_TOPC: 19;

      assume

       A4: R is condensed;

      then

       A5: R c= ( Cl ( Int R));

      then ( Cl R) c= ( Cl ( Cl ( Int R))) by PRE_TOPC: 19;

      then

       A6: ( Cl R) c= ( Cl ( Int ( Cl R))) by A3;

      

       A7: ( Int ( Cl R)) c= R by A4;

      then ( Int ( Int ( Cl R))) c= ( Int R) by Th19;

      then

       A8: ( Int ( Cl ( Int R))) c= ( Int R) by A1;

      ( Int R) c= R by Th16;

      then

       A9: ( Int R) c= ( Cl ( Int ( Int R))) by A5;

      ( Int ( Cl ( Cl R))) c= ( Cl R) by A7, A2;

      hence thesis by A9, A6, A8;

    end;