The Mizar article:

On the Kuratowski Closure-Complement Problem

by
Lilla Krystyna Baginska, and
Adam Grabowski

Received June 12, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: KURATO_1
[ MML identifier index ]


environ

 vocabulary BOOLE, KURATO_1, FINSET_1, TOPS_1, PRE_TOPC, CARD_1, SUBSET_1,
      RCOMP_1, PROB_1, INCPROJ, SETFAM_1, AMI_1, TOPMETR, RAT_1, BORSUK_5;
 notation XBOOLE_0, TARSKI, SUBSET_1, STRUCT_0, NUMBERS, XREAL_0, PRE_TOPC,
      TOPS_1, ENUMSET1, CARD_1, FINSET_1, RCOMP_1, INCPROJ, NAT_1, SEQ_4,
      RCOMP_2, PCOMPS_1, TOPMETR, AMI_1, BORSUK_5;
 constructors TOPS_1, NAT_1, INCPROJ, RCOMP_2, PSCOMP_1, INTEGRA1, COMPTS_1,
      LIMFUNC1, TOPGRP_1, TREAL_1, DOMAIN_1, RAT_1, PROB_1, AMI_1, BORSUK_5,
      MEMBERED;
 clusters FINSET_1, TOPS_1, TOPREAL6, AMI_1, XBOOLE_0, BORSUK_5, MEMBERED,
      ZFMISC_1;
 requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
 definitions XBOOLE_0, TARSKI, INCPROJ, AMI_1, BORSUK_5;
 theorems ENUMSET1, TOPS_1, PRE_TOPC, CARD_2, REAL_1, AXIOMS, XBOOLE_0,
      TDLAT_1, TARSKI, TOPMETR, ZFMISC_1, XBOOLE_1, JORDAN6, SETFAM_1,
      WAYBEL12, AMI_1, MEASURE1, BORSUK_5;

begin :: Fourteen Kuratowski Sets

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

