isomichi.miz



    begin

    reserve T for TopSpace,

A,B for Subset of T;

    registration

      let D be non trivial set;

      cluster ( ADTS D) -> non trivial;

      coherence

      proof

        ( ADTS D) = TopStruct (# D, ( cobool D) #) by TEX_1:def 3;

        hence thesis;

      end;

    end

    registration

      cluster anti-discrete non trivial strict for TopSpace;

      existence

      proof

        set D = the non trivial set;

        take ( ADTS D);

        thus thesis;

      end;

    end

    theorem :: ISOMICHI:1

    

     Th1: (( Int ( Cl ( Int A))) /\ ( Int ( Cl ( Int B)))) = ( Int ( Cl ( Int (A /\ B))))

    proof

      set C = ( Int A), D = ( Int B);

      (( Int ( Cl C)) /\ ( Int ( Cl D))) = ( Int ( Cl (C /\ D))) by TDLAT_1: 7;

      hence thesis by TOPS_1: 17;

    end;

    theorem :: ISOMICHI:2

    

     Th2: ( Cl ( Int ( Cl (A \/ B)))) = (( Cl ( Int ( Cl A))) \/ ( Cl ( Int ( Cl B))))

    proof

      set C = ( Cl A), D = ( Cl B);

      (( Cl ( Int C)) \/ ( Cl ( Int D))) = ( Cl ( Int (C \/ D))) by TDLAT_1: 6;

      hence thesis by PRE_TOPC: 20;

    end;

    begin

    definition

      let T be TopStruct, A be Subset of T;

      :: ISOMICHI:def1

      attr A is supercondensed means

      : Def1: ( Int ( Cl A)) = ( Int A);

      :: ISOMICHI:def2

      attr A is subcondensed means

      : Def2: ( Cl ( Int A)) = ( Cl A);

    end

    registration

      let T;

      cluster closed -> supercondensed for Subset of T;

      coherence by PRE_TOPC: 22;

    end

    theorem :: ISOMICHI:3

    A is closed implies A is supercondensed;

    theorem :: ISOMICHI:4

    A is open implies A is subcondensed by TOPS_1: 23;

    definition

      let T be TopSpace, A be Subset of T;

      :: original: condensed

      redefine

      :: ISOMICHI:def3

      attr A is condensed means ( Cl ( Int A)) = ( Cl A) & ( Int ( Cl A)) = ( Int A);

      compatibility

      proof

        thus A is condensed implies ( Cl ( Int A)) = ( Cl A) & ( Int ( Cl A)) = ( Int A) by TDLAT_3: 9;

        assume that

         A1: ( Cl ( Int A)) = ( Cl A) and

         A2: ( Int ( Cl A)) = ( Int A);

        

         A3: ( Int A) c= A by TOPS_1: 16;

        A c= ( Cl ( Int A)) by A1, PRE_TOPC: 18;

        hence thesis by A2, A3, TOPS_1:def 6;

      end;

    end

    theorem :: ISOMICHI:5

    A is condensed iff A is subcondensed & A is supercondensed;

    registration

      let T be TopSpace;

      cluster condensed -> subcondensed supercondensed for Subset of T;

      coherence ;

      cluster subcondensed supercondensed -> condensed for Subset of T;

      coherence ;

    end

    registration

      let T be TopSpace;

      cluster condensed subcondensed supercondensed for Subset of T;

      existence

      proof

        set A = ( {} T);

        take A;

        A is supercondensed subcondensed;

        hence thesis;

      end;

    end

    theorem :: ISOMICHI:6

    A is supercondensed implies (A ` ) is subcondensed

    proof

      

       A1: (( Int A) ` ) = ( Cl (A ` )) by TDLAT_3: 2;

      assume A is supercondensed;

      then

       A2: (( Int ( Cl A)) ` ) = (( Int A) ` );

      (( Int ( Cl A)) ` ) = ( Cl (( Cl A) ` )) by TDLAT_3: 2

      .= ( Cl ( Int (A ` ))) by TDLAT_3: 3;

      hence thesis by A2, A1;

    end;

    theorem :: ISOMICHI:7

    A is subcondensed implies (A ` ) is supercondensed

    proof

      

       A1: (( Cl A) ` ) = ( Int (A ` )) by TDLAT_3: 3;

      assume A is subcondensed;

      then

       A2: (( Cl ( Int A)) ` ) = (( Cl A) ` );

      (( Cl ( Int A)) ` ) = ( Int (( Int A) ` )) by TDLAT_3: 3

      .= ( Int ( Cl (A ` ))) by TDLAT_3: 2;

      hence thesis by A2, A1;

    end;

    theorem :: ISOMICHI:8

    

     Th8: A is supercondensed iff ( Int ( Cl A)) c= A

    proof

      thus A is supercondensed implies ( Int ( Cl A)) c= A by TOPS_1: 16;

      assume ( Int ( Cl A)) c= A;

      then

       A1: ( Int ( Int ( Cl A))) c= ( Int A) by TOPS_1: 19;

      ( Int A) c= ( Int ( Cl A)) by PRE_TOPC: 18, TOPS_1: 19;

      then ( Int A) = ( Int ( Cl A)) by A1, XBOOLE_0:def 10;

      hence thesis;

    end;

    theorem :: ISOMICHI:9

    

     Th9: A is subcondensed iff A c= ( Cl ( Int A))

    proof

      thus A is subcondensed implies A c= ( Cl ( Int A)) by PRE_TOPC: 18;

      assume A c= ( Cl ( Int A));

      then

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

      ( Cl ( Int A)) c= ( Cl A) by PRE_TOPC: 19, TOPS_1: 16;

      then ( Cl ( Int A)) = ( Cl A) by A1, XBOOLE_0:def 10;

      hence thesis;

    end;

    registration

      let T be TopSpace;

      cluster subcondensed -> semi-open for Subset of T;

      coherence by Th9, DECOMP_1:def 2;

      cluster semi-open -> subcondensed for Subset of T;

      coherence by DECOMP_1:def 2, Th9;

    end

    theorem :: ISOMICHI:10

    

     Th10: A is condensed iff ( Int ( Cl A)) c= A & A c= ( Cl ( Int A))

    proof

      thus A is condensed implies ( Int ( Cl A)) c= A & A c= ( Cl ( Int A)) by Th8, Th9;

      assume that

       A1: ( Int ( Cl A)) c= A and

       A2: A c= ( Cl ( Int A));

      

       A3: A is subcondensed by A2, Th9;

      A is supercondensed by A1, Th8;

      hence thesis by A3;

    end;

    begin

    notation

      let T be TopStruct, A be Subset of T;

      synonym A is regular_open for A is open_condensed;

    end

    notation

      let T be TopStruct, A be Subset of T;

      synonym A is regular_closed for A is closed_condensed;

    end

    theorem :: ISOMICHI:11

    for T be TopSpace holds ( [#] T) is regular_open & ( [#] T) is regular_closed

    proof

      let T be TopSpace;

      

       A1: ( Int ( [#] T)) = ( [#] T) by TOPS_1: 15;

      ( Cl ( [#] T)) = ( [#] T) by TOPS_1: 2;

      hence thesis by A1, TOPS_1:def 7, TOPS_1:def 8;

    end;

    registration

      let T be TopSpace;

      cluster ( [#] T) -> regular_open regular_closed;

      coherence

      proof

        

         A1: ( Int ( [#] T)) = ( [#] T) by TOPS_1: 15;

        ( Cl ( [#] T)) = ( [#] T) by TOPS_1: 2;

        hence thesis by A1, TOPS_1:def 7, TOPS_1:def 8;

      end;

    end

    registration

      let T be TopSpace;

      cluster empty -> regular_open regular_closed for Subset of T;

      coherence

      proof

        let S be Subset of T;

        assume

         A1: S is empty;

        then

         A2: S = ( Int S);

        S = ( Cl S) by A1, PCOMPS_1: 2;

        hence thesis by A2, TOPS_1:def 7, TOPS_1:def 8;

      end;

    end

    theorem :: ISOMICHI:12

    ( Int ( Cl ( {} T))) = ( {} T)

    proof

      ( Int ( Cl ( {} T))) = ( Int ( {} T)) by PCOMPS_1: 2

      .= ( {} T);

      hence thesis;

    end;

    theorem :: ISOMICHI:13

    

     Th13: A is regular_open implies (A ` ) is regular_closed

    proof

      assume A is regular_open;

      then ( Int ( Cl A)) = A by TOPS_1:def 8;

      then ( Cl (( Cl A) ` )) = (A ` ) by TDLAT_3: 2;

      then ( Cl ( Int (A ` ))) = (A ` ) by TDLAT_3: 3;

      hence thesis by TOPS_1:def 7;

    end;

    registration

      let T be TopSpace;

      cluster regular_open regular_closed for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    registration

      let T be TopSpace;

      let A be regular_open Subset of T;

      cluster (A ` ) -> regular_closed;

      coherence by Th13;

    end

    theorem :: ISOMICHI:14

    

     Th14: A is regular_closed implies (A ` ) is regular_open

    proof

      assume A is regular_closed;

      then ( Cl ( Int A)) = A by TOPS_1:def 7;

      then ( Int (( Int A) ` )) = (A ` ) by TDLAT_3: 3;

      then ( Int ( Cl (A ` ))) = (A ` ) by TDLAT_3: 2;

      hence thesis by TOPS_1:def 8;

    end;

    registration

      let T be TopSpace;

      let A be regular_closed Subset of T;

      cluster (A ` ) -> regular_open;

      coherence by Th14;

    end

    registration

      let T be TopSpace;

      cluster regular_open -> open for Subset of T;

      coherence by TOPS_1: 67;

      cluster regular_closed -> closed for Subset of T;

      coherence by TOPS_1: 66;

    end

    theorem :: ISOMICHI:15

    

     Th15: ( Int ( Cl A)) is regular_open & ( Cl ( Int A)) is regular_closed

    proof

      

       A1: ( Cl ( Int ( Cl ( Int A)))) = ( Cl ( Int A)) by TOPS_1: 26;

      ( Int ( Cl ( Int ( Cl A)))) = ( Int ( Cl A)) by TDLAT_1: 5;

      hence thesis by A1, TOPS_1:def 7, TOPS_1:def 8;

    end;

    registration

      let T be TopSpace, A be Subset of T;

      cluster ( Int ( Cl A)) -> regular_open;

      coherence by Th15;

      cluster ( Cl ( Int A)) -> regular_closed;

      coherence by Th15;

    end

    theorem :: ISOMICHI:16

    A is regular_open iff A is supercondensed & A is open

    proof

      thus A is regular_open implies A is supercondensed & A is open

      proof

        assume A is regular_open;

        then

         A1: ( Int ( Cl A)) = A by TOPS_1:def 8;

        thus thesis by A1;

      end;

      assume that

       A2: A is supercondensed and

       A3: A is open;

      ( Int ( Cl A)) = ( Int A) by A2;

      hence thesis by A3, TOPS_1: 23;

    end;

    theorem :: ISOMICHI:17

    A is regular_closed iff A is subcondensed & A is closed

    proof

      thus A is regular_closed implies A is subcondensed & A is closed

      proof

        assume A is regular_closed;

        then

         A1: ( Cl ( Int A)) = A by TOPS_1:def 7;

        thus thesis by A1;

      end;

      assume that

       A2: A is subcondensed and

       A3: A is closed;

      ( Cl ( Int A)) = ( Cl A) by A2;

      hence thesis by A3, PRE_TOPC: 22;

    end;

    registration

      let T be TopSpace;

      cluster regular_open -> condensed open for Subset of T;

      coherence by TOPS_1: 67;

      cluster condensed open -> regular_open for Subset of T;

      coherence by TOPS_1: 67;

      cluster regular_closed -> condensed closed for Subset of T;

      coherence by TOPS_1: 66;

      cluster condensed closed -> regular_closed for Subset of T;

      coherence by TOPS_1: 66;

    end

    theorem :: ISOMICHI:18

    A is condensed iff ex B st B is regular_open & B c= A & A c= ( Cl B)

    proof

      thus A is condensed implies ex B st B is regular_open & B c= A & A c= ( Cl B)

      proof

        assume

         A1: A is condensed;

        then

         A2: ( Cl ( Int A)) = ( Cl A);

        take ( Int ( Cl A));

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

        hence thesis by A2, PRE_TOPC: 18, TOPS_1: 16;

      end;

      given B such that

       A3: B is regular_open and

       A4: B c= A and

       A5: A c= ( Cl B);

      

       A6: ( Int ( Cl B)) = B by A3, TOPS_1:def 8;

      ( Int B) c= ( Int A) by A4, TOPS_1: 19;

      then

       A7: ( Cl ( Int B)) c= ( Cl ( Int A)) by PRE_TOPC: 19;

      

       A8: ( Cl ( Int B)) = ( Cl B) by A3, Def2;

      ( Int A) c= ( Int ( Cl B)) by A5, TOPS_1: 19;

      then ( Cl ( Int A)) c= ( Cl B) by A6, PRE_TOPC: 19;

      then

       A9: ( Cl B) = ( Cl ( Int A)) by A7, A8, XBOOLE_0:def 10;

      ( Cl B) c= ( Cl A) by A4, PRE_TOPC: 19;

      then

       A10: ( Int ( Cl B)) c= ( Int ( Cl A)) by TOPS_1: 19;

      ( Cl A) c= ( Cl ( Cl B)) by A5, PRE_TOPC: 19;

      then ( Int ( Cl A)) c= ( Int ( Cl ( Cl B))) by TOPS_1: 19;

      then B = ( Int ( Cl A)) by A6, A10, XBOOLE_0:def 10;

      hence thesis by A4, A5, A9, Th10;

    end;

    theorem :: ISOMICHI:19

    A is condensed iff ex B st B is regular_closed & ( Int B) c= A & A c= B

    proof

      thus A is condensed implies ex B st B is regular_closed & ( Int B) c= A & A c= B

      proof

        assume

         A1: A is condensed;

        then

         A2: ( Cl ( Int A)) = ( Cl A);

        take ( Cl ( Int A));

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

        hence thesis by A2, PRE_TOPC: 18, TOPS_1: 16;

      end;

      given B such that

       A3: B is regular_closed and

       A4: ( Int B) c= A and

       A5: A c= B;

      

       A6: ( Cl ( Int B)) = B by A3, TOPS_1:def 7;

      ( Cl A) c= ( Cl B) by A5, PRE_TOPC: 19;

      then ( Int ( Cl A)) c= ( Int ( Cl B)) by TOPS_1: 19;

      then

       A7: ( Int ( Cl A)) c= ( Int B) by A3, Def1;

      ( Cl ( Int B)) c= ( Cl A) by A4, PRE_TOPC: 19;

      then ( Int B) c= ( Int ( Cl A)) by A6, TOPS_1: 19;

      then

       A8: ( Int B) = ( Int ( Cl A)) by A7, XBOOLE_0:def 10;

      ( Int A) c= ( Int B) by A5, TOPS_1: 19;

      then

       A9: ( Cl ( Int A)) c= ( Cl ( Int B)) by PRE_TOPC: 19;

      ( Int ( Int B)) c= ( Int A) by A4, TOPS_1: 19;

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

      then ( Cl ( Int A)) = B by A6, A9, XBOOLE_0:def 10;

      hence thesis by A4, A5, A8, Th10;

    end;

    begin

    definition

      let T be TopStruct, A be Subset of T;

      :: original: Fr

      redefine

      :: ISOMICHI:def4

      func Fr A equals (( Cl A) \ ( Int A));

      compatibility by TOPGEN_1: 8;

    end

    theorem :: ISOMICHI:20

    A is condensed iff ( Fr A) = (( Cl ( Int A)) \ ( Int ( Cl A))) & ( Fr A) = (( Cl ( Int A)) /\ ( Cl ( Int (A ` ))))

    proof

      

       A1: A c= ( Cl A) by PRE_TOPC: 18;

      (( Cl ( Int A)) /\ ( Cl ( Int (A ` )))) c= ( Cl ( Int A)) by XBOOLE_1: 17;

      then

       A2: (( Int A) \/ (( Cl ( Int A)) /\ ( Cl ( Int (A ` ))))) c= (( Int A) \/ ( Cl ( Int A))) by XBOOLE_1: 13;

      thus A is condensed implies ( Fr A) = (( Cl ( Int A)) \ ( Int ( Cl A))) & ( Fr A) = (( Cl ( Int A)) /\ ( Cl ( Int (A ` ))))

      proof

        assume

         A3: A is condensed;

        then (A ` ) is condensed by TDLAT_1: 16;

        then

         A4: ( Cl ( Int (A ` ))) = ( Cl (A ` ));

        thus thesis by A3, A4, TOPS_1:def 2;

      end;

      assume that ( Fr A) = (( Cl ( Int A)) \ ( Int ( Cl A))) and

       A5: ( Fr A) = (( Cl ( Int A)) /\ ( Cl ( Int (A ` ))));

      

       A6: (( Cl A) \/ ( Int A)) = (( Int A) \/ ( Fr A)) by XBOOLE_1: 39;

      ( Int A) c= A by TOPS_1: 16;

      then ( Cl A) = (( Int A) \/ (( Cl ( Int A)) /\ ( Cl ( Int (A ` ))))) by A5, A1, A6, XBOOLE_1: 1, XBOOLE_1: 12;

      then

       A7: ( Cl A) c= ( Cl ( Int A)) by A2, PRE_TOPC: 18, XBOOLE_1: 12;

      ( Cl ( Int A)) c= ( Cl A) by PRE_TOPC: 19, TOPS_1: 16;

      then ( Cl ( Int A)) = ( Cl A) by A7, XBOOLE_0:def 10;

      then

       A8: A is subcondensed;

      

       A9: (A ` ) c= ( Cl (A ` )) by PRE_TOPC: 18;

      

       A10: (( Cl (A ` )) \/ ( Int (A ` ))) = (( Int (A ` )) \/ ( Fr (A ` ))) by XBOOLE_1: 39;

      

       A11: ( Fr A) = ( Fr (A ` )) by TOPS_1: 29;

      (( Cl ( Int (A ` ))) /\ ( Cl ( Int ((A ` ) ` )))) c= ( Cl ( Int (A ` ))) by XBOOLE_1: 17;

      then

       A12: (( Int (A ` )) \/ (( Cl ( Int (A ` ))) /\ ( Cl ( Int ((A ` ) ` ))))) c= (( Int (A ` )) \/ ( Cl ( Int (A ` )))) by XBOOLE_1: 13;

      

       A13: ( Cl ( Int (A ` ))) c= ( Cl (A ` )) by PRE_TOPC: 19, TOPS_1: 16;

      

       A14: ( Cl ( Int (A ` ))) = ( Cl (( Cl A) ` )) by TDLAT_3: 3

      .= (( Int ( Cl A)) ` ) by TDLAT_3: 2;

      

       A15: (( Int (A ` )) \/ ( Cl ( Int (A ` )))) = ( Cl ( Int (A ` ))) by PRE_TOPC: 18, XBOOLE_1: 12;

      ( Int (A ` )) c= (A ` ) by TOPS_1: 16;

      then ( Cl (A ` )) = (( Int (A ` )) \/ (( Cl ( Int (A ` ))) /\ ( Cl ( Int ((A ` ) ` ))))) by A5, A9, A11, A10, XBOOLE_1: 1, XBOOLE_1: 12;

      then

       A16: ( Cl (A ` )) = ( Cl ( Int (A ` ))) by A13, A12, A15, XBOOLE_0:def 10;

      ( Cl (A ` )) = (( Int A) ` ) by TDLAT_3: 2;

      then ( Int A) = ((( Int ( Cl A)) ` ) ` ) by A16, A14;

      then A is supercondensed;

      hence thesis by A8;

    end;

    definition

      let T be TopStruct, A be Subset of T;

      :: ISOMICHI:def5

      func Border A -> Subset of T equals ( Int ( Fr A));

      coherence ;

    end

    theorem :: ISOMICHI:21

    

     Th21: ( Border A) is regular_open & ( Border A) = (( Int ( Cl A)) \ ( Cl ( Int A))) & ( Border A) = (( Int ( Cl A)) /\ ( Int ( Cl (A ` ))))

    proof

      ( Fr A) = ( Cl ( Fr A)) by PRE_TOPC: 22;

      hence ( Border A) is regular_open;

      (( Int ( Cl A)) \ ( Cl ( Int A))) = (( Int ( Cl A)) \ ((( Cl ( Int A)) ` ) ` ))

      .= (( Int ( Cl A)) \ (( Int (( Int A) ` )) ` )) by TDLAT_3: 3

      .= (( Int ( Cl A)) \ (( Int ( Cl (A ` ))) ` )) by TDLAT_3: 2

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

      .= ( Int (( Cl A) /\ ( Cl (A ` )))) by TOPS_1: 17

      .= ( Int ( Fr A)) by TOPS_1:def 2;

      hence ( Border A) = (( Int ( Cl A)) \ ( Cl ( Int A)));

      (( Int ( Cl A)) /\ ( Int ( Cl (A ` )))) = ( Int (( Cl A) /\ ( Cl (A ` )))) by TOPS_1: 17

      .= ( Int ( Fr A)) by TOPS_1:def 2;

      hence thesis;

    end;

    registration

      let T be TopSpace, A be Subset of T;

      cluster ( Border A) -> regular_open;

      coherence by Th21;

    end

    theorem :: ISOMICHI:22

    

     Th22: A is supercondensed iff ( Int A) is regular_open & ( Border A) is empty

    proof

      

       A1: ( Int A) c= ( Int ( Cl A)) by PRE_TOPC: 18, TOPS_1: 19;

      thus A is supercondensed implies ( Int A) is regular_open & ( Border A) is empty

      proof

        assume

         A2: A is supercondensed;

        then ( Int ( Cl A)) = ( Int A);

        then ( Int ( Cl A)) c= ( Cl ( Int A)) by PRE_TOPC: 18;

        then (( Int ( Cl A)) \ ( Cl ( Int A))) is empty by XBOOLE_1: 37;

        hence thesis by A2, Th21;

      end;

      assume that

       A3: ( Int A) is regular_open and

       A4: ( Border A) is empty;

      (( Int ( Cl A)) \ ( Cl ( Int A))) is empty by A4, Th21;

      then ( Int ( Cl A)) c= ( Cl ( Int A)) by XBOOLE_1: 37;

      then

       A5: ( Int ( Int ( Cl A))) c= ( Int ( Cl ( Int A))) by TOPS_1: 19;

      ( Int A) = ( Int ( Cl ( Int A))) by A3, TOPS_1:def 8;

      then ( Int ( Cl A)) = ( Int A) by A5, A1, XBOOLE_0:def 10;

      hence thesis;

    end;

    theorem :: ISOMICHI:23

    

     Th23: A is subcondensed iff ( Cl A) is regular_closed & ( Border A) is empty

    proof

      

       A1: ( Cl ( Int A)) c= ( Cl A) by PRE_TOPC: 19, TOPS_1: 16;

      thus A is subcondensed implies ( Cl A) is regular_closed & ( Border A) is empty

      proof

        assume

         A2: A is subcondensed;

        then ( Cl ( Int A)) = ( Cl A);

        then ( Int ( Cl A)) c= ( Cl ( Int A)) by TOPS_1: 16;

        then (( Int ( Cl A)) \ ( Cl ( Int A))) is empty by XBOOLE_1: 37;

        hence thesis by A2, Th21;

      end;

      assume that

       A3: ( Cl A) is regular_closed and

       A4: ( Border A) is empty;

      (( Int ( Cl A)) \ ( Cl ( Int A))) is empty by A4, Th21;

      then ( Int ( Cl A)) c= ( Cl ( Int A)) by XBOOLE_1: 37;

      then

       A5: ( Cl ( Int ( Cl A))) c= ( Cl ( Cl ( Int A))) by PRE_TOPC: 19;

      ( Cl A) = ( Cl ( Int ( Cl A))) by A3, TOPS_1:def 7;

      then ( Cl ( Int A)) = ( Cl A) by A5, A1, XBOOLE_0:def 10;

      hence thesis;

    end;

    registration

      let T be TopSpace, A be Subset of T;

      cluster ( Border ( Border A)) -> empty;

      coherence ;

    end

    theorem :: ISOMICHI:24

    A is condensed iff ( Int A) is regular_open & ( Cl A) is regular_closed & ( Border A) is empty

    proof

      thus A is condensed implies ( Int A) is regular_open & ( Cl A) is regular_closed & ( Border A) is empty by Th22;

      assume that

       A1: ( Int A) is regular_open and

       A2: ( Cl A) is regular_closed and

       A3: ( Border A) is empty;

      

       A4: A is subcondensed by A2, A3, Th23;

      A is supercondensed by A1, A3, Th22;

      hence thesis by A4;

    end;

    begin

    theorem :: ISOMICHI:25

    for A be Subset of R^1 , a be Real st A = ]. -infty , a.] holds ( Int A) = ]. -infty , a.[

    proof

      let A be Subset of R^1 , a be Real;

      assume A = ]. -infty , a.];

      then (A ` ) = ].a, +infty .[ by TOPMETR: 17, XXREAL_1: 224, XXREAL_1: 288;

      then ( Cl (A ` )) = [.a, +infty .[ by BORSUK_5: 49;

      then (( Cl (A ` )) ` ) = ]. -infty , a.[ by TOPMETR: 17, XXREAL_1: 224, XXREAL_1: 294;

      hence thesis by TOPS_1:def 1;

    end;

    theorem :: ISOMICHI:26

    for A be Subset of R^1 , a be Real st A = [.a, +infty .[ holds ( Int A) = ].a, +infty .[

    proof

      let A be Subset of R^1 , a be Real;

      assume A = [.a, +infty .[;

      then (A ` ) = ]. -infty , a.[ by TOPMETR: 17, XXREAL_1: 224, XXREAL_1: 294;

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

      then (( Cl (A ` )) ` ) = ].a, +infty .[ by TOPMETR: 17, XXREAL_1: 224, XXREAL_1: 288;

      hence thesis by TOPS_1:def 1;

    end;

    theorem :: ISOMICHI:27

    

     Th27: for A be Subset of R^1 , a,b be Real st A = (( ]. -infty , a.] \/ ( IRRAT (a,b))) \/ [.b, +infty .[) holds ( Cl A) = the carrier of R^1

    proof

      reconsider B = IRRAT as Subset of R^1 by TOPMETR: 17;

      let A be Subset of R^1 , a,b be Real;

      assume

       A1: A = (( ]. -infty , a.] \/ ( IRRAT (a,b))) \/ [.b, +infty .[);

      B c= A

      proof

        let x be object;

        assume

         A2: x in B;

        then

        reconsider x9 = x as Real;

        per cases ;

          suppose x9 <= a;

          then x9 in ]. -infty , a.] by XXREAL_1: 234;

          then x9 in ( ]. -infty , a.] \/ ( IRRAT (a,b))) by XBOOLE_0:def 3;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

          suppose x9 > a & x9 < b;

          then x9 in ].a, b.[ by XXREAL_1: 4;

          then x9 in ( IRRAT /\ ].a, b.[) by A2, XBOOLE_0:def 4;

          then x9 in ( IRRAT (a,b)) by BORSUK_5:def 3;

          then x9 in ( ]. -infty , a.] \/ ( IRRAT (a,b))) by XBOOLE_0:def 3;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

          suppose x9 >= b;

          then x9 in [.b, +infty .[ by XXREAL_1: 236;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

      end;

      then

       A3: ( Cl B) c= ( Cl A) by PRE_TOPC: 19;

      ( Cl B) = the carrier of R^1 by BORSUK_5: 28;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: ISOMICHI:28

    for A be Subset of R^1 , a,b be Real st A = ( RAT (a,b)) holds ( Int A) = {}

    proof

      let A be Subset of R^1 , a,b be Real;

      assume

       A1: A = ( RAT (a,b));

      (A ` ) = ( REAL \ A) by TOPMETR: 17

      .= (( ]. -infty , a.] \/ ( IRRAT (a,b))) \/ [.b, +infty .[) by A1, BORSUK_5: 58;

      then ( Cl (A ` )) = ( [#] R^1 ) by Th27;

      then (( Cl (A ` )) ` ) = ( {} R^1 ) by XBOOLE_1: 37;

      hence thesis by TOPS_1:def 1;

    end;

    theorem :: ISOMICHI:29

    for A be Subset of R^1 , a,b be Real st A = ( IRRAT (a,b)) holds ( Int A) = {}

    proof

      reconsider B = IRRAT as Subset of R^1 by TOPMETR: 17;

      let A be Subset of R^1 , a,b be Real;

      assume A = ( IRRAT (a,b));

      then A = ( IRRAT /\ ].a, b.[) by BORSUK_5:def 3;

      then A c= B by XBOOLE_1: 17;

      then A is boundary by TOPGEN_1: 54, TOPS_3: 11;

      hence thesis;

    end;

    theorem :: ISOMICHI:30

    for a,b be Real st a >= b holds ( IRRAT (a,b)) = {}

    proof

      let a,b be Real;

      assume

       A1: a >= b;

      ( IRRAT (a,b)) = ( IRRAT /\ ].a, b.[) by BORSUK_5:def 3

      .= ( IRRAT /\ {} ) by A1, XXREAL_1: 28;

      hence thesis;

    end;

    theorem :: ISOMICHI:31

    

     Th31: for a,b be Real holds ( IRRAT (a,b)) c= [.a, +infty .[

    proof

      let a,b be Real;

      let x be object;

      assume

       A1: x in ( IRRAT (a,b));

      then

      reconsider x as Real;

      a < x by A1, BORSUK_5: 30;

      hence thesis by XXREAL_1: 236;

    end;

    theorem :: ISOMICHI:32

    

     Th32: for A be Subset of R^1 , a,b,c be Real st A = ( ]. -infty , a.[ \/ ( RAT (b,c))) & a < b & b < c holds ( Int A) = ]. -infty , a.[

    proof

      let A be Subset of R^1 , a,b,c be Real;

      reconsider B = [.a, b.], C = ( IRRAT (b,c)), D = [.c, +infty .[ as Subset of R^1 by TOPMETR: 17;

      assume that

       A1: A = ( ]. -infty , a.[ \/ ( RAT (b,c))) and

       A2: a < b and

       A3: b < c;

      

       A4: a < c by A2, A3, XXREAL_0: 2;

      (A ` ) = ( REAL \ ( ]. -infty , a.[ \/ ( RAT (b,c)))) by A1, TOPMETR: 17

      .= (( REAL \ ( RAT (b,c))) \ ]. -infty , a.[) by XBOOLE_1: 41

      .= ((( ]. -infty , b.] \/ ( IRRAT (b,c))) \/ [.c, +infty .[) \ ]. -infty , a.[) by BORSUK_5: 58

      .= (( ]. -infty , b.] \/ (( IRRAT (b,c)) \/ [.c, +infty .[)) \ ]. -infty , a.[) by XBOOLE_1: 4

      .= (( ]. -infty , b.] \ ]. -infty , a.[) \/ ((( IRRAT (b,c)) \/ [.c, +infty .[) \ ]. -infty , a.[)) by XBOOLE_1: 42;

      

      then

       A5: (A ` ) = ( [.a, b.] \/ ((( IRRAT (b,c)) \/ [.c, +infty .[) \ ]. -infty , a.[)) by XXREAL_1: 289

      .= ( [.a, b.] \/ ((( IRRAT (b,c)) \ ]. -infty , a.[) \/ ( [.c, +infty .[ \ ]. -infty , a.[))) by XBOOLE_1: 42;

      ( right_closed_halfline c) is closed;

      then D is closed by JORDAN5A: 23;

      then

       A6: ( Cl D) = D by PRE_TOPC: 22;

       [.b, +infty .[ misses ]. -infty , a.[ by A2, XXREAL_1: 94;

      then ( IRRAT (b,c)) misses ]. -infty , a.[ by Th31, XBOOLE_1: 63;

      then

       A7: (( IRRAT (b,c)) \ ]. -infty , a.[) = ( IRRAT (b,c)) by XBOOLE_1: 83;

      B is closed by JORDAN5A: 23;

      then

       A8: ( Cl B) = B by PRE_TOPC: 22;

       [.c, +infty .[ misses ]. -infty , a.[ by A2, A3, XXREAL_0: 2, XXREAL_1: 94;

      

      then (A ` ) = ( [.a, b.] \/ (( IRRAT (b,c)) \/ [.c, +infty .[)) by A5, A7, XBOOLE_1: 83

      .= ( [.a, b.] \/ (( IRRAT (b,c)) \/ ( {c} \/ ].c, +infty .[))) by BORSUK_5: 43

      .= (( [.a, b.] \/ ( IRRAT (b,c))) \/ ( {c} \/ ].c, +infty .[)) by XBOOLE_1: 4

      .= (( [.a, b.] \/ ( IRRAT (b,c))) \/ [.c, +infty .[) by BORSUK_5: 43;

      

      then ( Cl (A ` )) = (( Cl (B \/ C)) \/ ( Cl D)) by PRE_TOPC: 20

      .= ((( Cl B) \/ ( Cl C)) \/ ( Cl D)) by PRE_TOPC: 20

      .= ((B \/ [.b, c.]) \/ D) by A8, A6, A3, BORSUK_5: 32

      .= ( [.a, c.] \/ D) by A2, A3, XXREAL_1: 165

      .= [.a, +infty .[ by A4, BORSUK_5: 11;

      then (( Cl (A ` )) ` ) = ]. -infty , a.[ by TOPMETR: 17, XXREAL_1: 224, XXREAL_1: 294;

      hence thesis by TOPS_1:def 1;

    end;

    

     Lm1: for a,b be Real st a < b holds ( [.a, b.] \/ {b}) = [.a, b.]

    proof

      let a,b be Real;

      assume

       A1: a < b;

      

      then [.a, b.] = ( [.a, b.[ \/ {b}) by XXREAL_1: 129

      .= (( [.a, b.[ \/ {b}) \/ {b}) by XBOOLE_1: 6;

      hence thesis by A1, XXREAL_1: 129;

    end;

    theorem :: ISOMICHI:33

    for a,b be Real st a < b holds REAL = (( ]. -infty , a.[ \/ [.a, b.]) \/ ].b, +infty .[)

    proof

      let a,b be Real;

      assume

       A1: a < b;

       REAL = (( REAL \ {a}) \/ {a}) by XBOOLE_1: 45

      .= (( ]. -infty , a.[ \/ ].a, +infty .[) \/ {a}) by XXREAL_1: 389

      .= ( ]. -infty , a.[ \/ ( ].a, +infty .[ \/ {a})) by XBOOLE_1: 4

      .= ( ]. -infty , a.[ \/ [.a, +infty .[) by BORSUK_5: 43

      .= ( ]. -infty , a.[ \/ ( [.a, b.] \/ [.b, +infty .[)) by A1, BORSUK_5: 11

      .= ( ]. -infty , a.[ \/ ( [.a, b.] \/ ( {b} \/ ].b, +infty .[))) by BORSUK_5: 43

      .= ( ]. -infty , a.[ \/ (( [.a, b.] \/ {b}) \/ ].b, +infty .[)) by XBOOLE_1: 4

      .= (( ]. -infty , a.[ \/ ( [.a, b.] \/ {b})) \/ ].b, +infty .[) by XBOOLE_1: 4;

      hence thesis by A1, Lm1;

    end;

    theorem :: ISOMICHI:34

    

     Th34: for A be Subset of R^1 , a,b,c be Real st A = ( ]. -infty , a.] \/ [.b, c.]) & a < b & b < c holds ( Int A) = ( ]. -infty , a.[ \/ ].b, c.[)

    proof

      let A be Subset of R^1 , a,b,c be Real;

      assume that

       A1: A = ( ]. -infty , a.] \/ [.b, c.]) and

       A2: a < b and

       A3: b < c;

      a < c by A2, A3, XXREAL_0: 2;

      then

       A4: ( ].c, +infty .[ /\ ].a, +infty .[) = ].c, +infty .[ by XBOOLE_1: 28, XXREAL_1: 46;

      reconsider B = ].a, b.[, C = ].c, +infty .[ as Subset of R^1 by TOPMETR: 17;

      

       A5: ( Cl B) = [.a, b.] by A2, BORSUK_5: 16;

      

       A6: ( Cl C) = [.c, +infty .[ by BORSUK_5: 49;

      (A ` ) = ( REAL \ ( ]. -infty , a.] \/ [.b, c.])) by A1, TOPMETR: 17

      .= (( REAL \ ( left_closed_halfline a)) \ [.b, c.]) by XBOOLE_1: 41

      .= (( right_open_halfline a) \ [.b, c.]) by XXREAL_1: 224, XXREAL_1: 288

      .= ( ].a, +infty .[ \ ( [.b, +infty .[ \ ].c, +infty .[)) by XXREAL_1: 295

      .= (( ].a, +infty .[ \ [.b, +infty .[) \/ ( ].a, +infty .[ /\ ].c, +infty .[)) by XBOOLE_1: 52

      .= ( ].a, b.[ \/ ].c, +infty .[) by A4, XXREAL_1: 294;

      

      then (( Cl (A ` )) ` ) = ( REAL \ ( [.c, +infty .[ \/ [.a, b.])) by A5, A6, PRE_TOPC: 20, TOPMETR: 17

      .= (( REAL \ ( right_closed_halfline c)) \ [.a, b.]) by XBOOLE_1: 41

      .= (( left_open_halfline c) \ [.a, b.]) by XXREAL_1: 224, XXREAL_1: 294

      .= ( ]. -infty , a.[ \/ ].b, c.[) by A2, A3, XXREAL_0: 2, XXREAL_1: 339;

      hence thesis by TOPS_1:def 1;

    end;

    begin

    notation

      let A,B be set;

      antonym A,B are_c=-incomparable for A,B are_c=-comparable ;

    end

    theorem :: ISOMICHI:35

    

     Th35: for A,B be set holds (A,B) are_c=-incomparable or A c= B or B c< A

    proof

      let A,B be set;

      assume that

       A1: (A,B) are_c=-comparable and

       A2: not A c= B and

       A3: not B c< A;

      A c= B or B c= A by A1, XBOOLE_0:def 9;

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

    end;

    definition

      let T, A;

      :: ISOMICHI:def6

      attr A is 1st_class means ( Int ( Cl A)) c= ( Cl ( Int A));

      :: ISOMICHI:def7

      attr A is 2nd_class means ( Cl ( Int A)) c< ( Int ( Cl A));

      :: ISOMICHI:def8

      attr A is 3rd_class means (( Cl ( Int A)),( Int ( Cl A))) are_c=-incomparable ;

    end

    theorem :: ISOMICHI:36

    A is 1st_class or A is 2nd_class or A is 3rd_class by Th35;

    registration

      let T be TopSpace;

      cluster 1st_class -> non 2nd_class non 3rd_class for Subset of T;

      coherence by XBOOLE_0:def 9, XBOOLE_1: 60;

      cluster 2nd_class -> non 1st_class non 3rd_class for Subset of T;

      coherence

      proof

        let A be Subset of T;

        assume A is 2nd_class;

        then

         A1: ( Cl ( Int A)) c< ( Int ( Cl A));

        then ( Cl ( Int A)) c= ( Int ( Cl A)) by XBOOLE_0:def 8;

        then

         A2: (( Cl ( Int A)),( Int ( Cl A))) are_c=-comparable by XBOOLE_0:def 9;

         not ( Int ( Cl A)) c= ( Cl ( Int A)) by A1, XBOOLE_0:def 8;

        hence thesis by A2;

      end;

      cluster 3rd_class -> non 1st_class non 2nd_class for Subset of T;

      coherence ;

    end

    theorem :: ISOMICHI:37

    

     Th37: A is 1st_class iff ( Border A) is empty

    proof

      

       A1: ( Border A) is empty implies A is 1st_class

      proof

        assume ( Border A) is empty;

        then (( Int ( Cl A)) \ ( Cl ( Int A))) = {} by Th21;

        then ( Int ( Cl A)) c= ( Cl ( Int A)) by XBOOLE_1: 37;

        hence thesis;

      end;

      A is 1st_class implies ( Border A) is empty

      proof

        assume A is 1st_class;

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

        then (( Int ( Cl A)) \ ( Cl ( Int A))) = {} by XBOOLE_1: 37;

        hence thesis by Th21;

      end;

      hence thesis by A1;

    end;

    registration

      let T be TopSpace;

      cluster supercondensed -> 1st_class for Subset of T;

      coherence

      proof

        let A be Subset of T;

        assume A is supercondensed;

        then ( Border A) is empty by Th22;

        hence thesis by Th37;

      end;

      cluster subcondensed -> 1st_class for Subset of T;

      coherence

      proof

        let A be Subset of T;

        assume A is subcondensed;

        then ( Border A) is empty by Th23;

        hence thesis by Th37;

      end;

    end

    definition

      let T be TopSpace;

      :: ISOMICHI:def9

      attr T is with_1st_class_subsets means ex A be Subset of T st A is 1st_class;

      :: ISOMICHI:def10

      attr T is with_2nd_class_subsets means

      : Def10: ex A be Subset of T st A is 2nd_class;

      :: ISOMICHI:def11

      attr T is with_3rd_class_subsets means

      : Def11: ex A be Subset of T st A is 3rd_class;

    end

    registration

      let T be anti-discrete non empty TopSpace;

      cluster proper non empty -> 2nd_class for Subset of T;

      coherence

      proof

        let A be Subset of T;

        assume

         A1: A is proper non empty;

        then A <> the carrier of T;

        then ( Int A) = {} by TEX_1: 10;

        then

         A2: ( Cl ( Int A)) = {} by TEX_1: 9;

        ( Cl A) = the carrier of T by A1, TEX_1: 9;

        then ( Int ( Cl A)) = the carrier of T by TEX_1: 10;

        then ( Cl ( Int A)) c< ( Int ( Cl A)) by A2, XBOOLE_0:def 8;

        hence thesis;

      end;

    end

    registration

      let T be anti-discrete non trivial strict TopSpace;

      cluster 2nd_class for Subset of T;

      existence

      proof

        set x = the Element of T;

        reconsider A = {x} as Subset of T;

        ( Cl A) = the carrier of T by TEX_1: 9;

        hence thesis;

      end;

    end

    registration

      cluster with_1st_class_subsets with_2nd_class_subsets strict non trivial for TopSpace;

      existence

      proof

        set T = the anti-discrete non trivial strict TopSpace;

        set B = the 2nd_class Subset of T;

        B is 2nd_class;

        then

         A1: T is with_2nd_class_subsets;

        ( {} T) is 1st_class;

        then T is with_1st_class_subsets;

        hence thesis by A1;

      end;

      cluster with_3rd_class_subsets non empty strict for TopSpace;

      existence

      proof

        set B = ]. -infty , 1.[, C = ( RAT (2,4));

        take R^1 ;

        set A = (B \/ C);

        reconsider A, B, C as Subset of R^1 by TOPMETR: 17;

        

         A2: ( Cl C) = [.2, 4.] by BORSUK_5: 31;

        ( Cl B) = ]. -infty , 1.] by BORSUK_5: 51;

        then ( Cl A) = ( ]. -infty , 1.] \/ [.2, 4.]) by A2, PRE_TOPC: 20;

        then

         A3: ( Int ( Cl A)) = ( ]. -infty , 1.[ \/ ].2, 4.[) by Th34;

        

         A4: ( Cl ( Int A)) = ]. -infty , 1.] by Th32, BORSUK_5: 51;

        3 in ].2, 4.[ by XXREAL_1: 4;

        then 3 in ( Int ( Cl A)) by A3, XBOOLE_0:def 3;

        then

         A5: not ( Int ( Cl A)) c= ( Cl ( Int A)) by A4, XXREAL_1: 234;

        

         A6: not 1 in ].2, 4.[ by XXREAL_1: 4;

        

         A7: not 1 in ]. -infty , 1.[ by XXREAL_1: 4;

        1 in ( Cl ( Int A)) by A4, XXREAL_1: 234;

        then not ( Cl ( Int A)) c= ( Int ( Cl A)) by A3, A7, A6, XBOOLE_0:def 3;

        then (( Int ( Cl A)),( Cl ( Int A))) are_c=-incomparable by A5, XBOOLE_0:def 9;

        then A is 3rd_class;

        hence thesis;

      end;

    end

    registration

      let T;

      cluster 1st_class for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    registration

      let T be with_2nd_class_subsets TopSpace;

      cluster 2nd_class for Subset of T;

      existence by Def10;

    end

    registration

      let T be with_3rd_class_subsets TopSpace;

      cluster 3rd_class for Subset of T;

      existence by Def11;

    end

    theorem :: ISOMICHI:38

    

     Th38: A is 1st_class iff (A ` ) is 1st_class

    proof

      

       A1: (A ` ) is 1st_class implies A is 1st_class

      proof

        assume (A ` ) is 1st_class;

        then ( Int ( Cl (A ` ))) c= ( Cl ( Int (A ` )));

        then ( Int (( Int A) ` )) c= ( Cl ( Int (A ` ))) by TDLAT_3: 2;

        then (( Cl ( Int A)) ` ) c= ( Cl ( Int (A ` ))) by TDLAT_3: 3;

        then (( Cl ( Int A)) ` ) c= ( Cl (( Cl A) ` )) by TDLAT_3: 3;

        then (( Cl ( Int A)) ` ) c= (( Int ( Cl A)) ` ) by TDLAT_3: 2;

        then ( Int ( Cl A)) c= ( Cl ( Int A)) by SUBSET_1: 12;

        hence thesis;

      end;

      A is 1st_class implies (A ` ) is 1st_class

      proof

        assume A is 1st_class;

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

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

        then ( Int (( Int A) ` )) c= (( Int ( Cl A)) ` ) by TDLAT_3: 3;

        then ( Int (( Int A) ` )) c= ( Cl (( Cl A) ` )) by TDLAT_3: 2;

        then ( Int (( Int A) ` )) c= ( Cl ( Int (A ` ))) by TDLAT_3: 3;

        then ( Int ( Cl (A ` ))) c= ( Cl ( Int (A ` ))) by TDLAT_3: 2;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: ISOMICHI:39

    

     Th39: A is 2nd_class iff (A ` ) is 2nd_class

    proof

      

       A1: for A be Subset of T st (A ` ) is 2nd_class holds A is 2nd_class

      proof

        let A be Subset of T;

        assume (A ` ) is 2nd_class;

        then

         A2: ( Cl ( Int (A ` ))) c< ( Int ( Cl (A ` )));

        then ( Cl ( Int (A ` ))) c= ( Int ( Cl (A ` ))) by XBOOLE_0:def 8;

        then ( Cl ( Int (A ` ))) c= ( Int (( Int A) ` )) by TDLAT_3: 2;

        then ( Cl ( Int (A ` ))) c= (( Cl ( Int A)) ` ) by TDLAT_3: 3;

        then ( Cl (( Cl A) ` )) c= (( Cl ( Int A)) ` ) by TDLAT_3: 3;

        then (( Int ( Cl A)) ` ) c= (( Cl ( Int A)) ` ) by TDLAT_3: 2;

        then

         A3: ( Cl ( Int A)) c= ( Int ( Cl A)) by SUBSET_1: 12;

        ( Cl (( Cl A) ` )) <> ( Int ( Cl (A ` ))) by A2, TDLAT_3: 3;

        then ( Cl (( Cl A) ` )) <> ( Int (( Int A) ` )) by TDLAT_3: 2;

        then (( Cl ( Int A)) ` ) <> ( Cl (( Cl A) ` )) by TDLAT_3: 3;

        then ( Cl ( Int A)) <> ( Int ( Cl A)) by TDLAT_3: 2;

        then ( Cl ( Int A)) c< ( Int ( Cl A)) by A3, XBOOLE_0:def 8;

        hence thesis;

      end;

      A is 2nd_class implies (A ` ) is 2nd_class

      proof

        assume A is 2nd_class;

        then ((A ` ) ` ) is 2nd_class;

        hence thesis by A1;

      end;

      hence thesis by A1;

    end;

    theorem :: ISOMICHI:40

    

     Th40: A is 3rd_class iff (A ` ) is 3rd_class

    proof

      (( Int ( Cl A)) ` ) = ( Cl (( Cl A) ` )) by TDLAT_3: 2

      .= ( Cl ( Int (A ` ))) by TDLAT_3: 3;

      then

       A1: ( Int ( Cl A)) = (( Cl ( Int (A ` ))) ` );

      (( Cl ( Int A)) ` ) = ( Int (( Int A) ` )) by TDLAT_3: 3

      .= ( Int ( Cl (A ` ))) by TDLAT_3: 2;

      then

       A2: ( Cl ( Int A)) = (( Int ( Cl (A ` ))) ` );

      

       A3: (A ` ) is 3rd_class implies A is 3rd_class

      proof

        assume (A ` ) is 3rd_class;

        then

         A4: (( Cl ( Int (A ` ))),( Int ( Cl (A ` )))) are_c=-incomparable ;

        then not ( Int ( Cl (A ` ))) c= ( Cl ( Int (A ` ))) by XBOOLE_0:def 9;

        then

         A5: not ( Int ( Cl A)) c= ( Cl ( Int A)) by A2, A1, SUBSET_1: 12;

         not ( Cl ( Int (A ` ))) c= ( Int ( Cl (A ` ))) by A4, XBOOLE_0:def 9;

        then not ( Cl ( Int A)) c= ( Int ( Cl A)) by A2, A1, SUBSET_1: 12;

        then (( Cl ( Int A)),( Int ( Cl A))) are_c=-incomparable by A5, XBOOLE_0:def 9;

        hence thesis;

      end;

      A is 3rd_class implies (A ` ) is 3rd_class

      proof

        assume A is 3rd_class;

        then

         A6: (( Cl ( Int A)),( Int ( Cl A))) are_c=-incomparable ;

        then not ( Int ( Cl A)) c= ( Cl ( Int A)) by XBOOLE_0:def 9;

        then

         A7: not ( Int ( Cl (A ` ))) c= ( Cl ( Int (A ` ))) by A2, A1, SUBSET_1: 12;

         not ( Cl ( Int A)) c= ( Int ( Cl A)) by A6, XBOOLE_0:def 9;

        then not ( Cl ( Int (A ` ))) c= ( Int ( Cl (A ` ))) by A2, A1, SUBSET_1: 12;

        then (( Cl ( Int (A ` ))),( Int ( Cl (A ` )))) are_c=-incomparable by A7, XBOOLE_0:def 9;

        hence thesis;

      end;

      hence thesis by A3;

    end;

    registration

      let T;

      let A be 1st_class Subset of T;

      cluster (A ` ) -> 1st_class;

      coherence by Th38;

    end

    registration

      let T be with_2nd_class_subsets TopSpace;

      let A be 2nd_class Subset of T;

      cluster (A ` ) -> 2nd_class;

      coherence by Th39;

    end

    registration

      let T be with_3rd_class_subsets TopSpace;

      let A be 3rd_class Subset of T;

      cluster (A ` ) -> 3rd_class;

      coherence by Th40;

    end

    theorem :: ISOMICHI:41

    

     Th41: A is 1st_class implies ( Int ( Cl A)) = ( Int ( Cl ( Int A))) & ( Cl ( Int A)) = ( Cl ( Int ( Cl A)))

    proof

      ( Cl ( Int A)) c= ( Cl A) by PRE_TOPC: 19, TOPS_1: 16;

      then

       A1: ( Int ( Cl ( Int A))) c= ( Int ( Cl A)) by TOPS_1: 19;

      ( Int A) c= ( Int ( Cl A)) by PRE_TOPC: 18, TOPS_1: 19;

      then

       A2: ( Cl ( Int A)) c= ( Cl ( Int ( Cl A))) by PRE_TOPC: 19;

      assume A is 1st_class;

      then

       A3: ( Int ( Cl A)) c= ( Cl ( Int A));

      then

       A4: ( Cl ( Int ( Cl A))) c= ( Cl ( Cl ( Int A))) by PRE_TOPC: 19;

      ( Int ( Int ( Cl A))) c= ( Int ( Cl ( Int A))) by A3, TOPS_1: 19;

      hence thesis by A1, A4, A2, XBOOLE_0:def 10;

    end;

    theorem :: ISOMICHI:42

    

     Th42: (( Int ( Cl A)) = ( Int ( Cl ( Int A))) or ( Cl ( Int A)) = ( Cl ( Int ( Cl A)))) implies A is 1st_class

    proof

      assume

       A1: ( Int ( Cl A)) = ( Int ( Cl ( Int A))) or ( Cl ( Int A)) = ( Cl ( Int ( Cl A)));

      per cases by A1;

        suppose

         A2: ( Int ( Cl A)) = ( Int ( Cl ( Int A)));

        ( Int ( Cl ( Int A))) c= ( Cl ( Int A)) by TOPS_1: 16;

        hence thesis by A2;

      end;

        suppose

         A3: ( Cl ( Int A)) = ( Cl ( Int ( Cl A)));

        ( Int ( Cl A)) c= ( Cl ( Int ( Cl A))) by PRE_TOPC: 18;

        hence thesis by A3;

      end;

    end;

    theorem :: ISOMICHI:43

    

     Th43: A is 1st_class & B is 1st_class implies (( Int ( Cl A)) /\ ( Int ( Cl B))) = ( Int ( Cl (A /\ B))) & (( Cl ( Int A)) \/ ( Cl ( Int B))) = ( Cl ( Int (A \/ B)))

    proof

      assume that

       A1: A is 1st_class and

       A2: B is 1st_class;

      

       A3: ( Cl ( Int B)) = ( Cl ( Int ( Cl B))) by A2, Th41;

      ( Cl ( Int A)) = ( Cl ( Int ( Cl A))) by A1, Th41;

      then

       A4: (( Cl ( Int A)) \/ ( Cl ( Int B))) = ( Cl ( Int ( Cl (A \/ B)))) by A3, Th2;

      ( Int ( Cl (A /\ B))) c= ( Int (( Cl A) /\ ( Cl B))) by PRE_TOPC: 21, TOPS_1: 19;

      then

       A5: ( Int ( Cl (A /\ B))) c= (( Int ( Cl A)) /\ ( Int ( Cl B))) by TOPS_1: 17;

      ( Int (A \/ B)) c= ( Int ( Cl (A \/ B))) by PRE_TOPC: 18, TOPS_1: 19;

      then

       A6: ( Cl ( Int (A \/ B))) c= ( Cl ( Int ( Cl (A \/ B)))) by PRE_TOPC: 19;

      ( Cl (( Int A) \/ ( Int B))) c= ( Cl ( Int (A \/ B))) by PRE_TOPC: 19, TOPS_1: 20;

      then

       A7: (( Cl ( Int A)) \/ ( Cl ( Int B))) c= ( Cl ( Int (A \/ B))) by PRE_TOPC: 20;

      

       A8: ( Int ( Cl B)) = ( Int ( Cl ( Int B))) by A2, Th41;

      ( Cl ( Int (A /\ B))) c= ( Cl (A /\ B)) by PRE_TOPC: 19, TOPS_1: 16;

      then

       A9: ( Int ( Cl ( Int (A /\ B)))) c= ( Int ( Cl (A /\ B))) by TOPS_1: 19;

      ( Int ( Cl A)) = ( Int ( Cl ( Int A))) by A1, Th41;

      then (( Int ( Cl A)) /\ ( Int ( Cl B))) = ( Int ( Cl ( Int (A /\ B)))) by A8, Th1;

      hence thesis by A5, A9, A7, A4, A6, XBOOLE_0:def 10;

    end;

    theorem :: ISOMICHI:44

    A is 1st_class & B is 1st_class implies (A \/ B) is 1st_class & (A /\ B) is 1st_class

    proof

      assume that

       A1: A is 1st_class and

       A2: B is 1st_class;

      

       A3: ( Cl ( Int A)) = ( Cl ( Int ( Cl A))) by A1, Th41;

      

       A4: ( Int ( Cl B)) = ( Int ( Cl ( Int B))) by A2, Th41;

      

       A5: ( Int ( Cl A)) = ( Int ( Cl ( Int A))) by A1, Th41;

      

       A6: ( Cl ( Int B)) = ( Cl ( Int ( Cl B))) by A2, Th41;

      

       A7: ( Cl ( Int (A \/ B))) = (( Cl ( Int A)) \/ ( Cl ( Int B))) by A1, A2, Th43

      .= ( Cl ( Int ( Cl (A \/ B)))) by A3, A6, Th2;

      ( Int ( Cl (A /\ B))) = (( Int ( Cl A)) /\ ( Int ( Cl B))) by A1, A2, Th43

      .= ( Int ( Cl ( Int (A /\ B)))) by A5, A4, Th1;

      hence thesis by A7, Th42;

    end;