The Mizar article:

Subsets of Topological Spaces

by
Miroslaw Wysocki, and
Agata Darmochwal

Received April 28, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: TOPS_1
[ MML identifier index ]


environ

 vocabulary BOOLE, SUBSET_1, PRE_TOPC, TOPS_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
 constructors PRE_TOPC, MEMBERED;
 clusters PRE_TOPC, STRUCT_0, MEMBERED, ZFMISC_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0;
 theorems PRE_TOPC, TARSKI, SUBSET_1, STRUCT_0, XBOOLE_0, XBOOLE_1;

begin

 reserve TS for 1-sorted,
         K, Q for Subset of TS;

canceled;

theorem
   K \/ [#] TS = [#] TS
  proof
    K \/ [#] TS = K \/ (the carrier of TS) by PRE_TOPC:def 3;
  then K \/ [#] TS = the carrier of TS by XBOOLE_1:12;
  hence thesis by PRE_TOPC:def 3;
  end;

canceled 5;

theorem Th8:
 ([#]TS)` = {} TS
  proof
    ([#]TS)` = [#] TS \ [#] TS by PRE_TOPC:17
      .= {} TS by XBOOLE_1:37;
  hence thesis;
  end;

canceled 11;

theorem Th20:
 K c= Q iff K misses Q`
 proof
 hereby assume K c= Q;
   then K \ Q = {} by XBOOLE_1:37;
   then K /\ Q` = {} by SUBSET_1:32;
   hence K misses Q` by XBOOLE_0:def 7;
 end;
 assume K misses Q`;
 then K /\ Q` = {} by XBOOLE_0:def 7;
 then K \ Q = {} by SUBSET_1:32;
 hence thesis by XBOOLE_1:37;
 end;

theorem Th21:
 K` = Q` implies K = Q
  proof
    K`` = K & Q`` = Q;
  hence thesis;
  end;

::
::    CLOSED AND OPEN SETS, CLOSURE OF SET
::

 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 Th22:
 {} TS is closed
 proof
  A1: [#] TS = the carrier of TS by PRE_TOPC:def 3;
    the carrier of TS in the topology of TS by PRE_TOPC:def 1;
  then A2: [#] TS is open by A1,PRE_TOPC:def 5;
    [#] TS = [#] TS \ {} TS;
  hence thesis by A2,PRE_TOPC:def 6;
 end;

definition let T be TopSpace;
 cluster {}T -> closed;
coherence by Th22;
end;

canceled 3;

theorem Th26:
 Cl Cl T = Cl T
  proof
  thus Cl Cl T c= Cl T
   proof
   let x; assume A1: x in Cl Cl T;
   then reconsider p=x as Point of GX;
     for C being Subset of GX st C is closed
    holds (T c= C implies p in C)
    proof
    let C be Subset of GX; assume A2: C is closed;
    assume T c= C;
    then Cl T c= Cl C by PRE_TOPC:49;
    then Cl T c= C by A2,PRE_TOPC:52;
    hence p in C by A1,A2,PRE_TOPC:45;
    end;
   hence thesis by A1,PRE_TOPC:45;
   end;
   thus Cl T c= Cl Cl T by PRE_TOPC:48;
  end;

theorem Th27:
 Cl([#] GX) = [#] GX
proof
 thus Cl([#] GX) c= [#] GX by PRE_TOPC:14;
 thus ([#] GX) c= Cl([#] GX) by PRE_TOPC:48;
 end;

Lm1: Cl P is closed
      proof
         Cl Cl P = Cl P by Th26;
       hence thesis by PRE_TOPC:52;
      end;

definition let T be TopSpace, P be Subset of T;
 cluster Cl P -> closed;
coherence by Lm1;
end;

canceled;

theorem Th29:
 R is closed iff R` is open
 proof
   R is closed iff [#] GX \ R is open by PRE_TOPC:def 6;
 hence thesis by PRE_TOPC:17;
 end;

definition let T be TopSpace, R be closed Subset of T;
 cluster R` -> open;
coherence by Th29;
end;

theorem Th30:
 R is open iff R` is closed
 proof
   R` is closed iff R`` is open by Th29;
 hence thesis;
 end;

definition let T be TopSpace;
 cluster open Subset of T;
existence
  proof
    consider R being closed Subset of T;
    take R`;
    thus thesis;
  end;
end;

definition let T be TopSpace, R be open Subset of T;
 cluster R` -> closed;
coherence by Th30;
end;

theorem
   S is closed & T c= S implies Cl T c= S
 proof
  assume A1: S is closed & T c= S;
     then Cl S = S by PRE_TOPC:52;
   hence thesis by A1,PRE_TOPC:49;
 end;

theorem Th32:
 Cl K \ Cl L c= Cl(K \ L)
 proof
  let x;
  assume x in (Cl K \ Cl L);
then A1: x in Cl K & not x in Cl L by XBOOLE_0:def 4;
    Cl K \/ Cl L = Cl (K \/ L) by PRE_TOPC:50
        .= Cl((K \ L) \/ L) by XBOOLE_1:39
        .= Cl(K \ L) \/ Cl L by PRE_TOPC:50;
  then (x in Cl K \/ Cl L iff x in Cl(K \ L) or x in Cl L) by XBOOLE_0:def 2;
  hence x in Cl(K \ L) by A1,XBOOLE_0:def 2;
 end;

canceled;

theorem Th34:
 R is closed & S is closed implies Cl(R /\ S) = Cl R /\ Cl S
 proof
  assume R is closed & S is closed;
   then A1: R = Cl R & S = Cl S by PRE_TOPC:52;
     A2: Cl(R /\ S) c= Cl R /\ Cl S by PRE_TOPC:51;
     Cl R /\ Cl S c= Cl(R /\ S) by A1,PRE_TOPC:48;
  hence thesis by A2,XBOOLE_0:def 10;
 end;

theorem Th35:
 P is closed & Q is closed implies P /\ Q is closed
proof
 assume P is closed & Q is closed;
 then P = Cl P & Q = Cl Q by PRE_TOPC:52;
  then Cl(P /\ Q) = P /\ Q by Th34;
 hence thesis;
end;

theorem Th36:
 P is closed & Q is closed implies P \/ Q is closed
proof
 assume P is closed & Q is closed;
 then P = Cl P & Q = Cl Q by PRE_TOPC:52;
 then Cl(P \/ Q) = P \/ Q by PRE_TOPC:50;
 hence thesis;
end;

theorem
   P is open & Q is open implies P \/ Q is open
proof 
A1: (P`) /\ Q` = (P \/ Q)` by SUBSET_1:29;
 assume P is open & Q is open;
 then P` is closed & Q` is closed by Th30;
 then (P \/ Q)` is closed by A1,Th35;
 hence thesis by Th30;
end;

theorem Th38:
 P is open & Q is open implies P /\ Q is open
proof 
A1: (P`) \/ Q` = (P /\ Q)` by SUBSET_1:30;
 assume P is open & Q is open;
 then P` is closed & Q` is closed by Th30;
 then (P /\ Q)` is closed by A1,Th36;
 hence thesis by Th30;
end;

 Lm2:
 for GX being non empty 1-sorted, R being Subset of GX
 for p being Element of GX holds p in R` iff not p in R
 proof let GX be non empty 1-sorted, R be Subset of GX;
  thus thesis by SUBSET_1:50,54;
 end;

theorem Th39:
 for GX being non empty TopSpace, R being Subset of GX,
   p being Point of GX holds
  p in Cl R iff
 for T being 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 being 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 SUBSET_1:30;
    R /\ T = {} GX by A4,XBOOLE_0:def 7;
  then (R /\ T)` = [#] GX by PRE_TOPC:27;
  then A6: R c= R` \/ T` by A5,PRE_TOPC:14;
  A7: R c= T`
  proof let x;
  assume A8: x in R;
  then x in R` or x in T` by A6,XBOOLE_0:def 2;
  hence x in T` by A8,Lm2;
  end;
    T` is closed by A2,Th30;
  then Cl(T`) = T` by PRE_TOPC:52;
  then Cl R c= T` by A7,PRE_TOPC:49;
 hence contradiction by A1,A3,Lm2;
 end;
 assume
A9: for T being Subset of GX st T is open & p in T holds R meets T;
 assume not p in Cl R;
  then A10: p in (Cl R)` by Lm2;
    A11: R meets (Cl R)` by A9,A10;
       R c= Cl R by PRE_TOPC:48;
     then (Cl R)` c= R` by PRE_TOPC:19;
    then A12: R /\ (Cl R)` c= R /\ R` by XBOOLE_1:26;
     R misses R` by PRE_TOPC:26;
   then R /\ R` = {} by XBOOLE_0:def 7;
   then R /\ (Cl R)` = {} by A12,XBOOLE_1:3;
 hence contradiction by A11,XBOOLE_0:def 7;
end;

theorem Th40:
 Q is open implies Q /\ Cl K c= Cl(Q /\ K)
proof
 assume A1: Q is open;
  let x;
   assume A2: x in Q /\ Cl K;
    then A3: x in Q by XBOOLE_0:def 3;
    A4: x in Cl K by A2,XBOOLE_0:def 3;
 reconsider p''= x as Point of TS by A2;
A5: TS is non empty by A2,STRUCT_0:def 1;
     for Q1 being Subset of TS holds Q1 is open implies
   (p'' in Q1 implies (Q /\ K) meets Q1)
       proof
        let Q1 be Subset of TS; assume A6: Q1 is open;
          assume p'' in Q1;
            then A7: p'' in Q1 /\ Q by A3,XBOOLE_0:def 3;
A8:         Q1 /\ Q is open by A1,A6,Th38;
A9:         K /\ (Q1 /\ Q) = (Q /\ K) /\ Q1 by XBOOLE_1:16;
              K meets (Q1 /\ Q) by A4,A5,A7,A8,Th39;
            then K /\ (Q1 /\ Q) <> {} by XBOOLE_0:def 7;
       hence (Q /\ K) meets Q1 by A9,XBOOLE_0:def 7;
     end;
   hence x in Cl(Q /\ K) by A5,Th39;
end;

theorem
   Q is open implies Cl(Q /\ Cl K) = Cl(Q /\ K)
proof
 assume Q is open;
  then Q /\ Cl K c= Cl(Q /\ K) by Th40;
   then Cl(Q /\ Cl K) c= Cl(Cl(Q /\ K)) by PRE_TOPC:49;
  then A1: Cl(Q /\ Cl K) c= Cl(Q /\ K) by Th26;
    Cl (Q /\ K) c= Cl(Q /\ Cl K)
 proof let x;
  assume A2: x in Cl(Q /\ K);
 then reconsider p''= x as Point of TS;
A3: TS is non empty by A2,STRUCT_0:def 1;
    for Q1 being Subset of TS holds Q1 is open implies
   (p'' in Q1 implies (Q /\ Cl K) meets Q1)
     proof let Q1 be Subset of TS; assume A4: Q1 is open;
      assume p'' in Q1;
        then (Q /\ K) meets Q1 by A2,A3,A4,Th39;
then A5:     (Q /\ K) /\ Q1 <> {} by XBOOLE_0:def 7;
          K c= Cl K by PRE_TOPC:48;
        then Q /\ K c= Q /\ Cl K by XBOOLE_1:26;
        then (Q /\ K) /\ Q1 c= (Q /\ Cl K) /\ Q1 by XBOOLE_1:26;
        then (Q /\ Cl K) /\ Q1 <> {} by A5,XBOOLE_1:3;
        hence thesis by XBOOLE_0:def 7;
       end;
     hence x in Cl(Q /\ Cl K) by A3,Th39;
   end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

::
::    INTERIOR OF A SET
::

 definition let GX be TopStruct, R be Subset of GX;
  func Int R -> Subset of GX equals
     :Def1: (Cl R`)`;
   coherence;
 end;

canceled;

theorem Th43:
 Int([#] TS) = [#] TS
  proof
    Int ([#] TS) = (Cl ([#]TS)`)` by Def1
       .= (Cl {} TS)` by Th8
       .= ({} TS)` by PRE_TOPC:52;
  hence thesis by PRE_TOPC:27;
   end;

theorem Th44:
 Int T c= T
proof
 let x;
  assume A1: x in Int T;
  A2: Int T = (Cl T`)` by Def1;
  reconsider x''= x as Point of GX by A1;
A3: GX is non empty by A1,STRUCT_0:def 1;
     T` c= Cl T` by PRE_TOPC:48;
  then not x'' in T` by A1,A2,A3,Lm2;
  hence x in T by A3,Lm2;
 end;

theorem Th45:
 Int Int T = Int T
   proof
     Int T = (Cl T`)` by Def1;
    then Int Int T = (Cl (Cl T`)``)` by Def1
           .= (Cl T`)` by Th26;
   hence thesis by Def1;
   end;

theorem Th46:
 Int K /\ Int L = Int(K /\ L)
proof
   Int K = (Cl K`)` by Def1;
 then Int K /\ Int L = ((Cl K`)`) /\ (Cl L`)` by Def1
         .= (Cl K` \/ Cl L`)` by SUBSET_1:29
         .= (Cl(K` \/ L`))` by PRE_TOPC:50
         .= (Cl (K /\ L)`)` by SUBSET_1:30;
 hence thesis by Def1;
end;

theorem Th47:
 Int({} GX) = {} GX
 proof
   {} GX = ([#] GX)` by Th8
   .= (Cl [#] GX)` by Th27
   .= (Cl ({}GX)`)` by PRE_TOPC:27;
 hence thesis by Def1;
 end;

theorem Th48:
 T c= W implies Int T c= Int W
 proof
  assume T c= W;
  then  W` c= T` by PRE_TOPC:19;
  then Cl W` c= Cl T` by PRE_TOPC:49;
  then A1: (Cl T`)` c= (Cl W`)` by PRE_TOPC:19;
     Int T = (Cl T`)` by Def1;
 hence thesis by A1,Def1;
end;

theorem Th49:
 Int T \/ Int W c= Int(T \/ W)
  proof
  A1: Int T \/ Int W = Int T \/ (Cl W`)` by Def1
          .= ((Cl T`)`) \/ (Cl W`)` by Def1
          .= ((Cl T`) /\ Cl W`)` by SUBSET_1:30;
          Cl(T` /\  W`) c= Cl T` /\ Cl W` by PRE_TOPC:51;
     then Int T \/ Int W c= (Cl(T` /\ W`))` by A1,PRE_TOPC:19;
   then Int T \/ Int W c= (Cl((T \/ W)`))` by SUBSET_1:29;
   then Int T \/ Int W c= (Cl(T \/ W)`)`;
  hence thesis by Def1;
  end;

theorem
   Int(K \ L) c= Int K \ Int L
  proof
  A1: Int(K \ L) = (Cl (K \ L)`)` by Def1
         .= (Cl (K /\ L`)`)` by SUBSET_1:32
         .= (Cl((K`) \/ L``))` by SUBSET_1:30
         .= ((Cl K` \/ Cl L))` by PRE_TOPC:50
         .= ((Cl K`)`) /\ (Cl L)` by SUBSET_1:29
         .= ((Cl L)`) /\ Int K by Def1;
       L c= Cl L by PRE_TOPC:48;
      then A2: (Cl L)` c= L` by PRE_TOPC:19;
        Int L c= L by Th44;
      then L` c= (Int L)` by PRE_TOPC:19;
      then L` c= (Int L)`;
      then ((Cl L)`) c= (Int L)` by A2,XBOOLE_1:1;
    then Int(K \ L) c= Int K /\ (Int L)` by A1,XBOOLE_1:26;
   hence thesis by SUBSET_1:32;
  end;

theorem Th51:
 Int K is open
 proof
        (Int K)` = (Cl K`)`` by Def1
       .= Cl K`;
 hence thesis by Th30;
end;

definition let T be TopSpace, K be Subset of T;
 cluster Int K -> open;
coherence by Th51;
end;

theorem Th52:
 {} TS is open
    proof
      Int({} TS) = {} TS by Th47;
    hence thesis;
    end;

theorem Th53:
 [#] TS is open
    proof
      Int([#] TS) = [#] TS by Th43;
    hence thesis;
    end;

definition let T be TopSpace;
 cluster {}T -> open;
coherence by Th52;
 cluster [#]T -> open;
coherence by Th53;
end;

definition let T be TopSpace;
 cluster open closed Subset of T;
existence
  proof
   take [#]T;
   thus thesis;
  end;
end;

definition let T be non empty TopSpace;
 cluster non empty open closed Subset of T;
existence
  proof
   take [#]T;
   thus thesis;
  end;
end;

theorem Th54:
 x in Int K iff ex Q st Q is open & Q c= K & x in Q
 proof
  hereby assume A1: x in Int K;
  take Q = Int K;
  thus Q is open & Q c= K & x in Q by A1,Th44;
  end;
  given Q such that
  A2: Q is open and
  A3: Q c= K and
  A4: x in Q;
     K` c= Q` by A3,PRE_TOPC:19;
   then A5: Cl K` c= Cl Q` by PRE_TOPC:49;
     Q` is closed by A2,Th30;
    then Cl K` c= Q` by A5,PRE_TOPC:52;
    then  Q`` c= (Cl K`)` by PRE_TOPC:19;
    then Q c= (Cl K`)`;
   then Q c= Int K by Def1;
  hence x in Int K by A4;
 end;

theorem Th55:
 (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 Th30;
    then A1: Cl R` = R` by PRE_TOPC:52;
      Int R = (Cl R`)` by Def1
      .= R by A1;
   hence Int R = R;
  end;
  thus thesis;
 end;

theorem
   S is open & S c= T implies S c= Int T
 proof
  assume A1: S is open & S c= T;
  then Int S = S by Th55;
  hence thesis by A1,Th48;
 end;

theorem
   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;
      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 Th54;
   end;
   hence thesis by TARSKI:2;
  end;

theorem Th58:
 Cl Int T = Cl Int Cl Int T
 proof
    Int T c= Cl Int T by PRE_TOPC:48;
  then Int Int T c= Int Cl Int T by Th48;
   then Int T c= Int Cl Int T by Th45;
 then A1: Cl Int T c= Cl Int Cl Int T by PRE_TOPC:49;
    Int Cl Int T c= Cl Int T by Th44;
   then Cl Int Cl Int T c= Cl Cl Int T by PRE_TOPC:49;
  then Cl Int Cl Int T c= Cl Int T by Th26;
 hence thesis by A1,XBOOLE_0:def 10;
 end;

theorem
   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 Th55
          .= Cl Int R by Th58
          .= Cl R by A1,Th55;
 hence thesis;
 end;

::
::    FRONTIER OF A SET
::

 definition let GX be TopStruct, R be Subset of GX;
  func Fr R -> Subset of GX equals
     :Def2: Cl R /\ Cl R`;
   coherence;
 end;

canceled;

theorem Th61:
 for GX being non empty TopSpace, R being Subset of GX,
   p being Point of GX holds p in Fr R iff
 (for S being 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;
A1: Fr R = (Cl R) /\ (Cl R`) by Def2;
 hereby assume A2: p in Fr R;
  let S be Subset of GX; assume A3:S is open & p in S;
    p in Cl R & p in Cl R` by A1,A2,XBOOLE_0:def 3;
  hence R meets S & R` meets S by A3,Th39;
 end;
 assume A4:for S being Subset of GX st S is open & p in S
    holds R meets S & R` meets S;
 then for S being Subset of GX st S is open & p in S holds R meets S;
 then A5:p in Cl R by Th39;
   for S being Subset of GX st S is open & p in S
   holds R` meets S by A4;
 then p in Cl R` by Th39;
 hence thesis by A1,A5,XBOOLE_0:def 3;
end;

theorem Th62:
 Fr T = Fr T`
  proof
     Fr T = Cl(T`) /\ Cl(T``) by Def2;
   hence thesis by Def2;
  end;

theorem Th63:
 Fr T c= Cl T
 proof
    Cl T /\ (Cl T`) c= Cl T by XBOOLE_1:17;
  hence thesis by Def2;
 end;

theorem
   Fr T = Cl(T`) /\ T \/ (Cl T \ T)
 proof
   for x holds x in Fr T iff x in ((Cl(T`) /\ T) \/ (Cl T\T))
proof
let x;
 A1: T c= Cl T by PRE_TOPC:48;
 A2: T` c= Cl(T`) by PRE_TOPC:48;
thus x in Fr T implies x in ((Cl(T`) /\ T) \/ (Cl T \ T))
 proof
  assume A3: x in Fr T;
   then reconsider x''= x as Point of GX;
A4: GX is non empty by A3,STRUCT_0:def 1;
     x'' in Cl T /\ Cl(T`) by A3,Def2;
 then x'' in Cl T & x'' in Cl(T`) & x'' in T
     or x'' in Cl T & x'' in Cl(T`) & x'' in T` by A4,Lm2,XBOOLE_0:def 3;
  then x'' in Cl(T`) /\ T or not x'' in T & x'' in Cl T
                     by XBOOLE_0:def 3;
  then x'' in (Cl(T`) /\ T) or x'' in (Cl T \ T) by XBOOLE_0:def 4;
 hence x in (Cl(T`) /\ T) \/ (Cl T \ T) by XBOOLE_0:def 2;
 end;
thus x in ((Cl(T`) /\ T) \/ (Cl T \ T)) implies x in Fr T
 proof
  assume A5: x in (Cl(T`) /\ T) \/ (Cl T \ T);
 then reconsider x''= x as Point of GX;
A6: GX is non empty by A5,STRUCT_0:def 1;
    x'' in (Cl(T`) /\ T) or x'' in (Cl T \ T) by A5,XBOOLE_0:def 2;
  then x'' in Cl(T`) & x'' in T or x'' in Cl T & not x'' in T
                   by XBOOLE_0:def 3,def 4;
 then x'' in Cl(T`) & x'' in T or x'' in Cl T & x'' in T` by A6,Lm2;
   then x'' in Cl T /\ Cl(T`) by A1,A2,XBOOLE_0:def 3;
  hence x in Fr T by Def2;
 end;
end;
hence thesis by TARSKI:2;
end;

theorem Th65:
 Cl T = T \/ Fr T
proof
 A1: Cl T c= T \/ Fr T
 proof
    T c= Cl T by PRE_TOPC:48;
  then A2: Cl T = T \/ (Cl T \ T) by XBOOLE_1:45;
     T \/ (Cl T \ T) c= T \/ (Cl T /\ Cl(T`))
  proof
   let x;
   assume A3: x in T \/ (Cl T \ T);
   then reconsider x''=x as Point of GX;
A4: GX is non empty by A3,STRUCT_0:def 1;
     x'' in T or x'' in Cl T \ T by A3,XBOOLE_0:def 2;
    then A5: x'' in T or (x'' in Cl T & x'' in T`) by A4,Lm2,XBOOLE_0:def 4;
      T` c= Cl(T`) by PRE_TOPC:48;
   then x'' in T or x'' in (Cl T /\ Cl (T`)) by A5,XBOOLE_0:def 3;
   hence x in T \/ (Cl T /\ Cl (T`)) by XBOOLE_0:def 2;
  end;
 hence Cl T c= T \/ Fr T by A2,Def2;
 end;
   T \/ Fr T c= Cl T
 proof
  A6: T \/ Fr T = T \/ (Cl T /\ Cl(T`)) by Def2
           .= (T \/ Cl T) /\ (T \/ Cl (T`)) by XBOOLE_1:24;
     T c= Cl T by PRE_TOPC:48;
    then (T \/ Cl T) /\ (T \/ Cl(T`)) = Cl T /\ (T \/ Cl(T`)) by XBOOLE_1:12;
 hence thesis by A6,XBOOLE_1:17;
 end;
 hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th66:
 Fr(K /\ L) c= Fr K \/ Fr L
  proof
  A1: Fr(K /\ L) = Cl(K /\ L) /\ Cl((K /\ L)`) by Def2
        .= Cl(K /\ L) /\ Cl((K`) \/ L`) by SUBSET_1:30
        .= Cl(K /\ L) /\ (Cl(K`) \/ Cl L`) by PRE_TOPC:50
        .=(Cl(K /\ L) /\ Cl(K`)) \/ (Cl(K /\ L) /\ Cl(L`))
                           by XBOOLE_1:23;
    K /\ L c= K & K /\ L c= L by XBOOLE_1:17;
  then Cl(K /\ L) c= Cl K & Cl(K /\ L) c= Cl L by PRE_TOPC:49;
  then Cl(K /\ L) /\ Cl(K`) c= Cl K /\ Cl(K`) &
    Cl(K /\ L) /\ Cl(L`) c= Cl L /\ Cl(L`) by XBOOLE_1:26;
  then (Cl(K /\ L) /\ Cl(K`)) \/ (Cl(K /\ L) /\ Cl(L`)) c=
          (Cl K /\ Cl(K`)) \/ (Cl L /\ Cl(L`)) by XBOOLE_1:13;
   then Fr(K /\ L) c= Fr K \/ (Cl L /\ Cl(L`)) by A1,Def2;
 hence thesis by Def2;
 end;

theorem Th67:
 Fr(K \/ L) c= Fr K \/ Fr L
  proof
  A1: Fr(K \/ L) = Cl(K \/ L) /\ Cl((K \/ L)`) by Def2
        .= (Cl K \/ Cl L) /\ Cl((K \/ L)`) by PRE_TOPC:50
        .= Cl((K`) /\ L`) /\ (Cl K \/ Cl L) by SUBSET_1:29
        .= (Cl((K`) /\ L`) /\ Cl K) \/ (Cl((K`) /\ L`) /\ Cl L)
                           by XBOOLE_1:23;
      (K`) /\ L` c= K` & (K`) /\ L` c= L` by XBOOLE_1:17;
   then Cl((K`) /\ L`) c= Cl K` & Cl((K`) /\ L`) c= Cl L` by PRE_TOPC:49;
  then Cl((K`) /\ L`) /\ Cl K c= Cl(K`) /\ Cl K &
      Cl((K`) /\ L`) /\ Cl L c= Cl(L`) /\ Cl L by XBOOLE_1:26;
   then Fr(K \/ L) c= (Cl K /\ Cl(K`)) \/ (Cl(L`) /\ Cl L) by A1,XBOOLE_1:13;
   then Fr(K \/ L) c= Fr K \/ (Cl L /\ Cl(L`)) by Def2;
 hence thesis by Def2;
 end;

theorem Th68:
 Fr Fr T c= Fr T
  proof
  A1:Fr(Fr T) = Fr(Cl T /\ Cl(T`)) by Def2
       .= Cl(Cl T /\ Cl(T`)) /\ Cl((Cl T /\ Cl(T`))`) by Def2;
    let x such that A2: x in Fr(Fr T);
     A3: Cl(Cl T /\ Cl(T`)) c= Cl(Cl T) /\ Cl(Cl(T`)) by PRE_TOPC:51;
       x in Cl(Cl T /\ Cl(T`)) by A1,A2,XBOOLE_0:def 3;
      then x in Cl(Cl T) /\ Cl(Cl(T`)) by A3;
      then x in Cl(Cl T) /\ Cl(T`) by Th26;
      then x in Cl T /\ Cl(T`) by Th26;
     hence x in Fr T by Def2;
  end;

theorem
   R is closed implies Fr R c= R
 proof
 assume R is closed;
  then A1: Cl R = R by PRE_TOPC:52;
  let x;
   assume A2: x in Fr R;
     Fr R = Cl R /\ Cl(R`) by Def2;
   hence x in R by A1,A2,XBOOLE_0:def 3;
 end;

Lm3: Fr K c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L)
  proof
    let x; assume A1: x in Fr K;
    then reconsider x''= x as Point of TS;
A2:   TS is non empty by A1,STRUCT_0:def 1;
    assume not x in (Fr(K \/ L) \/ Fr(K /\ L)) \/ (Fr K /\ Fr L);
       then A3: not x'' in (Fr(K \/ L) \/ Fr(K /\ L))
        & not x'' in (Fr K /\ Fr L) by XBOOLE_0:def 2;
       then A4: not x'' in Fr(K \/ L) & not x'' in Fr(K /\ L)
         & not x'' in (Fr K /\ Fr L) by XBOOLE_0:def 2;
  then consider Q1 being Subset of TS such that
   A5: Q1 is open and A6: x'' in Q1 and
   A7: (K \/ L) misses Q1 or ((K \/ L)`) misses Q1 by A2,Th61;
   A8: (K \/ L) /\ Q1 = {} or ((K \/ L)`) /\ Q1 = {} by A7,XBOOLE_0:def 7;
  (L`) /\ (K`) = (K \/ L)` by SUBSET_1:29;
  then A9: (K /\ Q1) \/ (Q1 /\ L)={} or (L`) /\ ((K`) /\ Q1)={} by A8,XBOOLE_1:
16,23;
     K meets Q1 by A1,A2,A5,A6,Th61;
then A10:K /\ Q1 <> {} by XBOOLE_0:def 7;
  consider Q2 being Subset of TS such that
  A11: Q2 is open and A12: x'' in Q2 and
    A13: (K /\ L) misses Q2 or ((K /\ L)`) misses Q2 by A2,A4,Th61;
    A14: (K /\ L) /\ Q2 = {} or ((K /\ L)`) /\ Q2 = {} by A13,XBOOLE_0:def 7;
  (L`) \/ (K`) = (K /\ L)` by SUBSET_1:30;
  then A15: (K /\ Q2) /\ L={} or ((K`) /\ Q2) \/ (Q2 /\
 (L`))={} by A14,XBOOLE_1:16,23;
     (K`) meets Q2 by A1,A2,A11,A12,Th61;
then A16:     (K`) /\ Q2 <> {} by XBOOLE_0:def 7;
       not x'' in Fr L by A1,A3,XBOOLE_0:def 3;
    then consider Q3 being Subset of TS such that
    A17: Q3 is open and A18: x'' in Q3 and
    A19: L misses Q3 or (L`) misses Q3 by A2,Th61;
   A20: now assume L /\ Q3 = {};
     then Q3 /\ L`` = {};
     then Q3 misses L`` by XBOOLE_0:def 7;
     then A21:Q3 c= L` by Th20;
       ((K`) /\ Q1) /\ ((L`) /\ Q3) = {} /\ Q3 by A9,A10,XBOOLE_1:15,16;
     then ((K`) /\ Q1) /\ Q3 = {} by A21,XBOOLE_1:28;
    hence (K`) /\ (Q1 /\ Q3) = {} by XBOOLE_1:16;
    end;
    A22: Q1 /\ Q3 is open by A5,A17,Th38;
  x'' in Q1 /\ Q3 by A6,A18,XBOOLE_0:def 3;
    then (K`) meets (Q1 /\ Q3) by A1,A2,A22,Th61;
    then A23:Q3 c= L by A19,A20,Th20,XBOOLE_0:def 7;
      (K /\ (Q2 /\ L)) /\ Q3 = {} /\ Q3 by A15,A16,XBOOLE_1:15,16;
    then K /\ ((Q2 /\ L) /\ Q3) = {} by XBOOLE_1:16;
    then K /\ (Q2 /\ (L /\ Q3)) = {} by XBOOLE_1:16;
    then K /\ (Q2 /\ Q3) = {} by A23,XBOOLE_1:28;
    then A24: K misses (Q2 /\ Q3) by XBOOLE_0:def 7;
    A25: Q2 /\ Q3 is open by A11,A17,Th38;
     x'' in Q2 /\ Q3 by A12,A18,XBOOLE_0:def 3;
   hence contradiction by A1,A2,A24,A25,Th61;
  end;

theorem
   Fr K \/ Fr L = Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L)
  proof
   A1: Fr K \/ Fr L c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L)
     proof
    A2: Fr K c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L) by Lm3;
    Fr L c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L) by Lm3;
   hence thesis by A2,XBOOLE_1:8;
   end;
     Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L) c= Fr K \/ Fr L
     proof
   let x; assume
             x in (Fr(K \/ L) \/ Fr(K /\ L)) \/ (Fr K /\ Fr L);
       then A3: x in (Fr(K \/ L) \/ Fr(K /\ L)) or x in (Fr K /\ Fr L)
                           by XBOOLE_0:def 2;
      A4: now assume A5: x in Fr(K \/ L);
         Fr(K \/ L) c= (Fr K \/ Fr L) by Th67;
      hence x in (Fr K \/ Fr L) by A5;
     end;
     A6: now assume A7: x in Fr(K /\ L);
        Fr(K /\ L) c= (Fr K \/ Fr L) by Th66;
      hence x in (Fr K \/ Fr L) by A7;
     end;
       now assume x in (Fr K /\ Fr L);
      then x in Fr K & x in Fr L by XBOOLE_0:def 3;
      hence x in (Fr K \/ Fr L) by XBOOLE_0:def 2;
     end;
     hence thesis by A3,A4,A6,XBOOLE_0:def 2;
     end;
   hence thesis by A1,XBOOLE_0:def 10;
  end;

theorem
   Fr Int T c= Fr T
 proof
   let x;
   assume A1: x in Fr(Int T);
      Fr(Int T) = Fr((Cl T`)`) by Def1
           .= Cl((Cl T`)`) /\ Cl(((Cl T`)`)`) by Def2
           .= Cl((Cl T`)`) /\ Cl(T`) by Th26;
   then A2: x in Cl((Cl T`)`) & x in Cl(T`) by A1,XBOOLE_0:def 3;
      Int T = (Cl T`)` by Def1;
   then (Cl T`)` c= T by Th44;
   then Cl((Cl T`)`) c= Cl T by PRE_TOPC:49;
    then x in (Cl T) /\ Cl(T`) by A2,XBOOLE_0:def 3;
    hence x in Fr T by Def2;
 end;

theorem
   Fr Cl T c= Fr T
  proof
  A1: Fr Cl T = Cl(Cl T) /\ Cl((Cl T)`) by Def2
       .= Cl((Cl T)`) /\ Cl T by Th26;
      T c= Cl T by PRE_TOPC:48;
       then (Cl T)` c= T` by PRE_TOPC:19;
     then Cl((Cl T)`) c= Cl(T`) by PRE_TOPC:49;
   then Fr(Cl T) c= Cl T /\ Cl(T`) by A1,XBOOLE_1:26;
  hence thesis by Def2;
  end;

theorem Th73:
 Int T misses Fr T
 proof
A1: ((Cl T`)`) misses (Cl T \ ((Cl T`)`)) by XBOOLE_1:79;
    Fr T = Cl T /\ (((Cl T`)`)`) by Def2
     .= Cl T \ ((Cl T`)`) by SUBSET_1:32;
   then Int T /\ Fr T = ((Cl T`)`) /\ (Cl T \ ((Cl T`)`)) by Def1
           .= {} by A1,XBOOLE_0:def 7;
  hence thesis by XBOOLE_0:def 7;
 end;

theorem Th74:
 Int T = T \ Fr T
  proof
A1:  (Cl T`)` \/ (Cl T)` = (Cl T /\ Cl T`)` by SUBSET_1:30;
   A2: T \ Fr T = T \ (Cl T /\ Cl(T`)) by Def2
         .= T /\ ((Cl T`)` \/ (Cl T)`) by A1,SUBSET_1:32
         .= (T /\ (Cl T)`) \/ (T /\ (Cl T`)`) by XBOOLE_1:23
         .= (T /\ (Cl T)`) \/ (T /\ Int T) by Def1;
        Int T c= T by Th44;
   then A3: Int T = T /\ Int T by XBOOLE_1:28;
     T c= Cl T by PRE_TOPC:48;
   then T misses (Cl T)` by Th20;
   then T \ Fr T = {} \/ Int T by A2,A3,XBOOLE_0:def 7;
  hence thesis;
 end;

Lm4: Fr T = Cl T \ Int T
 proof
    Fr T = Cl T /\ ((Cl T`)`)` by Def2
    .= Cl T /\ (Int T)` by Def1
    .= Cl T \ Int T by SUBSET_1:32;
  hence thesis;
 end;

Lm5: Cl Fr K = Fr K
 proof
  A1: Cl Fr K = Cl(Cl K /\ Cl(K`)) by Def2;
  A2: Cl Cl K = Cl K by Th26;
        Cl Cl K` = Cl K` by Th26;
   then Cl(Cl K /\ Cl(K`)) = Cl K /\ Cl(K`) by A2,Th34;
  hence thesis by A1,Def2;
 end;

Lm6: Int Fr Fr K = {}
 proof
   assume A1: Int Fr Fr K <> {};
   consider x' being Element of Int(Fr(Fr K));
   reconsider x = x' as Point of TS by A1,TARSKI:def 3;
     x in Int(Fr(Fr K)) by A1;
then A2:  TS is non empty by STRUCT_0:def 1;
   A3: Int(Fr(Fr K)) c= Fr(Fr K) by Th44;
    then A4: x in Fr(Fr K) by A1,TARSKI:def 3;
       Fr(Fr K) c= Fr K by Th68;
     then A5: Int(Fr(Fr K)) c= Fr K by A3,XBOOLE_1:1;
       (Fr K)` meets Int(Fr(Fr K)) by A1,A2,A4,Th61;
  then A6: (Fr K)` /\ Int(Fr(Fr K)) <> {} by XBOOLE_0:def 7;
   A7: (Fr K)` /\ Int(Fr(Fr K)) c= (Fr K)` /\ Fr K by A5,XBOOLE_1:26;
A8:Fr K misses (Fr K)` by PRE_TOPC:26;
     (Fr K)` /\ Fr K <> {} by A6,A7,XBOOLE_1:3;
   hence contradiction by A8,XBOOLE_0:def 7;
 end;

theorem
   Fr Fr Fr K = Fr Fr K
 proof
 A1: Int Fr Fr K = {} by Lm6;
     Fr Fr Fr K = Cl(Fr(Fr K)) \ Int(Fr(Fr K)) by Lm4
         .= Fr Fr K by A1,Lm5;
 hence thesis;
end;

Lm7: for X, Y, Z being 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; assume x in X;
  then x in Z & not x in Y by A1,A2,XBOOLE_0:def 4;
  hence x in Z \ Y by XBOOLE_0:def 4;
 end;

theorem Th76:
 P is open iff Fr P = Cl P \ P
  proof
   hereby assume P is open;
    then P = Int P by Th55;
    hence Fr P = Cl P \ P by Lm4;
   end;
   assume A1: Fr P = Cl P \ P;
A2: Fr P misses (Fr P)` by PRE_TOPC:26;
A3:   Fr P c= Cl P & P c= Cl P by Th63,PRE_TOPC:48;
     Cl P \ Fr P = (P \/ Fr P) \ Fr P by Th65
       .= (Fr P)` /\ (P \/ Fr P) by SUBSET_1:32
       .= (P /\ (Fr P)`) \/ ((Fr P)` /\ (Fr P)) by XBOOLE_1:23
       .= (P \ Fr P) \/ (Fr P /\ (Fr P)`) by SUBSET_1:32
       .= Int P \/ (Fr P /\ (Fr P)`) by Th74
       .= Int P \/ {} TS by A2,XBOOLE_0:def 7
       .= Int P;
    then P c= Int P & Int P c= P by A1,A3,Lm7,Th44;
   hence thesis by XBOOLE_0:def 10;
  end;

theorem Th77:
 P is closed iff Fr P = P \ Int P
  proof
  thus P is closed implies Fr P = P \ Int P
   proof
   assume P is closed;
   then P = Cl P by PRE_TOPC:52;
   hence thesis by Lm4;
   end;
  assume A1: Fr P = P \ Int P;
A2:(P`) misses P by PRE_TOPC:26;
    Int P c= P by Th44;
    then (P`) /\ Int P c= (P`) /\ P by XBOOLE_1:26;
    then (P`) /\ Int P c= {} TS by A2,XBOOLE_0:def 7;
    then A3: (P`) /\ Int P ={} the carrier of TS by XBOOLE_1:3;
A4:   (P``) \/ (Int P)` = ((P`) /\ Int P)` by SUBSET_1:30;
      Cl P = P \/ (P \ Int P) by A1,Th65
      .= P \/ ((Int P)` /\ P) by SUBSET_1:32
      .= (P \/ (Int P)`) /\ (P \/ P) by XBOOLE_1:24
      .= ({} TS)` /\ P by A3,A4
      .= ([#] TS) /\ P by PRE_TOPC:27
      .= P by PRE_TOPC:15;
   hence thesis;
 end;

::
::    DENSE, BOUNDARY AND NOWHEREDENSE SETS
::

 definition let GX be TopStruct, R be Subset of GX;
   attr R is dense means
   :Def3: Cl R = [#] GX;
 end;

canceled;

theorem
   R is dense & R c= S implies S is dense
  proof
   assume that A1: R is dense and A2:R c= S;
    A3: Cl R = [#] GX by A1,Def3;
    A4: Cl S c= [#] GX by PRE_TOPC:14;
       [#] GX c= Cl S by A2,A3,PRE_TOPC:49;
    then [#] GX = Cl S by A4,XBOOLE_0:def 10;
   hence thesis by Def3;
  end;

theorem Th80:
 P is dense iff (for Q st Q <> {} & Q is open holds P meets Q)
 proof
  hereby assume A1: P is dense;
  let Q;
  assume that A2: Q<>{} and A3: Q is open;
  A4: Cl P = [#] TS by A1,Def3;
  consider x being Element of Q;
    x in Q by A2;
then A5: TS is non empty by STRUCT_0:def 1;
     x is Point of TS by A2,TARSKI:def 3;
    then x in Cl P by A4,A5,PRE_TOPC:13;
   hence P meets Q by A2,A3,A5,Th39;
 end;
  assume A6: for Q st Q <> {} & Q is open holds P meets Q;
   A7: Cl P c= [#] TS by PRE_TOPC:14;
     [#] TS c= Cl P
   proof
    let x be set; assume
A8:   x in [#] TS;
then A9:   TS is non empty by STRUCT_0:def 1;
      for C be Subset of TS st C is open & x in C holds P meets C by A6;
    hence x in Cl P by A8,A9,Th39;
   end;
  then Cl P = [#] TS by A7,XBOOLE_0:def 10;
  hence thesis by Def3;
 end;

theorem
   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 set; assume A3: x in Cl Q;
then A4: TS is non empty by STRUCT_0:def 1;
     now let Q1 be Subset of TS; assume A5: Q1 is open;
    assume x in Q1;
   then Q meets Q1 by A3,A4,A5,Th39;
then A6:   Q /\ Q1 <> {} by XBOOLE_0:def 7;
A7:   Q /\ Q1 is open by A2,A5,Th38;
A8: P /\ (Q /\ Q1) = (Q /\ P) /\ Q1 by XBOOLE_1:16;
      P meets (Q /\ Q1) by A1,A6,A7,Th80;
    then P /\ (Q /\ Q1) <> {} by XBOOLE_0:def 7;
    hence (Q /\ P) meets Q1 by A8,XBOOLE_0:def 7;
   end;
  hence thesis by A3,A4,Th39;
 end;
   Q /\ P c= Q by XBOOLE_1:17;
 hence Cl(Q /\ P) c= Cl Q by PRE_TOPC:49;
 end;

theorem
   P is dense & Q is dense & Q is open implies P /\ Q is dense
 proof
  assume that A1:P is dense and A2:Q is dense and A3:Q is open;
     Cl P = [#] TS by A1,Def3;
    then Cl P /\ Cl Q = ([#] TS) /\ ([#] TS) by A2,Def3
            .= [#] TS;
    then A4: Cl(P /\ Q) c= [#] TS by PRE_TOPC:51;
       [#] TS c= Cl(P /\ Q)
     proof
     let x be set; assume
A5:     x in [#] TS;
then A6: TS is non empty by STRUCT_0:def 1;
        now let C be Subset of TS; assume A7: C is open;
       assume x in C;
       then Q meets C by A2,A7,Th80;
       then A8:Q /\ C <> {} by XBOOLE_0:def 7;
         Q /\ C is open by A3,A7,Th38;
       then P meets (Q /\ C) by A1,A8,Th80;
       then P /\ (Q /\ C) <> {} by XBOOLE_0:def 7;
       then (P /\ Q) /\ C <> {} by XBOOLE_1:16;
       hence (P /\ Q) meets C by XBOOLE_0:def 7;
      end;
    hence thesis by A5,A6,Th39;
    end;
    then Cl(P /\ Q) = [#] TS by A4,XBOOLE_0:def 10;
   hence thesis by Def3;
  end;

 definition let GX be TopStruct, R be Subset of GX;
   attr R is boundary means
   :Def4: R` is dense;
 end;

canceled;

theorem Th84:
 R is boundary iff Int R = {}
 proof
   R is boundary iff R` is dense by Def4;
 then R is boundary iff Cl(R`) = [#] GX by Def3;
  then R is boundary iff (Cl R`)` = ([#] GX)` by Th21;
  then R is boundary iff (Cl R`)` = [#] GX \ ([#] GX) by PRE_TOPC:17;
  then R is boundary iff (Cl R`)` = {} by XBOOLE_1:37;
 hence thesis by Def1;
 end;

theorem Th85:
 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:  P` is dense by A1,Def4;
     Q` is dense by A2,Def4;
    then A5: Cl(Q`) = [#] TS by Def3;
    A6: [#] TS \ Q = Cl(P`) \ Q by A4,Def3;
    A7: Cl(P`) \ Q = Cl(P`) \ Cl Q by A3,PRE_TOPC:52;
     A8: Cl(P`) \ Cl Q c= Cl((P`) \ Q) by Th32;
       Cl((P`) \ Q) = Cl(((P`) /\ Q`)) by SUBSET_1:32;
     then [#] TS \ Q c= Cl((P \/ Q)`) by A6,A7,A8,SUBSET_1:29;
     then [#] TS \ Q c= Cl((P \/ Q)`);
     then Q` c= Cl((P \/ Q)`) by PRE_TOPC:17;
     then Cl(Q`) c= Cl(Cl((P \/ Q)`)) by PRE_TOPC:49;
    then A9: [#] TS c= Cl((P \/ Q)`) by A5,Th26;
      Cl((P \/ Q)`) c= [#] TS by PRE_TOPC:14;
   then [#] TS = Cl((P \/ Q)`) by A9,XBOOLE_0:def 10;
   then (P \/ Q)` is dense by Def3;
  hence thesis by Def4;
 end;

theorem
   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 by Def4;
   let Q;
   assume that A2: Q c= P and A3:Q is open and A4: Q <> {};
     Q meets P` by A1,A3,A4,Th80;
   hence contradiction by A2,Th20;
  end;
  assume A5: for Q st Q c= P & Q is open holds Q={};
  assume not P is boundary;
  then not P` is dense by Def4;
  then consider C being Subset of TS such that A6: C <> {} and
       A7: C is open and A8: (P`) misses C by Th80;
    C c= P by A8,Th20;
  hence contradiction by A5,A6,A7;
 end;

theorem
   P is closed implies (P is boundary iff
     for Q st Q <> {} & Q is open
     ex G being 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 by Def4;
   let Q such that A3: Q <> {} and A4: Q is open;
   (P`) meets Q by A2,A3,A4,Th80;
then A5: (P`) /\ Q <> {} by XBOOLE_0:def 7;
A6: P misses (P`) by PRE_TOPC:26;
     P /\ ((P`) /\ Q) = (P /\ (P`)) /\ Q by XBOOLE_1:16
          .= {} TS /\ Q by A6,XBOOLE_0:def 7
          .= {};
then A7: P misses ((P`) /\ Q) by XBOOLE_0:def 7;
     P` is open by A1,Th29;
then A8: (P`) /\ Q is open by A4,Th38;
     (P`) /\ Q c= Q by XBOOLE_1:17;
   hence ex G being Subset of TS st G c= Q & G <> {}
    & G is open & P misses G by A5,A7,A8;
  end;
  assume A9: for Q st Q <> {} & Q is open
       ex G being Subset of TS st G c= Q & G <> {} & G is open & P misses G;
     now let Q such that A10:Q <> {} and A11:Q is open;
    consider G being Subset of TS such that
    A12: G c= Q and A13: G <> {} and G is open and A14: P misses G
 by A9,A10,A11;
       (P``) /\ G = {} by A14,XBOOLE_0:def 7;
     then G misses (P``) by XBOOLE_0:def 7;
     then G c= P` by Th20;
     hence (P`) meets Q by A12,A13,XBOOLE_1:67;
    end;
    then P` is dense by Th80;
    hence thesis by Def4;
  end;

theorem
   R is boundary iff R c= Fr R
 proof
  hereby assume R is boundary;
  then R` is dense by Def4;
   then Cl R /\ Cl R` = Cl R /\ ([#] GX) by Def3;
   then Cl R = Cl R /\ Cl R` by PRE_TOPC:15;
   then R c= Cl R /\ Cl R` by PRE_TOPC:48;
  hence R c= Fr R by Def2;
 end;
 assume R c= Fr R;
  then R c= Cl R /\ Cl(R`) & Cl R /\ Cl(R`) c= Cl(R`) by Def2,XBOOLE_1:17;
  then A1: R c= Cl(R`) by XBOOLE_1:1;
   A2: Cl(R`) c= [#] GX by PRE_TOPC:14;
      R` c= Cl(R`) by PRE_TOPC:48;
    then R \/ (R`) c= Cl(R`) by A1,XBOOLE_1:8;
   then [#] GX c= Cl(R`) by PRE_TOPC:18;
   then [#] GX = Cl(R`) by A2,XBOOLE_0:def 10;
  then R` is dense by Def3;
  hence thesis by Def4;
 end;

 definition let GX be TopStruct, R be Subset of GX;
   attr R is nowhere_dense means
   :Def5: Cl R is boundary;
 end;

canceled;

theorem
   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 P is boundary by A1,Def5;
         Cl Q is boundary by A2,Def5;
   then Cl P \/ Cl Q is boundary by A3,Th85;
   then Cl(P \/ Q) is boundary by PRE_TOPC:50;
  hence thesis by Def5;
 end;

theorem Th91:
 R is nowhere_dense implies R` is dense
 proof
  assume R is nowhere_dense;
  then Cl R is boundary by Def5;
   then (Cl R)` is dense by Def4;
   then A1: Cl((Cl R)`) = [#] GX by Def3;
     A2: Cl(R`) c= [#] GX by PRE_TOPC:14;
     R c= Cl R by PRE_TOPC:48;
    then (Cl R)` c= R` by PRE_TOPC:19;
   then [#] GX c= Cl(R`) by A1,PRE_TOPC:49;
  then [#] GX= Cl(R`) by A2,XBOOLE_0:def 10;
  hence thesis by Def3;
 end;

theorem
   R is nowhere_dense implies R is boundary
 proof
  assume R is nowhere_dense;
  then R` is dense by Th91;
  hence thesis by Def4;
 end;

theorem Th93:
 S is boundary & S is closed implies S is nowhere_dense
 proof
  assume S is boundary & S is closed;
  then Cl S is boundary by PRE_TOPC:52;
  hence thesis by Def5;
 end;

theorem
   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:52;
  hereby assume R is nowhere_dense;
   then Cl R is boundary by Def5;
   then A2: (Cl R)` is dense by Def4;
      Fr R = R /\ Cl((Cl R)`) by A1,Def2
      .= R /\ [#] GX by A2,Def3;
   hence R = Fr R by PRE_TOPC:15;
  end;
  assume A3: R = Fr R;
      A4: Int R c= R by Th44;
     R = R \ Int R by A1,A3,Lm4;
   then Int(Cl R) = {} by A1,A4,XBOOLE_1:38;
   then Cl R is boundary by Th84;
  hence thesis by Def5;
 end;

theorem Th95:
 P is open implies Fr P is nowhere_dense
proof
 assume P is open;
then A1: Int P = P by Th55;
    Fr P = Cl P /\ Cl(P`) by Def2;
then A2: Fr P c= Cl P by XBOOLE_1:17;
    P misses Fr P by A1,Th73;
then A3: P /\ Fr P = {} TS by XBOOLE_0:def 7;
    Int (P /\ Fr P) = P /\ Int(Fr P) by A1,Th46;
then P /\ Int(Fr P) = {} by A3,Th47;
then A4: P misses Int(Fr P) by XBOOLE_0:def 7;
A5: Int(Fr P) c= Int(Cl P) by A2,Th48;
    Int(Cl P) c= Cl P by Th44;
then A6: Int(Fr P) c= Cl P by A5,XBOOLE_1:1;
A7: Fr P is boundary
  proof
  assume not Fr P is boundary;
  then A8:Int (Fr P) <> {} by Th84;
  consider x being Element of Int(Fr P);
   x in Int(Fr P) by A8;
then A9: TS is non empty by STRUCT_0:def 1;
    x in Cl P by A6,A8,TARSKI:def 3;
  hence contradiction by A4,A8,A9,Th39;
 end;
   Cl Fr P = Fr P by Lm5;
 hence thesis by A7,Th93;
end;

theorem
   P is closed implies Fr P is nowhere_dense
proof
 assume P is closed;
 then P` is open by Th29;
 then Fr P` is nowhere_dense by Th95;
 hence thesis by Th62;
end;

theorem
   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` is dense by A2,Th91;
  then P meets P` by A1,A3,Th80;
  hence contradiction by PRE_TOPC:26;
 end;

::
::    CLOSED AND OPEN DOMAIN, DOMAIN
::

definition let GX be TopStruct, R be Subset of GX;
   attr R is condensed means
   :Def6: Int Cl R c= R & R c= Cl Int R;
   attr R is closed_condensed means
   :Def7:R = Cl Int R;
   attr R is open_condensed means
   :Def8:R = Int Cl R;
end;

canceled 3;

theorem Th101:
 R is open_condensed iff R` is closed_condensed
 proof
    R is open_condensed iff R = Int(Cl R) by Def8;
   then R is open_condensed iff R = (Cl((Cl R)`))` by Def1;
   then R is open_condensed iff R = (Cl((Cl(R``))`))`;
    then R is open_condensed iff R = (Cl(Int(R`)))` by Def1;
 then R is open_condensed iff R` = (Cl(Int(R`)));
 hence thesis by Def7;
 end;

theorem Th102:
 R is closed_condensed implies Fr Int R = Fr R
 proof
  assume R is closed_condensed;
  then A1: R = Cl(Int R) by Def7;
  then A2: Cl R = R by Th26;
     Fr(Int R) = Cl(Int R) /\ Cl((Int R)`) by Def2
       .= Cl(Int R) /\ Cl(((Cl R`)`)`) by Def1
       .= Cl R /\ Cl(R`) by A1,A2,Th26;
  hence thesis by Def2;
 end;

theorem
   R is closed_condensed implies Fr R c= Cl Int R
proof
 assume R is closed_condensed;
 then R = Cl(Int R) by Def7;
 then Fr R = Cl(Cl(Int R)) /\ Cl((Cl(Int R))`) by Def2;
 then Fr R c= Cl(Cl(Int R)) by XBOOLE_1:17;
 hence thesis by Th26;
end;

theorem Th104:
 R is open_condensed implies Fr R = Fr Cl R & Fr Cl R = Cl R \ R
 proof
 assume A1: R is open_condensed;
  then A2: R = Int(Cl R) by Def8;
  A3: Fr R = Cl R \ Int R by Lm4
      .= Cl(Cl R) \ Int(Int(Cl R)) by A2,Th26
      .= Cl(Cl R) \ Int(Cl R) by Th45
      .= Fr(Cl R) by Lm4;
    Fr(Cl R) = Cl(Cl R) \ Int(Cl R) by Lm4
      .= Cl R \ Int(Cl R) by Th26;
  hence thesis by A1,A3,Def8;
 end;

theorem
   R is open & R is closed implies
     (R is closed_condensed iff R is open_condensed)
 proof
 assume that A1: R is open and A2: R is closed;
 thus R is closed_condensed iff R is open_condensed
 proof
 A3: R = Cl R by A2,PRE_TOPC:52;
    R = Int R by A1,Th55;
  hence thesis by A3,Def7,Def8;
  end;
 end;

theorem Th106:
 (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:52;
    A4: Int(Cl R) c=R & R c= Cl(Int R) by A2,Def6;
      Int R c= R by A2,A3,Def6;
     then Cl(Int R) c= R by A3,PRE_TOPC:49;
    then Cl(Int R) = R by A4,XBOOLE_0:def 10;
   hence R is closed_condensed by Def7;
   end;
  assume A5: P is closed_condensed;
  then A6: Cl Int P = P by Def7;
     Fr(Int P) = Cl(Int P) \ Int(Int P) by Lm4;
   then Fr P = Cl(Int P) \ Int(Int P) by A5,Th102
       .= P \ Int P by A6,Th45;
   then P is closed by Th77;
   then Cl P = P by PRE_TOPC:52;
   then Int Cl P c= P by Th44;
  hence thesis by A6,Def6;
  end;

theorem
   (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;
    A3: R = Int R by A1,Th55;
    A4: Int Cl R c= R & R c= Cl Int R by A2,Def6;
       R c= Cl R by PRE_TOPC:48;
     then R c= Int(Cl R) by A3,Th48;
     then Int Cl R = R by A4,XBOOLE_0:def 10;
    hence R is open_condensed by Def8;
   end;
   assume A5: P is open_condensed;
   then Fr P = Fr Cl P & Fr Cl P = Cl P \ P by Th104;
    then A6: P is open by Th76;
A7:      P = Int(Cl P) by A5,Def8;
        Int P = P by A6,Th55;
     then P c= Cl Int P by PRE_TOPC:48;
    hence thesis by A7,Def6;
   end;

theorem Th108:
 P is closed_condensed & Q is closed_condensed implies
      P \/ Q is closed_condensed
 proof
 assume A1: P is closed_condensed & Q is closed_condensed;
  then P = Cl(Int P) & Q = Cl(Int Q) by Def7;
  then A2: P \/ Q = Cl(Int P \/ Int Q) by PRE_TOPC:50;
      Int P \/ Int Q c= Int(P \/ Q) by Th49;
    then A3: P \/ Q c= Cl(Int(P \/ Q)) by A2,PRE_TOPC:49;
      Int(P \/ Q) c= P \/ Q by Th44;
    then A4: Cl(Int(P \/ Q)) c= Cl(P \/ Q) by PRE_TOPC:49;
      P is closed & Q is closed by A1,Th106;
    then P = Cl P & Q = Cl Q by PRE_TOPC:52;
    then Cl(Int(P \/ Q)) c= P \/ Q by A4,PRE_TOPC:50;
    then P \/ Q = Cl(Int(P \/ Q)) by A3,XBOOLE_0:def 10;
   hence thesis by Def7;
  end;

theorem
   P is open_condensed & Q is open_condensed implies P /\ Q is open_condensed
   proof 
A1:   P` \/ Q` = (P /\ Q)` by SUBSET_1:30;
    assume P is open_condensed & Q is open_condensed;
    then P` is closed_condensed & Q` is closed_condensed by Th101;
    then P` \/ Q` is closed_condensed by Th108;
   then (P /\ Q)` is closed_condensed by A1;
  hence thesis by Th101;
  end;

theorem
   P is condensed implies Int Fr P = {}
   proof
   assume P is condensed;
    then A1: Int(Cl P) c= P & P c= Cl(Int P) by Def6;
    then A2: (Cl(Int P))` c= P` by PRE_TOPC:19;
    A3: Int(Fr P) = Int (Cl P /\ Cl(P`)) by Def2
          .= (Cl(Cl P /\ Cl(P`))`)` by Def1
          .= (Cl(((Cl P)`) \/ (Cl P`)`))` by SUBSET_1:30
          .= (Cl(((Cl P)`)) \/ Cl((Cl P`))`)` by PRE_TOPC:50
          .= (Cl(((Cl P)`)))` /\ (Cl((Cl P`))`)` by SUBSET_1:29
          .= Int(Cl P) /\ (Cl((Cl P`)`))` by Def1
          .= Int(Cl P) /\ (Cl(Int P))` by Def1;
      assume A4: Int(Fr P) <> {};
      consider x being Element of Int(Fr P);
    x in Int(Fr P) by A4;
then A5: TS is non empty by STRUCT_0:def 1;
      reconsider x''= x as Point of TS by A4,TARSKI:def 3;
          x'' in Int(Cl P) & x'' in (Cl(Int P))` by A3,A4,XBOOLE_0:def 3;
  hence contradiction by A1,A2,A5,Lm2;
 end;

theorem
   R is condensed implies Int R is condensed & Cl R is condensed
 proof
  assume R is condensed;
   then A1: Int(Cl R) c= R & R c= Cl(Int R) by Def6;
   then A2: (Int(Cl(Cl R))) c= R by Th26;
    A3: R c= Cl R by PRE_TOPC:48;
    then A4: (Int(Cl(Cl R))) c= Cl R by A2,XBOOLE_1:1;
    A5: Int R c= R by Th44;
      R c= Cl(Int(Int R)) by A1,Th45;
    then A6: Int R c= Cl(Int(Int R)) by A5,XBOOLE_1:1;
      (Cl R)` c= R` by A3,PRE_TOPC:19;
    then Cl((Cl R)`) c= Cl(R`) by PRE_TOPC:49;
    then (Cl R`)` c= (Cl(((Cl R)`)))` by PRE_TOPC:19;
     then Cl((Cl R`)`) c= Cl((Cl((Cl R)`))`) by PRE_TOPC:49;
     then Cl(Int R) c= Cl((Cl((Cl R)`))`) by Def1;
     then A7: Cl(Int R) c= Cl(Int(Cl R)) by Def1;
       Cl R c= Cl(Cl(Int R)) by A1,PRE_TOPC:49;
     then Cl R c= Cl(Int R) by Th26;
    then A8: Cl R c= Cl(Int(Cl R)) by A7,XBOOLE_1:1;
     Cl(Int R) c= Cl R by A5,PRE_TOPC:49;
   then Int(Cl(Int R)) c= Int(Cl R) by Th48;
    then A9: Int(Cl(Int R)) c= Int(Int(Cl R)) by Th45;
       Int(Int(Cl R)) c= Int R by A1,Th48;
    then Int(Cl(Int R)) c= Int R by A9,XBOOLE_1:1;
   hence thesis by A4,A6,A8,Def6;
  end;

Back to top