theorem Th1:
  Cl (Cl (Cl (Cl A)`)`)` = Cl (Cl A)`
  proof
    set B = Cl (Cl A)`;
     Int B c= B by TOPS_1:44;
    then Cl Int B c= Cl B by PRE_TOPC:49;
then A1: Cl Int B c= B by PRE_TOPC:52;
    set U = (Cl A)`;
A2: U c= Cl U by PRE_TOPC:48;
     U = Int U by TOPS_1:55;
    then U c= Int Cl U by A2,TOPS_1:48;
    then Cl U c= Cl Int Cl U by PRE_TOPC:49;
    then Cl Int B = B by A1,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 equals :Def1:
    { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
      Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` };
  coherence;
end;

definition let T, A;
  cluster Kurat14Part A -> finite;
  coherence
  proof
     Kurat14Part A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
         Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by Def1;
    hence thesis;
  end;
end;

definition let T, A;
  func Kurat14Set A -> Subset-Family of T equals :Def2:
    { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
         Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
    { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
          Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl 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`)`)`)` };
     X1 c= bool the carrier of T
    proof
      let x be set;
      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:33;
      hence thesis;
    end;
    then reconsider X1 as Subset-Family of T by SETFAM_1:def 7;
     X2 c= bool the carrier of T
    proof
      let x be set;
      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:33;
      hence thesis;
    end;
    then reconsider X2 as Subset-Family of T by SETFAM_1:def 7;
     X1 \/ X2 is Subset-Family of T;
    hence thesis;
  end;
end;

theorem Th2:
  Kurat14Set A = Kurat14Part A \/ Kurat14Part A`
  proof
     Kurat14Set A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
              Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
            { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
              Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def2
        .= Kurat14Part A \/ { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
              Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def1;
    hence thesis by Def1;
  end;

theorem Th3:
  A in Kurat14Set A & Cl A in Kurat14Set A & (Cl A)` in Kurat14Set A &
    Cl (Cl A)` in Kurat14Set A & (Cl (Cl A)`)` in Kurat14Set A &
      Cl (Cl (Cl A)`)` in Kurat14Set A & (Cl (Cl (Cl A)`)`)` in Kurat14Set A
  proof
     Kurat14Set A = Kurat14Part A \/ Kurat14Part A` by Th2;
then A1: Kurat14Part A c= Kurat14Set A by XBOOLE_1:7;
     Kurat14Part A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
        Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by Def1;
    then A in Kurat14Part A & Cl A in Kurat14Part A &
      (Cl A)` in Kurat14Part A &
    Cl (Cl A)` in Kurat14Part A & (Cl (Cl A)`)` in Kurat14Part A &
    Cl (Cl (Cl A)`)` in Kurat14Part A & (Cl (Cl (Cl A)`)`)` in Kurat14Part A
      by ENUMSET1:34;
    hence thesis by A1;
  end;

theorem Th4:
  A` in Kurat14Set A & Cl A` in Kurat14Set A &
    (Cl A`)` in Kurat14Set A & Cl (Cl A`)` in Kurat14Set A &
      (Cl (Cl A`)`)` in Kurat14Set A & Cl (Cl (Cl A`)`)` in Kurat14Set A &
        (Cl (Cl (Cl A`)`)`)` in Kurat14Set A
  proof
     Kurat14Set A = Kurat14Part A \/ Kurat14Part A` by Th2;
then A1: Kurat14Part A` c= Kurat14Set A by XBOOLE_1:7;
     Kurat14Part A` = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
       Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def1;
    then A` in Kurat14Part A` & Cl A` in Kurat14Part A` &
      (Cl A`)` in Kurat14Part A` &
      Cl (Cl A`)` in Kurat14Part A` & (Cl (Cl A`)`)` in Kurat14Part A` &
      Cl (Cl (Cl A`)`)` in Kurat14Part A` &
      (Cl (Cl (Cl A`)`)`)` in Kurat14Part A`
        by ENUMSET1:34;
    hence thesis by A1;
  end;

definition let T, A;
  func Kurat14ClPart A -> Subset-Family of T equals :Def3:
    { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
            Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` };
  coherence
  proof
A1: {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`)`)` } by ENUMSET1:53;
A2: { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)` } is Subset-Family of T
                    by BORSUK_5:32;
     { Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } is Subset-Family of T
                    by BORSUK_5:32;
    hence thesis by A1,A2,Lm1;
  end;
  func Kurat14OpPart A -> Subset-Family of T equals :Def4:
    { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
             (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
  coherence
  proof
A3: { (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`)`)`)` } by ENUMSET1:53;
A4: { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } is Subset-Family of T
           by BORSUK_5:32;
     { (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } is Subset-Family of T
      by BORSUK_5:32;
    hence thesis by A3,A4,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
A1: Kurat14Set A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)` ,
              Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
     { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
         Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def2;
    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;
A2: Y3 c= Y & Y1 \/ Y2 c= Y by XBOOLE_1:7;
     Y1 c= Y1 \/ Y2 & Y2 c= Y1 \/ Y2 by XBOOLE_1:7;
then A3: Y1 c= Y & Y2 c= Y by A2,XBOOLE_1:1;
A4: Cl A in Y1 & Cl (Cl A)` in Y1 & Cl (Cl (Cl A)`)` in Y1 &
    Cl A` in Y1 & Cl (Cl A`)` in Y1 & Cl (Cl (Cl A`)`)` in Y1 by ENUMSET1:29;
A5: A in Y2 & A` in Y2 by TARSKI:def 2;
     (Cl A)` in Y3 & (Cl (Cl A)`)` in Y3 & (Cl (Cl (Cl A)`)`)` in Y3 &
      (Cl A`)` in Y3 & (Cl (Cl A`)`)` in Y3 & (Cl (Cl (Cl A`)`)`)` in Y3
        by ENUMSET1:29;
then A6: Cl A in Y & Cl (Cl A)` in Y & Cl (Cl (Cl A)`)` in Y &
      Cl A` in Y & Cl (Cl A`)` in Y & Cl (Cl (Cl A`)`)` in Y &
      A in Y & A` in Y &
      (Cl A)` in Y & (Cl (Cl A)`)` in Y & (Cl (Cl (Cl A)`)`)` in Y &
      (Cl A`)` in Y & (Cl (Cl A`)`)` in Y & (Cl (Cl (Cl A`)`)`)` in Y
       by A2,A3,A4,A5;
     Kurat14Set A = Y
    proof
      thus Kurat14Set A c= Y
      proof
        let x be set;
        assume
A7:     x in Kurat14Set A;
        per cases by A1,A7,XBOOLE_0:def 2;
        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 A6,ENUMSET1:33;
        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 A6,ENUMSET1:33;
      end;
      thus Y c= Kurat14Set A
      proof
        let x be set;
        assume x in Y;
then A8:     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 2;
        per cases by A8,XBOOLE_0:def 2;
        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:28;
        hence thesis by Th3,Th4;
        suppose x in { A, A` };
        then x = A or x = A` by TARSKI:def 2;
        hence thesis by Th3,Th4;
        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:28;
        hence thesis by Th3,Th4;
      end;
    end;
    hence thesis;
  end;

theorem Th5:
  Kurat14Set A = { A, A` } \/ Kurat14ClPart A \/ Kurat14OpPart A
  proof
      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`)`)`)` } by Lm2
       .= { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
            Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } \/
          { A, A` } \/ Kurat14OpPart A by Def4
       .= { A, A` } \/ Kurat14ClPart A \/ Kurat14OpPart A by Def3;
    hence thesis;
  end;

definition let T, A;
  cluster Kurat14Set A -> finite;
  coherence
  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`)`)`)` };
     X \/ Y is finite;
    hence thesis by Def2;
  end;
end;

theorem Th6:
  for Q being Subset of T holds
    Q in Kurat14Set A implies Q` in Kurat14Set A & Cl 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 Q in Kurat14Set A;
then A1: Q in { A, k1, k2, k3, k4, k5, k6 } \/
         { A`, k7, k8, k9, k10, k11, k12 } by Def2;
    per cases by A1,XBOOLE_0:def 2;
    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:33;
      suppose
A3:   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)`)`)` } by ENUMSET1:34;
then A4:   Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
               Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` in { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
               Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by A3,ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A4,Def2;

      suppose
A5:   Q = Cl A;
      then Cl Q = Cl A by TOPS_1:26;
      then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
                Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
      then A6: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
                Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` in { A, k1, k2, k3, k4, k5, k6 } by A5,ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A6,Def2;

      suppose
A7:   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)`)`)` } by ENUMSET1:34;
      then A8: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
               Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` = Cl A by A7;
      then Q` in { A, Cl A, (Cl A)`, k3, k4, k5, k6 } by ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A8,Def2;

      suppose
A9:   Q = Cl (Cl A)`;
      then Cl Q = Cl (Cl A)` by TOPS_1:26;
      then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
                Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A10:  Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
               Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` in { A, k1, k2, k3, k4, k5, k6 } by A9,ENUMSET1:34;
      then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
            { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A10,Def2;

      suppose
A11:  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)`)`)` } by ENUMSET1:34;
then A12:  Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
               Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` = Cl (Cl A)` by A11;
      then Q` in { A, k1, k2, Cl (Cl A)`, k4, k5, k6 } by ENUMSET1:34;
      then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A12,Def2;

      suppose
A13:  Q = Cl (Cl (Cl A)`)`;
      then Cl Q = Cl (Cl (Cl A)`)` by TOPS_1:26;
      then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
                Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A14:  Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
                Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` in { A, k1, k2, k3, k4, k5, k6 } by A13,ENUMSET1:34;
      then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A14,Def2;

      suppose
