:: On the {K}uratowski Closure-Complement Problem
::  by Lilla Krystyna Bagi\'nska and Adam Grabowski
::
:: Received June 12, 2003
:: Copyright (c) 2003-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, PRE_TOPC, SUBSET_1, ARYTM_1, TOPS_1, TARSKI,
      STRUCT_0, SETFAM_1, FINSET_1, ZFMISC_1, CARD_1, XXREAL_0, ARYTM_3,
      TOPMETR, XXREAL_1, BORSUK_5, RCOMP_1, PROB_1, KURATO_1;
 notations XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, CARD_1,
      ORDINAL1, NUMBERS, XXREAL_0, PRE_TOPC, TOPS_1, ENUMSET1, FINSET_1,
      RCOMP_1, NAT_1, SEQ_4, TOPMETR, TOPS_2, BORSUK_5, PROB_1;
 constructors PROB_1, RCOMP_1, TOPS_1, TOPS_2, TOPMETR, BORSUK_5, SEQ_4,
      NUMBERS;
 registrations XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, XXREAL_0, MEMBERED,
      TOPS_1, TOPMETR, BORSUK_5, STRUCT_0;
 requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
 definitions TARSKI, ZFMISC_1, SETFAM_1, TOPS_2;
 equalities SUBSET_1, STRUCT_0;
 expansions TARSKI, ZFMISC_1, TOPS_2;
 theorems ENUMSET1, TOPS_1, PRE_TOPC, CARD_2, XBOOLE_0, TDLAT_1, TARSKI,
      TOPMETR, ZFMISC_1, XBOOLE_1, SETFAM_1, MEASURE1, BORSUK_5, TOPS_2,
      PROB_1, XREAL_1, XXREAL_0, XXREAL_1, XREAL_0;

begin :: Fourteen Kuratowski Sets

reserve T for non empty TopSpace;
reserve A for Subset of T;

notation
  let T be non empty TopSpace, A be Subset of T;
  synonym A- for Cl A;
end;

theorem Th1:
  A-`-`-`- = A-`-
proof
  set B = Cl (Cl A)`;
  set U = (Cl A)`;
  U = Int U by TOPS_1:23;
  then U c= Int Cl U by PRE_TOPC:18,TOPS_1:19;
  then Cl Int B c= Cl B & Cl U c= Cl Int Cl U by PRE_TOPC:19,TOPS_1:16;
  then Cl Int B = B by XBOOLE_0:def 10;
  hence thesis by TOPS_1:def 1;
end;

Lm1: for T being 1-sorted, A, B being Subset-Family of T holds A \/ B is
Subset-Family of T;

definition
  let T, A;
  func Kurat14Part A -> set equals
  { A, A-, A-`, A-`-, A-`-`, A-`-`-, A-`-`-` };
  coherence;
end;

registration
  let T, A;
  cluster Kurat14Part A -> finite;
  coherence;
end;

definition
  let T, A;
  func Kurat14Set A -> Subset-Family of T equals
  { A, A-, A-`, A-`-, A-`-`, A-
  `-`-, A-`-`-` } \/ { A`, A`-, A`-`, A`-`-, A`-`-`, A`-`-`-, A`-`-`-` };
  coherence
  proof
    set X1 = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl A)`)`,
(Cl (Cl (Cl A)`)`)` }, X2 = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
    Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
    X2 c= bool the carrier of T
    proof
      let x be object;
      assume x in X2;
      then
      x = A` or x = Cl A` or x = (Cl A`)` or x = Cl (Cl A`)` or x = (Cl (
Cl A`)`)` or x = Cl (Cl (Cl A`)`)` or x = (Cl (Cl (Cl A`)`)`)` by
ENUMSET1:def 5;
      hence thesis;
    end;
    then reconsider X2 as Subset-Family of T;
    X1 c= bool the carrier of T
    proof
      let x be object;
      assume x in X1;
      then
      x = A or x = Cl A or x = (Cl A)` or x = Cl (Cl A)` or x = (Cl (Cl A)
      `)` or x = Cl (Cl (Cl A)`)` or x = (Cl (Cl (Cl A)`)`)` by ENUMSET1:def 5;
      hence thesis;
    end;
    then reconsider X1 as Subset-Family of T;
    X1 \/ X2 is Subset-Family of T;
    hence thesis;
  end;
end;

theorem
  Kurat14Set A = Kurat14Part A \/ Kurat14Part A`;

theorem Th3:
  A in Kurat14Set A & A- in Kurat14Set A & A-` in Kurat14Set A & A-
  `- in Kurat14Set A & A-`-` in Kurat14Set A & A-`-`- in Kurat14Set A & A-`-`-`
  in Kurat14Set A
proof
A1: Cl A in Kurat14Part A & (Cl A)` in Kurat14Part A by ENUMSET1:def 5;
A2: Cl (Cl A)` in Kurat14Part A & (Cl (Cl A)`)` in Kurat14Part A by
ENUMSET1:def 5;
A3: Cl (Cl (Cl A)`)` in Kurat14Part A & (Cl (Cl (Cl A)`)`)` in Kurat14Part A
  by ENUMSET1:def 5;
  Kurat14Part A c= Kurat14Set A & A in Kurat14Part A by ENUMSET1:def 5
,XBOOLE_1:7;
  hence thesis by A1,A2,A3;
end;

theorem Th4:
  A` in Kurat14Set A & A`- in Kurat14Set A & A`-` in Kurat14Set A &
A`-`- in Kurat14Set A & A`-`-` in Kurat14Set A & A`-`-`- in Kurat14Set A & A`-`
  -`-` in Kurat14Set A
proof
A1: Cl A` in Kurat14Part A` & (Cl A`)` in Kurat14Part A` by ENUMSET1:def 5;
A2: Cl (Cl A`)` in Kurat14Part A` & (Cl (Cl A`)`)` in Kurat14Part A` by
ENUMSET1:def 5;
A3: Cl (Cl (Cl A`)`)` in Kurat14Part A` & (Cl (Cl (Cl A`)`)`)` in
  Kurat14Part A` by ENUMSET1:def 5;
  Kurat14Part A` c= Kurat14Set A & A` in Kurat14Part A` by ENUMSET1:def 5
,XBOOLE_1:7;
  hence thesis by A1,A2,A3;
end;

definition
  let T, A;
  func Kurat14ClPart A -> Subset-Family of T equals
  { A-, A-`-, A-`-`-, A`-, A
  `-`-, A`-`-`- };
  coherence
  proof
