ISOMICHI

:: The Properties of Supercondensed Sets, Subcondensed Sets and Condensed Sets
::  by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 31, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, PRE_TOPC, SUBSET_1, ZFMISC_1, TEX_1, TDLAT_3, XBOOLE_0,
      STRUCT_0, TOPS_1, RCOMP_1, TARSKI, DECOMP_1, TOPMETR, XXREAL_1, XXREAL_0,
      BORSUK_5, ARYTM_3, LIMFUNC1, ISOMICHI, REAL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, LIMFUNC1, RCOMP_1,
      NUMBERS, DOMAIN_1, ZFMISC_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TEX_1,
      TOPMETR, BORSUK_5, SEQ_4, DECOMP_1, XXREAL_0;
 constructors PROB_1, SEQ_4, RCOMP_1, LIMFUNC1, TOPS_1, TDLAT_3, TEX_1,
      TOPMETR, BORSUK_5, DECOMP_1;
 registrations XBOOLE_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, ZFMISC_1,
      STRUCT_0, TOPS_1, TEX_1, TEX_2, TOPMETR, FCONT_3, PRE_TOPC;
 requirements BOOLE, SUBSET, NUMERALS, REAL;
 definitions TARSKI;
 equalities SUBSET_1, STRUCT_0, LIMFUNC1, PROB_1;
 expansions SUBSET_1;
 theorems SUBSET_1, XBOOLE_0, XBOOLE_1, PRE_TOPC, TOPS_1, TDLAT_1, TDLAT_3,
      PCOMPS_1, TEX_1, BORSUK_5, TOPMETR, DECOMP_1, TOPGEN_1, TOPS_3, XXREAL_0,
      XXREAL_1, JORDAN5A;

begin :: Preliminaries

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 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 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 :: Connections between Supercondensed, Condensed and Subcondensed Sets

definition
  let T be TopStruct, A be Subset of T;
  attr A is supercondensed means
  :Def1:
  Int Cl A = Int A;
  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 :: Remark 1
  A is closed implies A is supercondensed;

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

definition
  let T be TopSpace, A be Subset of T;
  redefine attr A is condensed means  :: redefines condensed (TOPS_1, definition)

  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  :: Remark 2
  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 :: Theorem 1
  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 :: Theorem 1
  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;

:: Corollary to Theorem 1
::  A is condensed implies A` is condensed = TDLAT_1:16;

theorem Th8: :: Theorem 2
  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 Th9: :: Theorem 2
  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 Th10: :: Corollary to Theorem 2
  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 :: Regular Open and Regular Closed Sets

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 :: Remark 1
  for T being 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,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,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,def 8;
  end;
end;

theorem
  Int Cl {}T = {}T
proof
  Int Cl {}T = Int {}T by PCOMPS_1:2
    .= {}T;
  hence thesis;
end;

theorem Th13: :: Remark 2
  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 Th14: :: Remark 2
  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;

:: (A is regular_open & B is regular_open) implies
::   A /\ B is regular_open by TOPS_1:109;
:: A is regular_closed & B is regular_closed implies
::   A \/ B is regular_closed by TOPS_1:108;

theorem Th15: :: Remark 3
  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,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 :: Theorem 3
  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 :: Theorem 3
  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 :: Corollary to Theorem 3:: Theorem 4
  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 :: Theorem 4
  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 :: Boundaries and Borders

definition
  let T be TopStruct, A be Subset of T;
  redefine func Fr A equals  :: redefines Fr (TOPS_1, definition)
  Cl A \ Int A;
  compatibility by TOPGEN_1:8;
end;

theorem :: Theorem 5
  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,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
,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;
  func Border A -> Subset of T equals
  Int Fr A;
  coherence;
end;

theorem Th21: :: Theorem 6
  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 Th22: :: Theorem 7
  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 Th23: :: Theorem 7
  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 :: Remark:: Corollary to Theorem 7
  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 :: Auxiliary Theorems

theorem
  for A being Subset of R^1, a being 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,288;
  then Cl A` = [.a,+infty .[ by BORSUK_5:49;
  then (Cl A`)` = ]. -infty, a.[ by TOPMETR:17,XXREAL_1:224,294;
  hence thesis by TOPS_1:def 1;
end;

theorem
  for A being Subset of R^1, a being 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,294;
  then Cl A` = ]. -infty,a.] by BORSUK_5:51;
  then (Cl A`)` = ].a,+infty .[ by TOPMETR:17,XXREAL_1:224,288;
  hence thesis by TOPS_1:def 1;
end;

theorem Th27:
  for A being Subset of R^1, a, b being 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
  for A being Subset of R^1, a, b being 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
  for A being Subset of R^1, a, b being 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
  for a,b being 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 Th31:
  for a,b being 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 Th32:
  for A being Subset of R^1, a, b, c being 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,294;
  hence thesis by TOPS_1:def 1;
end;

Lm1: for a,b being 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
  for a,b being 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 Th34:
  for A being Subset of R^1, a, b, c being 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,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,294
    .= ]. -infty, a .[ \/ ].b,c.[ by A2,A3,XXREAL_0:2,XXREAL_1:339;
  hence thesis by TOPS_1:def 1;
end;

begin :: Classification of Subsets

notation
  let A, B be set;
  antonym A, B are_c=-incomparable for A, B are_c=-comparable;
end;

theorem Th35:
  for A, B being 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;
  attr A is 1st_class means

  Int Cl A c= Cl Int A;
  attr A is 2nd_class means

  Cl Int A c< Int Cl A;
  attr A is 3rd_class means

  Cl Int A, Int Cl A are_c=-incomparable;
end;

theorem
  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 Th37: :: Remark 1
  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;
  attr T is with_1st_class_subsets means

  ex A being Subset of T st A is 1st_class;
  attr T is with_2nd_class_subsets means
  :Def10:
  ex A being Subset of T st A is 2nd_class;
  attr T is with_3rd_class_subsets means
  :Def11:
  ex A being 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 Th38: :: Theorem 8
  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 Th39: :: Theorem 8
  A is 2nd_class iff A` is 2nd_class
proof
A1: for A being 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 Th40: :: Theorem 8
  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 Th41: :: Theorem 9
  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 Th42: :: Theorem 9
  (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 Th43: :: Theorem 10
  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 :: Theorem 11
  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;
 
:: TODO: Remark 2 from Isomichi's paper
:: condensed = domain    Int Cl A c= Cl Int A 
:: closed domain:   A = Cl Int A:  regular_closed = closed_condensed 
:: open domain:     A = Int Cl A:  regular_open = open_condensed