A15:  Q = (Cl (Cl (Cl A)`)`)`;
       Cl (Cl (Cl (Cl A)`)`)` = Cl (Cl A)` by Th1;
      then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
                Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by A15,ENUMSET1:34;
then A16:  Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
                 Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` = Cl (Cl (Cl A)`)` by A15;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
      then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A16,Def2;
    end;
    hence thesis;

    suppose
A17:Q in { A`, k7, k8, k9, k10, k11, k12 };
     Q` in Kurat14Set A & Cl Q in Kurat14Set A
    proof
      per cases by A17,ENUMSET1:33;
      suppose
A18:  Q = A`;
      then Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12 } by ENUMSET1:34;
then A19:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
                Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
       Q` = A by A18;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A19,Def2;

      suppose
A20:  Q = Cl A`;
      then Cl Q = Cl A` by TOPS_1:26;
      then Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A21:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
       Q` in { A`, k7, (Cl A`)`, k9, k10, k11, k12} by A20,ENUMSET1:34;
      then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
           { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A21,Def2;

      suppose
A22:  Q = (Cl A`)`;
      then Cl Q in { A`, k7, k8, Cl (Cl A`)`, k10, k11, k12} by ENUMSET1:34;
then A23:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
       Q` = Cl A` by A22;
      then Q` in { A`, Cl A`, k8, k9, k10, k11, k12} by ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A23,Def2;

      suppose
A24:  Q = Cl (Cl A`)`;
      then Cl Q = Cl (Cl A`)` by TOPS_1:26;
      then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A25:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
       Q` in { A`, k7, k8, k9, k10, k11, k12} by A24,ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A25,Def2;

      suppose
A26:  Q = (Cl (Cl A`)`)`;
      then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A27:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
       Q` = Cl (Cl A`)` by A26;
      then Q` in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
          { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A27,Def2;

      suppose
A28:  Q = Cl (Cl (Cl A`)`)`;
      then Cl Q = Cl (Cl (Cl A`)`)` by TOPS_1:26;
      then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A29:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
       Q` in { A`, k7, k8, k9, k10, k11, k12} by A28,ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
         { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A29,Def2;

      suppose
A30:  Q = (Cl (Cl (Cl A`)`)`)`;
      then Cl Q = Cl (Cl A`)` by Th1;
      then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A31:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
              { A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
       Q` = Cl (Cl (Cl A`)`)` by A30;
      then Q` in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
      then Q` in { A, k1, k2, k3, k4, k5 , k6 } \/
             { A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
      hence thesis by A31,Def2;
    end;
    hence thesis;
  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`)`)`)` };
A1: card (X \/ Y) <= card X + card Y by CARD_2:62;
     card X <= 7 & card Y <= 7 by CARD_2:74;
    then card X + card Y <= 7 + 7 by REAL_1:55;
    then card (X \/ Y) <= 14 by A1,AXIOMS:22;
    hence thesis by Def2;
  end;

begin :: Seven Kuratowski Sets

definition let T, A;
  func Kurat7Set A -> Subset-Family of T equals :Def5:
     { 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 set;
      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:33;
      hence thesis;
    end;
    then X is Subset-Family of T by SETFAM_1:def 7;
    hence thesis;
  end;
end;

theorem Th8:
  A in Kurat7Set A & Int A in Kurat7Set A &
    Cl A in Kurat7Set A & Int Cl A in Kurat7Set A & Cl Int A in Kurat7Set A &
      Cl Int Cl A in Kurat7Set A & Int Cl Int A in Kurat7Set A
  proof
     Kurat7Set A = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
      Int Cl Int A } by Def5;
    hence thesis by ENUMSET1:34;
  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 Def5
      .= { A } \/ { Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
         Int Cl Int A } by ENUMSET1:56
      .= { A } \/ ({ Int A, Int Cl A, Int Cl Int A } \/
         { Cl A, Cl Int A, Cl Int Cl A }) by BORSUK_5:3
      .= { 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;

definition let T, A;
  cluster Kurat7Set A -> finite;
  coherence
  proof
    set X = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A };
     X is finite;
    hence thesis by Def5;
  end;
end;

theorem Th10:
  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;
    set k1 = Int A, k2 = Cl A, k3 = Int Cl A,
        k4 = Cl Int A, k5 = Cl Int Cl A, k6 = Int Cl Int A;
    assume Q in Kurat7Set A;
then A1: Q in { A, k1, k2, k3, k4, k5, k6} by Def5;
     Int Q in Kurat7Set A & Cl Q in Kurat7Set A
    proof
      per cases by A1,ENUMSET1:33;
      suppose
A2:   Q = A;
then A3:   Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
       Int Q in { A, k1, k2, k3, k4, k5, k6 } by A2,ENUMSET1:34;
      hence thesis by A3,Def5;

      suppose
A4:   Q = Int A;
then A5:   Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
       Int Q = Int A by A4,TOPS_1:45;
      then Int Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
      hence thesis by A5,Def5;

      suppose
A6:   Q = Cl A;
      then Cl Q = Cl A by TOPS_1:26;
then A7:   Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
       Int Q in { A, k1, k2, k3, k4, k5, k6 } by A6,ENUMSET1:34;
      hence thesis by A7,Def5;

      suppose
A8:   Q = Int Cl A;
then A9:   Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
       Int Q = Int Cl A by A8,TOPS_1:45;
      then Int Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
      hence thesis by A9,Def5;

      suppose
A10:  Q = Cl Int A;
      then Cl Q = Cl Int A by TOPS_1:26;
then A11:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
       Int Q in { A, k1, k2, k3, k4, k5, k6 } by A10,ENUMSET1:34;
      hence thesis by A11,Def5;

      suppose
A12:  Q = Cl Int Cl A;
      then Cl Q = Cl Int Cl A by TOPS_1:26;
then A13:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
       Int Cl Int Cl A = Int Cl A by TDLAT_1:5;
      then Int Q in { A, k1, k2, k3, k4, k5, k6 } by A12,ENUMSET1:34;
      hence thesis by A13,Def5;

      suppose
A14:  Q = Int Cl Int A;
      then Cl Q = Cl Int A by TOPS_1:58;
then A15:  Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
       Int Q = Int Cl Int A by A14,TOPS_1:45;
      then Int Q in { A, k1, k2, k3, k4, k5, k6} by ENUMSET1:34;
      hence thesis by A15,Def5;
    end;
    hence thesis;
  end;

theorem
   card Kurat7Set A <= 7
  proof
     Kurat7Set A = { A, Int A, Cl A, Int Cl A, Cl Int A,
      Cl Int Cl A, Int Cl Int A } by Def5;
    hence thesis by CARD_2:74;
  end;

begin :: The Set Generating Exactly Fourteen Kuratowski Sets

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

theorem Th12:
  Cl KurExSet = {1} \/ [. 2,+infty.[
  proof
    reconsider B = {1},
      C = RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[ as Subset of R^1
        by TOPMETR:24;
    set A = KurExSet;
     A = {1} \/ (RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[)
      by Def6,XBOOLE_1:113;
then A1: Cl A = Cl B \/ Cl C by PRE_TOPC:50;
     Cl B = {1} by BORSUK_5:61;
    hence Cl A = {1} \/ [. 2,+infty.[ by A1,BORSUK_5:82;
  end;

theorem Th13:
  (Cl KurExSet)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;

theorem Th14:
  Cl (Cl KurExSet)` = ].-infty, 2 .] by Th13,BORSUK_5:96;

theorem Th15:
  (Cl (Cl KurExSet)`)` = ]. 2,+infty.[ by Th14,BORSUK_5:98;

theorem Th16:
  Cl (Cl (Cl KurExSet)`)` = [. 2,+infty.[ by Th15,BORSUK_5:75;

theorem Th17:
  (Cl (Cl (Cl KurExSet)`)`)` = ].-infty, 2 .[ by Th16,BORSUK_5:99;

theorem Th18:
  KurExSet` = ].-infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}
  proof
    reconsider B = {1},
      C = RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[ as Subset of R^1
        by TOPMETR:24;
    set A = KurExSet;
    A1: A = {1} \/ (RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[)
      by Def6,XBOOLE_1:113;
A2: B` = ].-infty, 1 .[ \/ ]. 1,+infty.[ by BORSUK_5:90;
     C` = ].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4} by BORSUK_5:89;
    hence thesis by A1,A2,BORSUK_5:92,WAYBEL12:5;
  end;

theorem Th19:
  Cl KurExSet` = ].-infty, 3 .] \/ {4} by Th18,BORSUK_5:101;

theorem Th20:
  (Cl KurExSet`)` = ]. 3, 4 .[ \/ ]. 4,+infty.[ by Th19,BORSUK_5:102;

theorem Th21:
  Cl (Cl KurExSet`)` = [. 3,+infty.[ by Th20,BORSUK_5:81;

theorem Th22:
  (Cl (Cl KurExSet`)`)` = ].-infty, 3 .[ by Th21,BORSUK_5:99;

theorem Th23:
  Cl (Cl (Cl KurExSet`)`)` = ].-infty, 3 .] by Th22,BORSUK_5:77;

theorem Th24:
  (Cl (Cl (Cl KurExSet`)`)`)` = ]. 3,+infty.[ by Th23,BORSUK_5:98;

begin :: The Set Generating Exactly Seven Kuratowski Sets

theorem Th25:
  Int KurExSet = ]. 3, 4 .[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;

theorem Th26:
  Cl Int KurExSet = [. 3,+infty.[
  proof
    set A = KurExSet;
     Cl (Cl A`)` = [. 3,+infty.[ by Th20,BORSUK_5:81;
    hence thesis by TOPS_1:def 1;
  end;

theorem Th27:
  Int Cl Int KurExSet = ]. 3,+infty.[
  proof
    set A = KurExSet;
     (Cl (Cl A`)`)` = ].-infty, 3 .[ by Th21,BORSUK_5:99;
then A1: Cl (Cl (Cl A`)`)` = ].-infty, 3 .] by BORSUK_5:77;
     Cl Int A = Cl (Cl A`)` by TOPS_1:def 1;
    then Int Cl Int A = (Cl (Cl (Cl A`)`)`)` by TOPS_1:def 1;
    hence thesis by A1,BORSUK_5:98;
  end;

theorem Th28:
  Int Cl KurExSet = ]. 2,+infty.[
  proof
    set A = KurExSet;
     (Cl A)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;
    then Cl (Cl A)` = ].-infty, 2 .] by BORSUK_5:96;
    then (Cl (Cl A)`)` = ]. 2,+infty.[ by BORSUK_5:98;
    hence thesis by TOPS_1:def 1;
  end;

theorem Th29:
  Cl Int Cl KurExSet = [. 2,+infty.[
  proof
    set A = KurExSet;
     (Cl A)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;
    then Cl (Cl A)` = ].-infty, 2 .] by BORSUK_5:96;
    then (Cl (Cl A)`)` = ]. 2,+infty.[ by BORSUK_5:98;
    then Cl (Cl (Cl A)`)` = [. 2,+infty.[ by BORSUK_5:75;
    hence thesis by TOPS_1:def 1;
  end;

begin :: The Difference Between Chosen Kuratowski Sets

theorem
   Cl Int Cl KurExSet <> Int Cl KurExSet
  proof
    set A = KurExSet;
     2 in Cl Int Cl A by Th29,BORSUK_5:15;
    hence thesis by Th28,BORSUK_5:14;
  end;

theorem Th31:
  Cl Int Cl KurExSet <> Cl KurExSet
  proof
    set A = KurExSet;
     1 in {1} by TARSKI:def 1;
    then 1 in Cl A by Th12,XBOOLE_0:def 2;
    hence thesis by Th29,BORSUK_5:15;
  end;

theorem
   Cl Int Cl KurExSet <> Int Cl Int KurExSet
  proof
    set A = KurExSet;
     3 in Cl Int Cl A by Th29,BORSUK_5:15;
    hence thesis by Th27,BORSUK_5:14;
  end;

theorem Th33:
  Cl Int Cl KurExSet <> Cl Int KurExSet
  proof
    set A = KurExSet;
     2 in Cl Int Cl A by Th29,BORSUK_5:15;
    hence Cl Int Cl A <> Cl Int A by Th26,BORSUK_5:15;
  end;

theorem
   Cl Int Cl KurExSet <> Int KurExSet
  proof
    set A = KurExSet;
A1: 2 in Cl Int Cl A by Th29,BORSUK_5:15;
     Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
    hence thesis by A1,BORSUK_5:86;
  end;

theorem
   Int Cl KurExSet <> Cl KurExSet
  proof
    set A = KurExSet;
     1 in {1} by TARSKI:def 1;
    then 1 in Cl A by Th12,XBOOLE_0:def 2;
    hence thesis by Th28,BORSUK_5:14;
  end;

theorem
   Int Cl KurExSet <> Int Cl Int KurExSet
  proof
    set A = KurExSet;
     3 in Int Cl A by Th28,BORSUK_5:14;
    hence Int Cl A <> Int Cl Int A by Th27,BORSUK_5:14;
  end;

theorem
   Int Cl KurExSet <> Cl Int KurExSet
  proof
    set A = KurExSet;
    assume Int Cl A = Cl Int A;
    then Int Cl A = {} or Int Cl A = REAL by BORSUK_5:57;
    hence thesis by Th28,BORSUK_5:71;
  end;

theorem Th38:
  Int Cl KurExSet <> Int KurExSet
  proof
    set A = KurExSet;
A1: 4 in Int Cl A by Th28,BORSUK_5:14;
     Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
    hence thesis by A1,BORSUK_5:87;
  end;

theorem
   Int Cl Int KurExSet <> Cl KurExSet
  proof
    set A = KurExSet;
     2 in [. 2,+infty.[ by BORSUK_5:15;
    then 2 in Cl A by Th12,XBOOLE_0:def 2;
    hence thesis by Th27,BORSUK_5:14;
  end;

theorem Th40:
  Cl Int KurExSet <> Cl KurExSet
  proof
    set A = KurExSet;
     2 in [. 2,+infty.[ by BORSUK_5:15;
    then 2 in Cl A by Th12,XBOOLE_0:def 2;
    hence thesis by Th26,BORSUK_5:15;
  end;

theorem
   Int KurExSet <> Cl KurExSet
  proof
    set A = KurExSet;
     4 in [. 2,+infty.[ by BORSUK_5:15;
then A1: 4 in Cl A by Th12,XBOOLE_0:def 2;
     Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
    hence thesis by A1,BORSUK_5:87;
  end;

theorem Th42:
  Cl KurExSet <> KurExSet
  proof
    set A = KurExSet;
     4 in [. 2,+infty.[ by BORSUK_5:15;
then A1: 4 in Cl A by Th12,XBOOLE_0:def 2;
A2: not 4 in ]. 3, 4 .[ by JORDAN6:45;
A3: not 4 in ]. 4,+infty.[ by BORSUK_5:14;
     not 4 in {1} & not 4 in RAT (2, 3) by BORSUK_5:52,TARSKI:def 1;
    then not 4 in {1} \/ RAT (2, 3) by XBOOLE_0:def 2;
    then not 4 in {1} \/ RAT (2, 3) \/ ]. 3, 4 .[ by A2,XBOOLE_0:def 2;
    hence thesis by A1,A3,Def6,XBOOLE_0:def 2;
  end;

theorem Th43:
  KurExSet <> Int KurExSet
  proof
    set A = KurExSet;
     1 in { 1 } by TARSKI:def 1;
    then 1 in {1} \/ RAT (2,3) by XBOOLE_0:def 2;
    then 1 in {1} \/ RAT (2,3) \/ ]. 3, 4 .[ by XBOOLE_0:def 2;
then A1: 1 in A by Def6,XBOOLE_0:def 2;
     Int A = ]. 3, 4 .[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
    hence thesis by A1,BORSUK_5:86;
  end;

theorem
   Cl Int KurExSet <> Int Cl Int KurExSet
  proof
    set A = KurExSet;
     3 in Cl Int A by Th26,BORSUK_5:15;
    hence Cl Int A <> Int Cl Int A by Th27,BORSUK_5:14;
  end;

theorem Th45:
  Int Cl Int KurExSet <> Int KurExSet
  proof
    set A = KurExSet;
A1: 4 in Int Cl Int A by Th27,BORSUK_5:14;
     Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
    hence Int Cl Int A <> Int A by A1,BORSUK_5:87;
  end;

theorem
   Cl Int KurExSet <> Int KurExSet
  proof
    set A = KurExSet;
A1: 3 in Cl Int A by Th26,BORSUK_5:15;
     Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
    hence Cl Int A <> Int A by A1,BORSUK_5:86;
  end;

begin :: Final Proofs For Seven

theorem Th47:
  Int Cl Int KurExSet <> Int Cl KurExSet
  proof
    set A = KurExSet;
     not 3 in Int Cl Int A by Th27,BORSUK_5:14;
    hence thesis by Th28,BORSUK_5:14;
  end;

theorem Th48:
  Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet are_mutually_different
  proof
    set A1 = Int KurExSet, A2 = Int Cl KurExSet, A3 = Int Cl Int KurExSet;
    thus A1 <> A2 by Th38;
    thus A2 <> A3 by Th47;
    thus A3 <> A1 by Th45;
  end;

theorem Th49:
  Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_different
  proof
    set A1 = Cl KurExSet, A2 = Cl Int KurExSet, A3 = Cl Int Cl KurExSet;
    thus A1 <> A2 by Th40;
    thus A2 <> A3 by Th33;
    thus A3 <> A1 by Th31;
  end;

theorem Th50:
  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:13;
     suppose X = Int KurExSet;
     hence thesis by Th20,TOPS_1:def 1;
     suppose X = Int Cl KurExSet;
     hence thesis by Th28;
     suppose X = Int Cl Int KurExSet;
     hence thesis by Th27;
   end;

theorem
   for X being set st X in
    { Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } holds
   X is closed Subset of R^1 by ENUMSET1:13;

theorem Th52:
  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:13;
    suppose X = Int KurExSet;
    hence thesis by Th25,BORSUK_5:87;
    suppose X = Int Cl KurExSet;
    hence thesis by Th28,BORSUK_5:71;
    suppose X = Int Cl Int KurExSet;
    hence thesis by Th27,BORSUK_5:71;
  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:13;
    suppose
A2: X = Cl KurExSet;
A3: not 0 in {1} by TARSKI:def 1;
     not 0 in [. 2,+infty.[ by BORSUK_5:15;
    hence thesis by A2,A3,Th12,XBOOLE_0:def 2;
    suppose X = Cl Int KurExSet;
    hence thesis by Th26,BORSUK_5:72;
    suppose X = Cl Int Cl KurExSet;
    hence thesis by Th29,BORSUK_5:72;
  end;

theorem Th54:
  { 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 set such that
A1: x in X & 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,Th50,ENUMSET1:13;
    then x = REAL by BORSUK_5:57;
    hence thesis by A1,Th52;
  end;

theorem Th55:
  Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
    Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet
      are_mutually_different by Th48,Th49,Th54,BORSUK_5:7;

definition
  cluster KurExSet -> non closed non open;
  coherence by Th42,Th43,PRE_TOPC:52,TOPS_1:55;
end;

theorem Th56:
  { 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:56;
    per cases by A1,ENUMSET1:28;
    suppose A = Int A;
    hence thesis;
    suppose A = Int Cl A;
    hence thesis;
    suppose A = Int Cl Int A;
    hence thesis;
    suppose A = Cl A;
    hence thesis;
    suppose A = Cl Int A;
    hence thesis;
    suppose A = Cl Int Cl A;
    hence thesis;
  end;

theorem Th57:
  KurExSet, Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
    Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_different
  proof
     Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
      Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet, KurExSet
        are_mutually_different by Th55,Th56,BORSUK_5:8;
    hence thesis by BORSUK_5:9;
  end;

theorem
   card Kurat7Set KurExSet = 7
  proof
    set A = KurExSet;
A1: Kurat7Set A = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
      Int Cl Int A } by Def5;
     A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A
      are_mutually_different by Th57,BORSUK_5:10;
    hence thesis by A1,BORSUK_5:5;
  end;

begin :: Final Proofs For Fourteen

definition
  cluster Kurat14ClPart KurExSet -> with_proper_subsets;
  coherence
  proof
    set A = KurExSet;
    assume the carrier of R^1 in Kurat14ClPart KurExSet;
then A1: REAL in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
         Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3,TOPMETR:24;
    per cases by A1,ENUMSET1:28;
    suppose REAL = Cl A;
    hence thesis by Th12,BORSUK_5:103;
    suppose REAL = Cl (Cl A)`;
    hence thesis by Th14,BORSUK_5:73;
    suppose REAL = Cl (Cl (Cl A)`)`;
    hence thesis by Th16,BORSUK_5:72;
    suppose REAL = Cl A`;
    hence thesis by Th19,BORSUK_5:104;
    suppose REAL = Cl (Cl A`)`;
    hence thesis by Th21,BORSUK_5:72;
    suppose REAL = Cl (Cl (Cl A`)`)`;
    hence thesis by Th23,BORSUK_5:73;
  end;
  cluster Kurat14OpPart KurExSet -> with_proper_subsets;
  coherence
  proof
    set A = KurExSet;
    assume the carrier of R^1 in Kurat14OpPart KurExSet;
