kurato_1.miz



    begin

    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 :: KURATO_1:1

    

     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 be 1-sorted, A,B be Subset-Family of T holds (A \/ B) is Subset-Family of T;

    definition

      let T, A;

      :: KURATO_1:def1

      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;

      :: KURATO_1:def2

      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 :: KURATO_1:2

    ( Kurat14Set A) = (( Kurat14Part A) \/ ( Kurat14Part (A ` )));

    theorem :: KURATO_1:3

    

     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 :: KURATO_1:4

    

     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;

      :: KURATO_1:def3

      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;

      :: KURATO_1:def4

      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 :: KURATO_1:5

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

    registration

      let T, A;

      cluster ( Kurat14Set A) -> finite;

      coherence ;

    end

    theorem :: KURATO_1:6

    

     Th6: for Q be 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 :: KURATO_1:7

    ( 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

    definition

      let T, A;

      :: KURATO_1:def5

      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 :: KURATO_1:8

    ( 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 :: KURATO_1:9

    

     Th9: for Q be 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

    definition

      :: KURATO_1:def6

      func KurExSet -> Subset of R^1 equals ((( {1} \/ ( RAT (2,4))) \/ ].4, 5.[) \/ ].5, +infty .[);

      coherence by TOPMETR: 17;

    end

    theorem :: KURATO_1:10

    

     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 :: KURATO_1:11

    

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

    theorem :: KURATO_1:12

    

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

    theorem :: KURATO_1:13

    

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

    theorem :: KURATO_1:14

    

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

    theorem :: KURATO_1:15

    

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

    theorem :: KURATO_1:16

    

     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 :: KURATO_1:17

    

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

    theorem :: KURATO_1:18

    

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

    theorem :: KURATO_1:19

    

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

    theorem :: KURATO_1:20

    

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

    theorem :: KURATO_1:21

    

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

    theorem :: KURATO_1:22

    

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

    begin

    theorem :: KURATO_1:23

    

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

    theorem :: KURATO_1:24

    

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

    theorem :: KURATO_1:25

    

     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, XXREAL_1: 294;

      then ( Cl (( Cl (( Cl (A ` )) ` )) ` )) = ]. -infty , 4.] by BORSUK_5: 51;

      hence thesis by A1, TOPMETR: 17, XXREAL_1: 224, XXREAL_1: 288;

    end;

    theorem :: KURATO_1:26

    

     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, XXREAL_1: 288;

      hence thesis by TOPS_1:def 1;

    end;

    theorem :: KURATO_1:27

    

     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, XXREAL_1: 288;

      hence thesis by BORSUK_5: 49, TOPS_1:def 1;

    end;

    begin

    theorem :: KURATO_1:28

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

    theorem :: KURATO_1:29

    

     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 :: KURATO_1:30

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

    theorem :: KURATO_1:31

    

     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 :: KURATO_1:32

    ( 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 :: KURATO_1:33

    ( 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 :: KURATO_1:34

    ( 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 :: KURATO_1:35

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

    theorem :: KURATO_1:36

    

     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 :: KURATO_1:37

    ( 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 :: KURATO_1:38

    

     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 :: KURATO_1:39

    ( 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 :: KURATO_1:40

    

     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 :: KURATO_1:41

    

     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 :: KURATO_1:42

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

    theorem :: KURATO_1:43

    

     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 :: KURATO_1:44

    ( 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

    theorem :: KURATO_1:45

    

     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 :: KURATO_1:46

    

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

    theorem :: KURATO_1:47

    

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

    theorem :: KURATO_1:48

    

     Th48: for X be 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 :: KURATO_1:49

    

     Th49: for X be 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 :: KURATO_1:50

    for X be 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 :: KURATO_1:51

    

     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 be 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 :: KURATO_1:52

    

     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 :: KURATO_1:53

     {( 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 :: KURATO_1:54

    

     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 :: KURATO_1:55

    ( 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

    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 :: KURATO_1:56

    

     Th56: for A be with_non-empty_elements set, B be 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 :: KURATO_1:57

    

     Th57: for F,G be 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 be 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 :: KURATO_1:58

    ( Kurat14ClPart KurExSet ) misses ( Kurat14OpPart KurExSet ) by Th57;

    registration

      let T, A;

      cluster ( Kurat14ClPart A) -> finite;

      coherence ;

      cluster ( Kurat14OpPart A) -> finite;

      coherence ;

    end

    theorem :: KURATO_1:59

    

     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, XXREAL_1: 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 :: KURATO_1:60

    

     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, XXREAL_1: 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, XXREAL_1: 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, XXREAL_1: 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 :: KURATO_1:61

    

     Th61: { KurExSet , ( KurExSet ` )} misses ( Kurat14ClPart KurExSet )

    proof

      set A = KurExSet ;

      assume {A, (A ` )} meets ( Kurat14ClPart A);

      then

      consider x be 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 :: KURATO_1:62

    

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

    theorem :: KURATO_1:63

    

     Th63: { KurExSet , ( KurExSet ` )} misses ( Kurat14OpPart KurExSet )

    proof

      set A = KurExSet ;

      assume {A, (A ` )} meets ( Kurat14OpPart A);

      then

      consider x be 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;

    ::$Notion-Name

    theorem :: KURATO_1:64

    ( 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

    definition

      let T be TopStruct, A be Subset-Family of T;

      :: KURATO_1:def7

      attr A is Cl-closed means for P be Subset of T st P in A holds ( Cl P) in A;

      :: KURATO_1:def8

      attr A is Int-closed means for P be 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