A1: { Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } is Subset-Family of T by
MEASURE1:3;
    {Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`
)`)`} = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)` } \/ { Cl A`, Cl (Cl A`)`, Cl (Cl
(Cl A`)` )` } & { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)` } is Subset-Family of T
by ENUMSET1:13,MEASURE1:3;
    hence thesis by A1,Lm1;
  end;
  func Kurat14OpPart A -> Subset-Family of T equals
  { A-`, A-`-`, A-`-`-`, A`-
  `, A`-`-`, A`-`-`-` };
  coherence
  proof
A2: { (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } is Subset-Family of
    T by MEASURE1:3;
    { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`, (Cl A`)`, (Cl (Cl A`)`)
`, (Cl (Cl (Cl A`)`)`)` } = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
{ (Cl A `)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } & { (Cl A)`, (Cl (Cl A)`)`,
    (Cl ( Cl (Cl A)`)`)` } is Subset-Family of T by ENUMSET1:13,MEASURE1:3;
    hence thesis by A2,Lm1;
  end;
end;

Lm2: Kurat14Set A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`,
Cl (Cl (Cl A`)`)` } \/ { A, A` } \/ { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`
)`, (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` }
proof
  set Y1 = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl (
Cl A`)`)` }, Y2 = { A, A` }, Y3 = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`
  , (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
  set Y = Y1 \/ Y2 \/ Y3;
A1: Y3 c= Y by XBOOLE_1:7;
A2: Y c= Kurat14Set A
  proof
    let x be object;
    assume x in Y;
    then
A3: x in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl
(Cl A`)`)` } \/ { A, A` } or x in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`
    , (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 3;
    per cases by A3,XBOOLE_0:def 3;
    suppose
      x in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`,
      Cl (Cl (Cl A`)`)` };
      then x = Cl A or x = Cl (Cl A)` or x = Cl (Cl (Cl A)`)` or x = Cl A` or
      x = Cl (Cl A`)` or x = Cl (Cl (Cl A`)`)` by ENUMSET1:def 4;
      hence thesis by Th3,Th4;
    end;
    suppose
      x in { A, A` };
      then x = A or x = A` by TARSKI:def 2;
      hence thesis by Th3,Th4;
    end;
    suppose
      x in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`, (Cl A`)`, (
      Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
      then x = (Cl A)` or x = (Cl (Cl A)`)` or x = (Cl (Cl (Cl A)`)`)` or x =
(Cl A`)` or x = (Cl (Cl A`)`)` or x = (Cl (Cl (Cl A`)`)`)` by ENUMSET1:def 4;
      hence thesis by Th3,Th4;
    end;
  end;
A4: Y1 \/ Y2 c= Y by XBOOLE_1:7;
  (Cl (Cl A)`)` in Y3 by ENUMSET1:def 4;
  then
A5: (Cl (Cl A)`)` in Y by A1;
  (Cl A)` in Y3 by ENUMSET1:def 4;
  then
A6: (Cl A)` in Y by A1;
  Y2 c= Y1 \/ Y2 by XBOOLE_1:7;
  then
A7: Y2 c= Y by A4;
  (Cl (Cl (Cl A`)`)`)` in Y3 by ENUMSET1:def 4;
  then
A8: (Cl (Cl (Cl A`)`)`)` in Y by A1;
  (Cl (Cl A`)`)` in Y3 by ENUMSET1:def 4;
  then
A9: (Cl (Cl A`)`)` in Y by A1;
  (Cl A`)` in Y3 by ENUMSET1:def 4;
  then
A10: (Cl A`)` in Y by A1;
  (Cl (Cl (Cl A)`)`)` in Y3 by ENUMSET1:def 4;
  then
A11: (Cl (Cl (Cl A)`)`)` in Y by A1;
  A in Y2 by TARSKI:def 2;
  then
A12: A in Y by A7;
  Y1 c= Y1 \/ Y2 by XBOOLE_1:7;
  then
A13: Y1 c= Y by A4;
  A` in Y2 by TARSKI:def 2;
  then
A14: A` in Y by A7;
  Cl (Cl (Cl A`)`)` in Y1 by ENUMSET1:def 4;
  then
A15: Cl (Cl (Cl A`)`)` in Y by A13;
  Cl (Cl A`)` in Y1 by ENUMSET1:def 4;
  then
A16: Cl (Cl A`)` in Y by A13;
  Cl A` in Y1 by ENUMSET1:def 4;
  then
A17: Cl A` in Y by A13;
  Cl (Cl (Cl A)`)` in Y1 by ENUMSET1:def 4;
  then
A18: Cl (Cl (Cl A)`)` in Y by A13;
  Cl (Cl A)` in Y1 by ENUMSET1:def 4;
  then
A19: Cl (Cl A)` in Y by A13;
  Cl A in Y1 by ENUMSET1:def 4;
  then
A20: Cl A in Y by A13;
  Kurat14Set A c= Y
  proof
    let x be object;
    assume
A21: x in Kurat14Set A;
    per cases by A21,XBOOLE_0:def 3;
    suppose
      x in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
      A)`)`, (Cl (Cl (Cl A)`)`)` };
      hence thesis by A20,A19,A18,A12,A6,A5,A11,ENUMSET1:def 5;
    end;
    suppose
      x in { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`, Cl (Cl
      (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
      hence thesis by A17,A16,A15,A14,A10,A9,A8,ENUMSET1:def 5;
    end;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
  Kurat14Set A = { A, A` } \/ Kurat14ClPart A \/ Kurat14OpPart A by Lm2;

registration
  let T, A;
  cluster Kurat14Set A -> finite;
  coherence;
end;

theorem Th6:
  for Q being Subset of T holds Q in Kurat14Set A implies Q` in
  Kurat14Set A & Q- in Kurat14Set A
proof
  let Q be Subset of T;
  set k1 = Cl A, k2 = (Cl A)`, k3 = Cl (Cl A)`, k4 = (Cl (Cl A)`)`, k5 = Cl (
Cl (Cl A)`)`, k6 = (Cl (Cl (Cl A)`)`)`, k7 = Cl A`, k8 = (Cl A`)`, k9 = Cl (Cl
A`)`, k10 = (Cl (Cl A`)`)`, k11 = Cl (Cl (Cl A`)`)`, k12 = (Cl (Cl (Cl A`)`)`)`
  ;
  assume
A1: Q in Kurat14Set A;
  per cases by A1,XBOOLE_0:def 3;
  suppose
A2: Q in { A, k1, k2, k3, k4, k5, k6 };
    Q` in Kurat14Set A & Cl Q in Kurat14Set A
    proof
      per cases by A2,ENUMSET1:def 5;
      suppose
        Q = A;
        then
        Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (
        Cl A`)`)`, Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = Cl A;
        then
        Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
        A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, k3, k4, k5, k6 } by
ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = (Cl A)`;
        then
        Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, Cl A, (Cl A)`, k3, k4, k5, k6 } by
ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = Cl (Cl A)`;
        then
        Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
        A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, k3, k4, k5, k6 } by
ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = (Cl (Cl A)`)`;
        then
        Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, Cl (Cl A)`, k4, k5, k6 } by
ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = Cl (Cl (Cl A)`)`;
        then
        Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
        A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, k3, k4, k5, k6 } by
ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
A3:     Q = (Cl (Cl (Cl A)`)`)`;
        Cl (Cl (Cl (Cl A)`)`)` = Cl (Cl A)` by Th1;
        then
A4:     Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
        A)`)`, (Cl (Cl (Cl A)`)`)` } by A3,ENUMSET1:def 5;
        Q` in { A, k1, k2, k3, k4, k5, k6 } by A3,ENUMSET1:def 5;
        hence thesis by A4,XBOOLE_0:def 3;
      end;
    end;
    hence thesis;
  end;
  suppose
A5: Q in { A`, k7, k8, k9, k10, k11, k12 };
    Q` in Kurat14Set A & Cl Q in Kurat14Set A
    proof
      per cases by A5,ENUMSET1:def 5;
      suppose
        Q = A`;
        then
        Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12 } & Q` in { A, k1, k2,
        k3, k4, k5, k6 } by ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = Cl A`;
        then
        Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12} & Q` in { A`, k7, (Cl
        A`)`, k9, k10, k11, k12} by ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = (Cl A`)`;
        then Cl Q in { A`, k7, k8, Cl (Cl A`)`, k10, k11, k12} & Q` in { A`,
        Cl A`, k8, k9, k10, k11, k12} by ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = Cl (Cl A`)`;
        then
        Cl Q in { A`, k7, k8, k9, k10, k11, k12} & Q` in { A`, k7, k8, k9
        , k10, k11, k12} by ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = (Cl (Cl A`)`)`;
        then
        Cl Q in { A`, k7, k8, k9, k10, k11, k12} & Q` in { A`, k7, k8, k9
        , k10, k11, k12} by ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        Q = Cl (Cl (Cl A`)`)`;
        then
        Cl Q in { A`, k7, k8, k9, k10, k11, k12} & Q` in { A`, k7, k8, k9
        , k10, k11, k12} by ENUMSET1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
A6:     Q = (Cl (Cl (Cl A`)`)`)`;
        then Cl Q = Cl (Cl A`)` by Th1;
        then
A7:     Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:def 5;
        Q` in { A`, k7, k8, k9, k10, k11, k12} by A6,ENUMSET1:def 5;
        hence thesis by A7,XBOOLE_0:def 3;
      end;
    end;
    hence thesis;
  end;
end;

theorem
  card Kurat14Set A <= 14
proof
  set X = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl A)`)`, (Cl
(Cl (Cl A)`)`)` }, Y = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`, Cl (
  Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
  card X <= 7 & card Y <= 7 by CARD_2:55;
  then card (X \/ Y) <= card X + card Y & card X + card Y <= 7 + 7 by CARD_2:43
,XREAL_1:7;
  hence thesis by XXREAL_0:2;
end;

begin :: Seven Kuratowski Sets

definition
  let T, A;
  func Kurat7Set A -> Subset-Family of T equals
  { A, Int A, Cl A, Int Cl A, Cl
  Int A, Cl Int Cl A, Int Cl Int A };
  coherence
  proof
    set X = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A };
    X c= bool the carrier of T
    proof
      let x be object;
      assume x in X;
      then
      x = A or x = Int A or x = Cl A or x = Int Cl A or x = Cl Int A or x
      = Cl Int Cl A or x = Int Cl Int A by ENUMSET1:def 5;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem
  Kurat7Set A = { A } \/ { Int A, Int Cl A, Int Cl Int A } \/ { Cl A, Cl
  Int A, Cl Int Cl A }
proof
  Kurat7Set A = { A } \/ { Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
  Int Cl Int A } by ENUMSET1:16
    .= { A } \/ ({ Int A, Int Cl A, Int Cl Int A } \/ { Cl A, Cl Int A, Cl
  Int Cl A }) by BORSUK_5:2
    .= { A } \/ { Int A, Int Cl A, Int Cl Int A } \/ { Cl A, Cl Int A, Cl
  Int Cl A } by XBOOLE_1:4;
  hence thesis;
end;

registration
  let T, A;
  cluster Kurat7Set A -> finite;
  coherence;
end;

theorem Th9:
  for Q being Subset of T holds Q in Kurat7Set A implies Int Q in
  Kurat7Set A & Cl Q in Kurat7Set A
proof
  let Q be Subset of T;
  assume
A1: Q in Kurat7Set A;
  Int Q in Kurat7Set A & Cl Q in Kurat7Set A
  proof
    per cases by A1,ENUMSET1:def 5;
    suppose
      Q = A;
      hence thesis by ENUMSET1:def 5;
    end;
    suppose
      Q = Int A;
      hence thesis by ENUMSET1:def 5;
    end;
    suppose
      Q = Cl A;
      hence thesis by ENUMSET1:def 5;
    end;
    suppose
      Q = Int Cl A;
      hence thesis by ENUMSET1:def 5;
    end;
    suppose
      Q = Cl Int A;
      hence thesis by ENUMSET1:def 5;
    end;
    suppose
A2:   Q = Cl Int Cl A;
      Int Cl Int Cl A = Int Cl A by TDLAT_1:5;
      hence thesis by A2,ENUMSET1:def 5;
    end;
    suppose
A3:   Q = Int Cl Int A;
      then Cl Q = Cl Int A by TOPS_1:26;
      hence thesis by A3,ENUMSET1:def 5;
    end;
  end;
  hence thesis;
end;

begin :: The Set Generating Exactly Fourteen Kuratowski Sets

definition
  func KurExSet -> Subset of R^1 equals
  {1} \/ RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5
  ,+infty .[;
  coherence by TOPMETR:17;
end;

theorem Th10:
  Cl KurExSet = {1} \/ [. 2,+infty .[
proof
  set A = KurExSet;
  reconsider B = {1}, C = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[ as Subset
  of R^1 by TOPMETR:17;
  A = {1} \/ (RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[) by XBOOLE_1:113;
  then
A1: Cl A = Cl B \/ Cl C by PRE_TOPC:20;
  Cl B = {1} by BORSUK_5:38;
  hence thesis by A1,BORSUK_5:56;
end;

theorem Th11:
  (Cl KurExSet)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ by Th10,BORSUK_5:63;

theorem Th12:
  Cl (Cl KurExSet)` = ]. -infty, 2 .] by Th11,BORSUK_5:64;

theorem Th13:
  (Cl (Cl KurExSet)`)` = ]. 2,+infty .[ by Th12,TOPMETR:17,XXREAL_1:224,288;

theorem Th14:
  Cl (Cl (Cl KurExSet)`)` = [. 2,+infty .[ by Th13,BORSUK_5:49;

theorem Th15:
  (Cl (Cl (Cl KurExSet)`)`)` = ]. -infty, 2 .[ by Th14,TOPMETR:17,XXREAL_1:224
,294;

theorem Th16:
  KurExSet` = ]. -infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
  set A = KurExSet;
  reconsider B = {1}, C = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[ as Subset
  of R^1 by TOPMETR:17;
A1: C` = ]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5} by BORSUK_5:60;
  A = {1} \/ (RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[) & B` = ]. -infty,
  1 .[ \/ ]. 1,+infty .[ by BORSUK_5:61,XBOOLE_1:113;
  hence thesis by A1,BORSUK_5:62,XBOOLE_1:53;
end;

theorem Th17:
  Cl KurExSet` = ]. -infty, 4 .] \/ {5} by Th16,BORSUK_5:67;

theorem Th18:
  (Cl KurExSet`)` = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th17,BORSUK_5:68;

theorem Th19:
  Cl (Cl KurExSet`)` = [. 4,+infty .[ by Th18,BORSUK_5:55;

theorem Th20:
  (Cl (Cl KurExSet`)`)` = ]. -infty, 4 .[ by Th19,TOPMETR:17,XXREAL_1:224,294;

theorem Th21:
  Cl (Cl (Cl KurExSet`)`)` = ]. -infty, 4 .] by Th20,BORSUK_5:51;

theorem Th22:
  (Cl (Cl (Cl KurExSet`)`)`)` = ]. 4,+infty .[ by Th21,TOPMETR:17,XXREAL_1:224
,288;

begin :: The Set Generating Exactly Seven Kuratowski Sets

theorem Th23:
  Int KurExSet = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,TOPS_1:def 1;

theorem Th24:
  Cl Int KurExSet = [. 4,+infty .[ by Th18,BORSUK_5:55,TOPS_1:def 1;

theorem Th25:
  Int Cl Int KurExSet = ]. 4,+infty .[
proof
  set A = KurExSet;
  Cl Int A = Cl (Cl A`)` by TOPS_1:def 1;
  then
A1: Int Cl Int A = (Cl (Cl (Cl A`)`)`)` by TOPS_1:def 1;
  (Cl (Cl A`)`)` = ]. -infty, 4 .[ by Th19,TOPMETR:17,XXREAL_1:224,294;
  then Cl (Cl (Cl A`)`)` = ]. -infty, 4 .] by BORSUK_5:51;
  hence thesis by A1,TOPMETR:17,XXREAL_1:224,288;
end;

theorem Th26:
  Int Cl KurExSet = ]. 2,+infty .[
proof
  set A = KurExSet;
  (Cl A)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ by Th10,BORSUK_5:63;
  then Cl (Cl A)` = ]. -infty, 2 .] by BORSUK_5:64;
  then (Cl (Cl A)`)` = ]. 2,+infty .[ by TOPMETR:17,XXREAL_1:224,288;
  hence thesis by TOPS_1:def 1;
end;

theorem Th27:
  Cl Int Cl KurExSet = [. 2,+infty .[
proof
  set A = KurExSet;
  (Cl A)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ by Th10,BORSUK_5:63;
  then Cl (Cl A)` = ]. -infty, 2 .] by BORSUK_5:64;
  then (Cl (Cl A)`)` = ]. 2,+infty .[ by TOPMETR:17,XXREAL_1:224,288;
  hence thesis by BORSUK_5:49,TOPS_1:def 1;
end;

begin :: The Difference Between Chosen Kuratowski Sets

theorem
  Cl Int Cl KurExSet <> Int Cl KurExSet
by Th27,XXREAL_1:236,Th26,XXREAL_1:235;

theorem Th29:
  Cl Int Cl KurExSet <> Cl KurExSet
proof
  set A = KurExSet;
  1 in {1} by TARSKI:def 1;
  then 1 in Cl A by Th10,XBOOLE_0:def 3;
  hence thesis by Th27,XXREAL_1:236;
end;

theorem
  Cl Int Cl KurExSet <> Int Cl Int KurExSet
by Th27,XXREAL_1:236,Th25,XXREAL_1:235;

theorem Th31:
  Cl Int Cl KurExSet <> Cl Int KurExSet
proof
  set A = KurExSet;
  2 in Cl Int Cl A by Th27,XXREAL_1:236;
  hence thesis by Th24,XXREAL_1:236;
end;

theorem
  Cl Int Cl KurExSet <> Int KurExSet
proof
  set A = KurExSet;
  2 in Cl Int Cl A & Int A = ]. 4, 5.[ \/ ]. 5,+infty .[ by Th18,Th27,
TOPS_1:def 1,XXREAL_1:236;
  hence thesis by XXREAL_1:223;
end;

theorem
  Int Cl KurExSet <> Cl KurExSet
proof
  set A = KurExSet;
  1 in {1} by TARSKI:def 1;
  then 1 in Cl A by Th10,XBOOLE_0:def 3;
  hence thesis by Th26,XXREAL_1:235;
end;

theorem
  Int Cl KurExSet <> Int Cl Int KurExSet
proof
  set A = KurExSet;
  3 in Int Cl A by Th26,XXREAL_1:235;
  hence thesis by Th25,XXREAL_1:235;
end;

theorem
  Int Cl KurExSet <> Cl Int KurExSet by Th26,BORSUK_5:34,45;

theorem Th36:
  Int Cl KurExSet <> Int KurExSet
proof
  set A = KurExSet;
  5 in Int Cl A & Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,Th26,
TOPS_1:def 1,XXREAL_1:235;
  hence thesis by XXREAL_1:205;
end;

theorem
  Int Cl Int KurExSet <> Cl KurExSet
proof
  set A = KurExSet;
  2 in [. 2,+infty .[ by XXREAL_1:236;
  then 2 in Cl A by Th10,XBOOLE_0:def 3;
  hence thesis by Th25,XXREAL_1:235;
end;

theorem Th38:
  Cl Int KurExSet <> Cl KurExSet
proof
  set A = KurExSet;
  2 in [. 2,+infty .[ by XXREAL_1:236;
  then 2 in Cl A by Th10,XBOOLE_0:def 3;
  hence thesis by Th24,XXREAL_1:236;
end;

theorem
  Int KurExSet <> Cl KurExSet
proof
  set A = KurExSet;
  5 in [. 2,+infty .[ by XXREAL_1:236;
  then
A1: 5 in Cl A by Th10,XBOOLE_0:def 3;
  Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,TOPS_1:def 1;
  hence thesis by A1,XXREAL_1:205;
end;

theorem Th40:
  Cl KurExSet <> KurExSet
proof
  set A = KurExSet;
  ( not 5 in {1})& not 5 in RAT (2, 4) by BORSUK_5:29,TARSKI:def 1;
  then ( not 5 in ]. 4, 5 .[)& not 5 in {1} \/ RAT (2, 4) by XBOOLE_0:def 3
,XXREAL_1:4;
  then
A1: ( not 5 in ]. 5,+infty .[)& not 5 in {1} \/ RAT (2, 4) \/ ]. 4, 5 .[ by
XBOOLE_0:def 3,XXREAL_1:235;
  5 in [. 2,+infty .[ by XXREAL_1:236;
  then 5 in Cl A by Th10,XBOOLE_0:def 3;
  hence thesis by A1,XBOOLE_0:def 3;
end;

theorem Th41:
  KurExSet <> Int KurExSet
proof
  set A = KurExSet;
  1 in { 1 } by TARSKI:def 1;
  then 1 in {1} \/ RAT (2,4) by XBOOLE_0:def 3;
  then 1 in {1} \/ RAT (2,4) \/ ]. 4, 5 .[ by XBOOLE_0:def 3;
  then
A1: 1 in A by XBOOLE_0:def 3;
  Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,TOPS_1:def 1;
  hence thesis by A1,XXREAL_1:223;
end;

theorem
  Cl Int KurExSet <> Int Cl Int KurExSet
by Th24,XXREAL_1:236,Th25,XXREAL_1:235;

theorem Th43:
  Int Cl Int KurExSet <> Int KurExSet
proof
  set A = KurExSet;
  5 in Int Cl Int A & Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,Th25,
TOPS_1:def 1,XXREAL_1:235;
  hence thesis by XXREAL_1:205;
end;

theorem
  Cl Int KurExSet <> Int KurExSet
proof
  set A = KurExSet;
  4 in Cl Int A & Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,Th24,
TOPS_1:def 1,XXREAL_1:236;
  hence thesis by XXREAL_1:223;
end;

begin :: Final Proofs For Seven

theorem Th45:
  Int Cl Int KurExSet <> Int Cl KurExSet
proof
  set A = KurExSet;
  not 3 in Int Cl Int A by Th25,XXREAL_1:235;
  hence thesis by Th26,XXREAL_1:235;
end;

theorem Th46:
  Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet are_mutually_distinct
by Th36,Th43,Th45;

theorem Th47:
  Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct
by Th38,Th29,Th31;

theorem Th48:
  for X being set st X in { Int KurExSet, Int Cl KurExSet, Int Cl
  Int KurExSet } holds X is open non empty Subset of R^1
proof
  let X be set;
  assume
A1: X in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet };
  per cases by A1,ENUMSET1:def 1;
  suppose
    X = Int KurExSet;
    hence thesis by Th18,TOPS_1:def 1;
  end;
  suppose
    X = Int Cl KurExSet;
    hence thesis by Th26;
  end;
  suppose
    X = Int Cl Int KurExSet;
    hence thesis by Th25;
  end;
end;

theorem Th49:
  for X being set st X in { Int KurExSet, Int Cl KurExSet, Int Cl
  Int KurExSet } holds X <> REAL
proof
  let X be set;
  assume
A1: X in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet };
  per cases by A1,ENUMSET1:def 1;
  suppose
A2: X = Int KurExSet;
     5 in REAL by XREAL_0:def 1;
    hence thesis by Th23,XXREAL_1:205,A2;
  end;
  suppose
    X = Int Cl KurExSet;
    hence thesis by Th26,BORSUK_5:45;
  end;
  suppose
    X = Int Cl Int KurExSet;
    hence thesis by Th25,BORSUK_5:45;
  end;
end;

theorem
  for X being set st X in { Cl KurExSet, Cl Int KurExSet, Cl Int Cl
  KurExSet } holds X <> REAL
proof
  let X be set;
  assume
A1: X in { Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet };
  per cases by A1,ENUMSET1:def 1;
  suppose
A2: X = Cl KurExSet;
A3: 0 in REAL by XREAL_0:def 1;
    ( not 0 in {1})& not 0 in [. 2,+infty .[ by XXREAL_1:236, TARSKI:def 1;
    hence thesis by A2,Th10,XBOOLE_0:def 3,A3;
  end;
  suppose
    X = Cl Int KurExSet;
    hence thesis by Th24,BORSUK_5:46;
  end;
  suppose
    X = Cl Int Cl KurExSet;
    hence thesis by Th27,BORSUK_5:46;
  end;
end;

theorem Th51:
  { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet } misses {
  Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet }
proof
  set X = { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet }, Y = { Cl
  KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet };
  assume X meets Y;
  then consider x being object such that
A1: x in X and
A2: x in Y by XBOOLE_0:3;
  x is open non empty Subset of R^1 & x is closed Subset of R^1 by A1,A2,Th48,
ENUMSET1:def 1;
  hence thesis by A1,Th49,BORSUK_5:34;
end;

theorem Th52:
  Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl KurExSet,
  Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct by Th46,Th47,Th51,
BORSUK_5:6;

registration
  cluster KurExSet -> non closed non open;
  coherence by Th40,Th41,PRE_TOPC:22,TOPS_1:23;
end;

theorem
  { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl
  KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } misses { KurExSet }
proof
  set A = KurExSet;
  assume { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl KurExSet,
  Cl Int KurExSet, Cl Int Cl KurExSet } meets { KurExSet };
  then
A1: KurExSet in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl
  KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } by ZFMISC_1:50;
  per cases by A1,ENUMSET1:def 4;
  suppose
    A = Int A;
    hence thesis;
  end;
  suppose
    A = Int Cl A;
    hence thesis;
  end;
  suppose
    A = Int Cl Int A;
    hence thesis;
  end;
  suppose
    A = Cl A;
    hence thesis;
  end;
  suppose
    A = Cl Int A;
    hence thesis;
  end;
  suppose
    A = Cl Int Cl A;
    hence thesis;
  end;
end;

theorem Th54:
  KurExSet, Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl
  KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct
by Th52;

theorem
  card Kurat7Set KurExSet = 7
proof
  set A = KurExSet;
  A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A
  are_mutually_distinct by Th54;
  hence thesis by BORSUK_5:4;
end;

begin :: Final Proofs For Fourteen

registration
  cluster Kurat14ClPart KurExSet -> with_proper_subsets;
  coherence
  proof
    set A = KurExSet;
    assume
A1: the carrier of R^1 in Kurat14ClPart KurExSet;
    per cases by A1,ENUMSET1:def 4,TOPMETR:17;
    suppose
      REAL = Cl A;
      hence thesis by Th10,BORSUK_5:69;
    end;
    suppose
      REAL = Cl (Cl A)`;
      hence thesis by Th12,BORSUK_5:47;
    end;
    suppose
      REAL = Cl (Cl (Cl A)`)`;
      hence thesis by Th14,BORSUK_5:46;
    end;
    suppose
      REAL = Cl A`;
      hence thesis by Th17,BORSUK_5:70;
    end;
    suppose
      REAL = Cl (Cl A`)`;
      hence thesis by Th19,BORSUK_5:46;
    end;
    suppose
      REAL = Cl (Cl (Cl A`)`)`;
      hence thesis by Th21,BORSUK_5:47;
    end;
  end;
  cluster Kurat14OpPart KurExSet -> with_proper_subsets;
  coherence
  proof
    set A = KurExSet;
    assume
A2: the carrier of R^1 in Kurat14OpPart KurExSet;
    per cases by A2,ENUMSET1:def 4,TOPMETR:17;
    suppose
      REAL = (Cl A)`;
      hence thesis by Th10,BORSUK_5:72;
    end;
    suppose
      REAL = (Cl (Cl A)`)`;
      hence thesis by Th12,BORSUK_5:72;
    end;
    suppose
      REAL = (Cl (Cl (Cl A)`)`)`;
      hence thesis by Th14,BORSUK_5:72;
    end;
    suppose
      REAL = (Cl A`)`;
      hence thesis by Th17,BORSUK_5:72;
    end;
    suppose
      REAL = (Cl (Cl A`)`)`;
      hence thesis by Th19,BORSUK_5:72;
    end;
    suppose
      REAL = (Cl (Cl (Cl A`)`)`)`;
      hence thesis by Th21,BORSUK_5:72;
    end;
  end;
end;

registration
  cluster Kurat14Set KurExSet -> with_proper_subsets;
  coherence
  proof
    reconsider AA = { KurExSet, KurExSet` } as Subset-Family of R^1 by
MEASURE1:2;
    AA is with_proper_subsets
    proof
      assume
A1:   the carrier of R^1 in AA;
      per cases by A1,TARSKI:def 2,TOPMETR:17;
      suppose
        REAL = KurExSet;
        then [#]R^1 = KurExSet by TOPMETR:17;
        hence thesis;
      end;
      suppose
        REAL = KurExSet`;
        then [#]R^1 = KurExSet` by TOPMETR:17;
        hence thesis by TOPS_1:3;
      end;
    end;
    then
A2: AA \/ Kurat14ClPart KurExSet is with_proper_subsets by SETFAM_1:48;
    Kurat14Set KurExSet = AA \/ Kurat14ClPart KurExSet \/ Kurat14OpPart
    KurExSet by Lm2;
    hence thesis by A2,SETFAM_1:48;
  end;
end;

registration
  cluster Kurat14Set KurExSet -> with_non-empty_elements;
  coherence
  proof
    reconsider E = {}R^1 as Subset of R^1;
    assume {} in Kurat14Set KurExSet;
    then E` in Kurat14Set KurExSet by Th6;
    hence thesis by SETFAM_1:def 12;
  end;
end;

theorem Th56:
  for A being with_non-empty_elements set, B being set st B c= A
  holds B is with_non-empty_elements
proof
  let A be with_non-empty_elements set, B be set;
  assume
A1: B c= A;
  assume {} in B;
  hence thesis by A1;
end;

registration
  cluster Kurat14ClPart KurExSet -> with_non-empty_elements;
  coherence
  proof
    Kurat14Set KurExSet = { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet
    \/ Kurat14OpPart KurExSet by Lm2;
    then
A1: { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet c= Kurat14Set
    KurExSet by XBOOLE_1:7;
    Kurat14ClPart KurExSet c= { KurExSet, KurExSet`} \/ Kurat14ClPart
    KurExSet by XBOOLE_1:7;
    hence thesis by A1,Th56,XBOOLE_1:1;
  end;
  cluster Kurat14OpPart KurExSet -> with_non-empty_elements;
  coherence
  proof
    Kurat14Set KurExSet = { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet
    \/ Kurat14OpPart KurExSet by Lm2;
    hence thesis by Th56,XBOOLE_1:7;
  end;
end;

registration
  cluster with_proper_subsets with_non-empty_elements for Subset-Family of R^1;
  existence
  proof
    take Kurat14Set KurExSet;
    thus thesis;
  end;
end;

theorem Th57:
  for F, G being with_proper_subsets with_non-empty_elements
  Subset-Family of R^1 st F is open & G is closed holds F misses G
proof
  let F, G be with_proper_subsets with_non-empty_elements Subset-Family of R^1;
  assume
A1: F is open & G is closed;
  assume F meets G;
  then consider x being object such that
A2: x in F and
A3: x in G by XBOOLE_0:3;
  reconsider x as Subset of R^1 by A2;
  x is open & x is closed by A1,A2,A3;
  then x = {} or x = REAL by BORSUK_5:34;
  hence thesis by A2,SETFAM_1:def 12,TOPMETR:17;
end;

registration
  cluster Kurat14ClPart KurExSet -> closed;
  coherence
  by ENUMSET1:def 4;
  cluster Kurat14OpPart KurExSet -> open;
  coherence
  by ENUMSET1:def 4;
end;

theorem
  Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th57;

registration
  let T, A;
  cluster Kurat14ClPart A -> finite;
  coherence;
  cluster Kurat14OpPart A -> finite;
  coherence;
end;

theorem Th59:
  card (Kurat14ClPart KurExSet) = 6
proof
  set A = KurExSet;
A1: Cl (Cl (Cl A`)`)` = ]. -infty, 4 .] by Th20,BORSUK_5:51;
  5 in {5} by TARSKI:def 1;
  then 5 in Cl A` by Th17,XBOOLE_0:def 3;
  then
A2: Cl Int A = Cl (Cl A`)` & Cl A` <> Cl (Cl (Cl A`)`)` by A1,TOPS_1:def 1
,XXREAL_1:234;
  ( not 5 in Cl (Cl (Cl A`)`)`)& 5 in [. 2,+infty .[ by Th21,XXREAL_1:234,236;
  then
A3: Cl A <> Cl (Cl (Cl A`)`)` by Th10,XBOOLE_0:def 3;
  ( not 5 in Cl (Cl (Cl A`)`)`)& Cl (Cl A`)` = [. 4,+infty .[ by Th18,Th21,
BORSUK_5:55,XXREAL_1:234;
  then
A4: Cl (Cl A`)` <> Cl (Cl (Cl A`)`)` by XXREAL_1:236;
  5 in Cl (Cl (Cl A)`)` by Th14,XXREAL_1:236;
  then
A5: Cl (Cl (Cl A)`)` <> Cl (Cl (Cl A`)`)` by Th21,XXREAL_1:234;
  ( not 6 in ]. -infty, 4 .])& not 6 in {5} by TARSKI:def 1,XXREAL_1:234;
  then
A6: not 6 in Cl A` by Th17,XBOOLE_0:def 3;
  Cl (Cl (Cl A)`)` = [. 2,+infty .[ by Th13,BORSUK_5:49;
  then
A7: Cl (Cl (Cl A)`)` <> Cl A` by A6,XXREAL_1:236;
A8: 4 in Cl (Cl (Cl A)`)` & Cl Int Cl A = Cl (Cl (Cl A)`)` by Th14,TOPS_1:def 1
,XXREAL_1:236;
A9: not 4 in Cl (Cl A)` by Th12,XXREAL_1:234;
  then Cl (Cl A)` <> Cl (Cl (Cl A`)`)` by A1,XXREAL_1:234;
  then
  Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`
  )` are_mutually_distinct by A9,A3,A7,A5,A8,A2,A4,Th29,Th31;
  hence thesis by BORSUK_5:3;
end;

theorem Th60:
  card (Kurat14OpPart KurExSet) = 6
proof
  set A = KurExSet;
A1: ( not 5 in ]. -infty, 1 .[)& not 5 in ]. 1, 2 .[ by XXREAL_1:4;
  (Cl A)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ & 5 in (Cl (Cl (Cl A`)`)`)` by Th10
,Th22,BORSUK_5:63,XXREAL_1:235;
  then
A2: (Cl A)` <> (Cl (Cl (Cl A`)`)`)` by A1,XBOOLE_0:def 3;
A3: (Cl (Cl (Cl A)`)`)` = ]. -infty, 2 .[ by Th14,TOPMETR:17,XXREAL_1:224,294;
  6 in ]. 5,+infty .[ by XXREAL_1:235;
  then 6 in (Cl A`)` by Th18,XBOOLE_0:def 3;
  then
A4: (Cl (Cl (Cl A)`)`)` <> (Cl A`)` by A3,XXREAL_1:233;
A5: 4 in (Cl (Cl A)`)` by Th13,XXREAL_1:235;
  ( not 5 in ]. 4, 5 .[)& not 5 in ]. 5,+infty .[ by XXREAL_1:4;
  then
A6: not 5 in (Cl A`)` by Th18,XBOOLE_0:def 3;
  (Cl A)` <> (Cl Int Cl A)` by Th29,BORSUK_5:71;
  then
A7: (Cl A)` <> (Cl (Cl (Cl A)`)`)` by TOPS_1:def 1;
A8: not 5 in (Cl (Cl A`)`)` by Th20,XXREAL_1:233;
  (Cl (Cl (Cl A`)`)`)` = ]. 4,+infty .[ by Th21,TOPMETR:17,XXREAL_1:224,288;
  then
A9: (Cl (Cl A)`)` <> (Cl (Cl (Cl A`)`)`)` by A5,XXREAL_1:235;
  (Cl Int Cl A)` = (Cl (Cl (Cl A)`)`)` & (Cl Int A)` = (Cl (Cl A`)`)` by
TOPS_1:def 1;
  then
A10: (Cl (Cl (Cl A)`)`)` <> (Cl (Cl A`)`)` by Th31,BORSUK_5:71;
A11: ( not 5 in (Cl (Cl (Cl A)`)`)`)& 5 in (Cl (Cl (Cl A`)`)`)` by Th15,Th22,
XXREAL_1:233,235;
  (Cl (Cl A)`)` <> (Cl (Cl (Cl A)`)`)` by A3,A5,XXREAL_1:233;
  then (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`, (Cl A`)`, (Cl (Cl A`)`)`,
  (Cl (Cl (Cl A`)`)`)` are_mutually_distinct by A2,A7,A9,A4,A10,A6,A11,A8;
  hence thesis by BORSUK_5:3;
end;

theorem Th61:
  { KurExSet, KurExSet` } misses Kurat14ClPart KurExSet
proof
  set A = KurExSet;
  assume { A, A` } meets Kurat14ClPart A;
  then consider x being object such that
A1: x in { A, A` } and
A2: x in Kurat14ClPart A by XBOOLE_0:3;
  reconsider x as Subset of R^1 by A2;
  x = A or x = A` by A1,TARSKI:def 2;
  then
A3: x` = A by A2,TOPS_2:def 2;
  x is closed by A2,TOPS_2:def 2;
  hence thesis by A3;
end;

registration
  cluster KurExSet -> non empty;
  coherence;
end;

theorem Th62:
  KurExSet <> KurExSet`
by XBOOLE_1:66,XBOOLE_1:79;

theorem Th63:
  { KurExSet, KurExSet` } misses Kurat14OpPart KurExSet
proof
  set A = KurExSet;
  assume { A, A` } meets Kurat14OpPart A;
  then consider x being object such that
A1: x in { A, A` } and
A2: x in Kurat14OpPart A by XBOOLE_0:3;
  reconsider x as Subset of R^1 by A2;
  x = A or x = A` by A1,TARSKI:def 2;
  then
A3: x` = A by A2,TOPS_2:def 1;
  x is open by A2,TOPS_2:def 1;
  hence thesis by A3;
end;

::$N Kuratowski's closure-complement problem
theorem
  card Kurat14Set KurExSet = 14
proof
  set A = KurExSet;
  set B = { A, A` };
A1: B misses (Kurat14ClPart A \/ Kurat14OpPart A) by Th61,Th63,XBOOLE_1:70;
A2: card (Kurat14ClPart A \/ Kurat14OpPart A) = 6 + 6 by Th57,Th59,Th60,
CARD_2:40
    .= 12;
  card Kurat14Set A = card (B \/ Kurat14ClPart A \/ Kurat14OpPart A) by Lm2
    .= card (B \/ (Kurat14ClPart A \/ Kurat14OpPart A)) by XBOOLE_1:4
    .= card B + card (Kurat14ClPart A \/ Kurat14OpPart A) by A1,CARD_2:40
    .= 2 + 12 by A2,Th62,CARD_2:57
    .= 14;
  hence thesis;
end;

begin :: Properties of Kuratowski Sets

definition
  let T be TopStruct, A be Subset-Family of T;
  attr A is Cl-closed means
  for P being Subset of T st P in A holds Cl P in A;
  attr A is Int-closed means
  for P being Subset of T st P in A holds Int P in A;
end;

registration
  let T, A;
  cluster Kurat14Set A -> non empty;
  coherence;
  cluster Kurat14Set A -> Cl-closed;
  coherence
  by Th6;
  cluster Kurat14Set A -> compl-closed;
  coherence
  proof
    for P be Subset of T st P in Kurat14Set A holds P` in Kurat14Set A by Th6;
    hence thesis by PROB_1:def 1;
  end;
end;

registration
  let T, A;
  cluster Kurat7Set A -> non empty;
  coherence;
  cluster Kurat7Set A -> Int-closed;
  coherence
  by Th9;
  cluster Kurat7Set A -> Cl-closed;
  coherence
  by Th9;
end;

registration
  let T;
  cluster Int-closed Cl-closed non empty for Subset-Family of T;
  existence
  proof
    take Kurat7Set {}T;
    thus thesis;
  end;
  cluster compl-closed Cl-closed non empty for Subset-Family of T;
  existence
  proof
    take Kurat14Set {}T;
    thus thesis;
  end;
end;