then A2: REAL in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
         (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4,TOPMETR:24;
    per cases by A2,ENUMSET1:28;
    suppose REAL = (Cl A)`;
    hence thesis by Th12,BORSUK_5:106;
    suppose REAL = (Cl (Cl A)`)`;
    hence thesis by Th14,BORSUK_5:106;
    suppose REAL = (Cl (Cl (Cl A)`)`)`;
    hence thesis by Th16,BORSUK_5:106;
    suppose REAL = (Cl A`)`;
    hence thesis by Th19,BORSUK_5:106;
    suppose REAL = (Cl (Cl A`)`)`;
    hence thesis by Th21,BORSUK_5:106;
    suppose REAL = (Cl (Cl (Cl A`)`)`)`;
    hence thesis by Th23,BORSUK_5:106;
  end;
end;

definition
  cluster Kurat14Set KurExSet -> with_proper_subsets;
  coherence
  proof
     { KurExSet, KurExSet` } is Subset-Family of R^1
      by MEASURE1:7;
    then reconsider AA = { KurExSet, KurExSet` } as Subset-Family of R^1
     ;
     AA is with_proper_subsets
    proof
      assume
A1:   the carrier of R^1 in AA;
      per cases by A1,TARSKI:def 2,TOPMETR:24;
      suppose REAL = KurExSet;
      then [#]R^1 = KurExSet by PRE_TOPC:12,TOPMETR:24;
      hence thesis;
      suppose REAL = KurExSet`;
      then [#]R^1 = KurExSet` by PRE_TOPC:12,TOPMETR:24;
      hence thesis by TOPS_1:29;
    end;
then A2: AA \/ Kurat14ClPart KurExSet is with_proper_subsets by BORSUK_5:115;
     Kurat14Set KurExSet =
      AA \/ Kurat14ClPart KurExSet \/ Kurat14OpPart KurExSet by Th5;
    hence thesis by A2,BORSUK_5:115;
  end;
end;

definition
  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;
    then [#]R^1 in Kurat14Set KurExSet by PRE_TOPC:27;
    then the carrier of R^1 in Kurat14Set KurExSet by PRE_TOPC:12;
    hence thesis by BORSUK_5:def 6;
  end;
end;

theorem Th59:
  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,AMI_1:def 1;
  end;

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

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

theorem Th60:
  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 set such that
A2: x in F and
A3: x in G by XBOOLE_0:3;
    reconsider x as Subset of R^1 by A2;
A4: x is open by A1,A2,BORSUK_5:def 7;
     x is closed by A1,A3,BORSUK_5:def 8;
    then x = {} or x = REAL by A4,BORSUK_5:57;
    hence thesis by A2,AMI_1:def 1,BORSUK_5:def 6,TOPMETR:24;
  end;

definition
  cluster Kurat14ClPart KurExSet -> closed;
  coherence
  proof
    set A = KurExSet;
    let P be Subset of R^1;
    assume P in Kurat14ClPart KurExSet;
    then P in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
         Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3;
    hence thesis by ENUMSET1:28;
  end;
  cluster Kurat14OpPart KurExSet -> open;
  coherence
  proof
    set A = KurExSet;
    let P be Subset of R^1;
    assume P in Kurat14OpPart KurExSet;
    then P in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
           (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4;
    hence thesis by ENUMSET1:28;
  end;
end;

theorem Th61:
  Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th60;

definition let T, A;
  cluster Kurat14ClPart A -> finite;
  coherence
  proof
     Kurat14ClPart A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
           Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3;
    hence thesis;
  end;
  cluster Kurat14OpPart A -> finite;
  coherence
  proof
      Kurat14OpPart A = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
           (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4;
    hence thesis;
  end;
end;

theorem Th62:
  card (Kurat14ClPart KurExSet) = 6
  proof
    set A = KurExSet;
A1:  Kurat14ClPart A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
           Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3;
A2:  Cl (Cl (Cl A`)`)` = ].-infty, 3 .] by Th22,BORSUK_5:77;
A3:  not 3 in Cl (Cl A)` by Th14,BORSUK_5:16;
      not 5 in ].-infty, 3 .] & not 5 in {4} by BORSUK_5:16,TARSKI:def 1;
then A4:  not 5 in Cl A` by Th19,XBOOLE_0:def 2;
A5:  not 4 in Cl (Cl (Cl A`)`)` by Th23,BORSUK_5:16;
      4 in [. 2,+infty.[ by BORSUK_5:15;
then A6:  Cl A <> Cl (Cl (Cl A`)`)` by A5,Th12,XBOOLE_0:def 2;
A7:  Cl (Cl (Cl A)`)` = [. 2,+infty.[ by Th15,BORSUK_5:75;
A8:  3 in Cl (Cl (Cl A)`)` by Th16,BORSUK_5:15;
A9:  Cl (Cl A)` <> Cl (Cl (Cl A`)`)` by A2,A3,BORSUK_5:16;
A10: Cl (Cl (Cl A)`)` <> Cl A` by A4,A7,BORSUK_5:15;
      4 in Cl (Cl (Cl A)`)` by Th16,BORSUK_5:15;
then A11: Cl (Cl (Cl A)`)` <> Cl (Cl (Cl A`)`)` by Th23,BORSUK_5:16;
A12: Cl Int Cl A = Cl (Cl (Cl A)`)` & Cl Int A = Cl (Cl A`)` by TOPS_1:def 1;
      4 in {4} by TARSKI:def 1;
then A13: 4 in Cl A` by Th19,XBOOLE_0:def 2;
A14: not 4 in Cl (Cl (Cl A`)`)` by Th23,BORSUK_5:16;
A15: Cl A` <> Cl (Cl (Cl A`)`)` by A2,A13,BORSUK_5:16;
      Cl (Cl A`)` = [. 3,+infty.[ by Th20,BORSUK_5:81;
     then Cl (Cl A`)` <> Cl (Cl (Cl A`)`)` by A14,BORSUK_5:15;
     then Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`,
          Cl (Cl A`)`, Cl (Cl (Cl A`)`)`
       are_mutually_different by A3,A6,A8,A9,A10,A11,A12,A15,Th31,Th33,BORSUK_5
:def 1;
     hence thesis by A1,BORSUK_5:4;
  end;

theorem Th63:
  card (Kurat14OpPart KurExSet) = 6
  proof
     set A = KurExSet;
A1:  Kurat14OpPart A = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
           (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4;
A2:  (Cl A)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;
A3:  (Cl (Cl (Cl A)`)`)` = ].-infty, 2 .[ by Th16,BORSUK_5:99;
A4:  (Cl (Cl (Cl A`)`)`)` = ]. 3,+infty.[ by Th23,BORSUK_5:98;
A5:  3 in (Cl (Cl A)`)` by Th15,BORSUK_5:14;
      5 in ]. 4,+infty.[ by BORSUK_5:14;
then A6:  5 in (Cl A`)` by Th20,XBOOLE_0:def 2;
A7:  4 in (Cl (Cl (Cl A`)`)`)` by Th24,BORSUK_5:14;
      not 4 in ].-infty, 1 .[ & not 4 in ]. 1, 2 .[
       by BORSUK_5:17,JORDAN6:45;
then A8:  (Cl A)` <> (Cl (Cl (Cl A`)`)`)` by A2,A7,XBOOLE_0:def 2;
      (Cl A)` <> (Cl Int Cl A)` by Th31,BORSUK_5:105;
then A9:  (Cl A)` <> (Cl (Cl (Cl A)`)`)` by TOPS_1:def 1;
A10: (Cl (Cl A)`)` <> (Cl (Cl (Cl A)`)`)` by A3,A5,BORSUK_5:17;
A11: (Cl (Cl A)`)` <> (Cl (Cl (Cl A`)`)`)` by A4,A5,BORSUK_5:14;
A12: (Cl (Cl (Cl A)`)`)` <> (Cl A`)` by A3,A6,BORSUK_5:17;
A13: not 4 in (Cl (Cl (Cl A)`)`)` by Th17,BORSUK_5:17;
      (Cl Int Cl A)` = (Cl (Cl (Cl A)`)`)` & (Cl Int A)` = (Cl (Cl A`)`)`
       by TOPS_1:def 1;
then A14: (Cl (Cl (Cl A)`)`)` <> (Cl (Cl A`)`)` by Th33,BORSUK_5:105;
A15: not 4 in ]. 3, 4 .[ by JORDAN6:45;
      not 4 in ]. 4,+infty.[ by BORSUK_5:14;
then A16: not 4 in (Cl A`)` by A15,Th20,XBOOLE_0:def 2;
A17: 4 in (Cl (Cl (Cl A`)`)`)` by Th24,BORSUK_5:14;
      not 4 in (Cl (Cl A`)`)` by Th22,BORSUK_5:17;
     then (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
         (Cl A`)`, (Cl (Cl A`)`)`,
       (Cl (Cl (Cl A`)`)`)` are_mutually_different
       by A8,A9,A10,A11,A12,A13,A14,A16,A17,BORSUK_5:def 1;
     hence thesis by A1,BORSUK_5:4;
  end;

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

definition
  cluster KurExSet -> non empty;
  coherence by Def6;
end;

theorem Th65:
  KurExSet <> KurExSet`
  proof
    assume KurExSet = KurExSet`;
    then KurExSet meets KurExSet` by XBOOLE_1:66;
    hence thesis by PRE_TOPC:26;
  end;

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

theorem
    card Kurat14Set KurExSet = 14
  proof
    set A = KurExSet;
A1: card (Kurat14ClPart A \/ Kurat14OpPart A) = 6 + 6
      by Th61,Th62,Th63,CARD_2:53
        .= 12;
    set B = { A, A` };
A2: B misses (Kurat14ClPart A \/ Kurat14OpPart A) by Th64,Th66,XBOOLE_1:70;
     card Kurat14Set A = card (B \/ Kurat14ClPart A \/ Kurat14OpPart A) by Th5
       .= card (B \/ (Kurat14ClPart A \/ Kurat14OpPart A)) by XBOOLE_1:4
       .= card B + card (Kurat14ClPart A \/ Kurat14OpPart A) by A2,CARD_2:53
       .= 2 + 12 by A1,Th65,CARD_2:76
       .= 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;

definition let T be 1-sorted, A be Subset-Family of T;
  attr A is compl-closed means
      for P being Subset of T st
      P in A holds P` in A;
end;

definition let T, A;
  cluster Kurat14Set A -> non empty;
  coherence by Th3;
  cluster Kurat14Set A -> Cl-closed;
  coherence
  proof
    let P be Subset of T;
    assume P in Kurat14Set A;
    hence thesis by Th6;
  end;
  cluster Kurat14Set A -> compl-closed;
  coherence
  proof
    let P be Subset of T;
    assume P in Kurat14Set A;
    hence thesis by Th6;
  end;
end;

definition let T, A;
  cluster Kurat7Set A -> non empty;
  coherence by Th8;
  cluster Kurat7Set A -> Int-closed;
  coherence
  proof
    let P be Subset of T;
    assume P in Kurat7Set A;
    hence thesis by Th10;
  end;
  cluster Kurat7Set A -> Cl-closed;
  coherence
  proof
    let P be Subset of T;
    assume P in Kurat7Set A;
    hence thesis by Th10;
  end;
end;

definition let T;
  cluster Int-closed Cl-closed non empty Subset-Family of T;
  existence
  proof
    consider A being Subset of T;
    take Kurat7Set A;
    thus thesis;
  end;
  cluster compl-closed Cl-closed non empty Subset-Family of T;
  existence
  proof
    consider A being Subset of T;
    take Kurat14Set A;
    thus thesis;
  end;
end;

Back to top