:: On the {K}uratowski Closure-Complement Problem
:: by Lilla Krystyna Bagi\'nska and Adam Grabowski
::
:: Received June 12, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

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

theorem Th1: :: KURATO_1:1
for T being non empty TopSpace
for A being Subset of T holds ((((((A -) `) -) `) -) `) - = ((A -) `) -
proofend;

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

definition
let T be non empty TopSpace;
let A be Subset of T;
func Kurat14Part A ->  set  equals :: KURATO_1:def 1
{A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)};
coherence
 {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} is set ;
end;

:: deftheorem  defines Kurat14Part KURATO_1:def_1_:_
 for T being non empty TopSpace
for A being Subset of T holds Kurat14Part A = {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)};

registration
let T be non empty TopSpace;
let A be Subset of T;
cluster Kurat14Part A ->  finite ;
coherence
 Kurat14Part A is finite ;
end;

definition
let T be non empty TopSpace;
let A be Subset of T;
func Kurat14Set A ->  Subset-Family of T equals :: KURATO_1:def 2
{A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)};
coherence
 {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T
proofend;
end;

:: deftheorem  defines Kurat14Set KURATO_1:def_2_:_
 for T being non empty TopSpace
for A being Subset of T holds Kurat14Set A = {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)};

theorem :: KURATO_1:2
for T being non empty TopSpace
for A being Subset of T holds Kurat14Set A = (Kurat14Part A) \/ (Kurat14Part (A `)) ;

theorem Th3: :: KURATO_1:3
for T being non empty TopSpace
for A being Subset of T holds
( 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 )
proofend;

theorem Th4: :: KURATO_1:4
for T being non empty TopSpace
for A being Subset of T holds
( 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 )
proofend;

definition
let T be non empty TopSpace;
let A be Subset of T;
func Kurat14ClPart A ->  Subset-Family of T equals :: KURATO_1:def 3
{(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)};
coherence
 {(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)} is Subset-Family of T
proofend;
func Kurat14OpPart A ->  Subset-Family of T equals :: KURATO_1:def 4
{((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)};
coherence
 {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T
proofend;
end;

:: deftheorem  defines Kurat14ClPart KURATO_1:def_3_:_
 for T being non empty TopSpace
for A being Subset of T holds Kurat14ClPart A = {(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)};

:: deftheorem  defines Kurat14OpPart KURATO_1:def_4_:_
 for T being non empty TopSpace
for A being Subset of T holds Kurat14OpPart A = {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)};

Lm2:  for T being non empty TopSpace
for A being Subset of T holds 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 `)) `)) `)) `)}
proofend;

theorem :: KURATO_1:5
for T being non empty TopSpace
for A being Subset of T holds Kurat14Set A = ({A,(A `)} \/ (Kurat14ClPart A)) \/ (Kurat14OpPart A) by Lm2;

registration
let T be non empty TopSpace;
let A be Subset of T;
cluster Kurat14Set A ->  finite ;
coherence
 Kurat14Set A is finite ;
end;

theorem Th6: :: KURATO_1:6
for T being non empty TopSpace
for A, Q being Subset of T st Q in Kurat14Set A holds
( Q ` in Kurat14Set A & Q - in Kurat14Set A )
proofend;

theorem :: KURATO_1:7
for T being non empty TopSpace
for A being Subset of T holds card (Kurat14Set A) <= 14
proofend;

begin

definition
let T be non empty TopSpace;
let A be Subset of T;
func Kurat7Set A ->  Subset-Family of T equals :: KURATO_1:def 5
{A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))};
coherence
 {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} is Subset-Family of T
proofend;
end;

:: deftheorem  defines Kurat7Set KURATO_1:def_5_:_
 for T being non empty TopSpace
for A being Subset of T holds Kurat7Set A = {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))};

theorem :: KURATO_1:8
for T being non empty TopSpace
for A being Subset of T holds Kurat7Set A = ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))}
proofend;

registration
let T be non empty TopSpace;
let A be Subset of T;
cluster Kurat7Set A ->  finite ;
coherence
 Kurat7Set A is finite ;
end;

theorem Th9: :: KURATO_1:9
for T being non empty TopSpace
for A, Q being Subset of T st Q in Kurat7Set A holds
( Int Q in Kurat7Set A &amp; Cl Q in Kurat7Set A )
proofend;

begin

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

:: deftheorem  defines KurExSet KURATO_1:def_6_:_
 KurExSet = (({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[;

theorem Th10: :: KURATO_1:10
Cl KurExSet = {1} \/ [.2,+infty.[
proofend;

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

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

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

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

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

theorem Th16: :: KURATO_1:16
KurExSet ` = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5}
proofend;

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

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

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

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

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

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

begin

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

theorem Th24: :: KURATO_1:24
Cl (Int KurExSet) = [.4,+infty.[ by Th18, BORSUK_5:55, TOPS_1:def_1;

theorem Th25: :: KURATO_1:25
Int (Cl (Int KurExSet)) = ].4,+infty.[
proofend;

theorem Th26: :: KURATO_1:26
Int (Cl KurExSet) = ].2,+infty.[
proofend;

theorem Th27: :: KURATO_1:27
Cl (Int (Cl KurExSet)) = [.2,+infty.[
proofend;

begin

theorem :: KURATO_1:28
Cl (Int (Cl KurExSet)) <> Int (Cl KurExSet)
proofend;

theorem Th29: :: KURATO_1:29
Cl (Int (Cl KurExSet)) <> Cl KurExSet
proofend;

theorem :: KURATO_1:30
Cl (Int (Cl KurExSet)) <> Int (Cl (Int KurExSet))
proofend;

theorem Th31: :: KURATO_1:31
Cl (Int (Cl KurExSet)) <> Cl (Int KurExSet)
proofend;

theorem :: KURATO_1:32
Cl (Int (Cl KurExSet)) <> Int KurExSet
proofend;

theorem :: KURATO_1:33
Int (Cl KurExSet) <> Cl KurExSet
proofend;

theorem :: KURATO_1:34
Int (Cl KurExSet) <> Int (Cl (Int KurExSet))
proofend;

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

theorem Th36: :: KURATO_1:36
Int (Cl KurExSet) <> Int KurExSet
proofend;

theorem :: KURATO_1:37
Int (Cl (Int KurExSet)) <> Cl KurExSet
proofend;

theorem Th38: :: KURATO_1:38
Cl (Int KurExSet) <> Cl KurExSet
proofend;

theorem :: KURATO_1:39
Int KurExSet <> Cl KurExSet
proofend;

theorem Th40: :: KURATO_1:40
Cl KurExSet <> KurExSet
proofend;

theorem Th41: :: KURATO_1:41
KurExSet <> Int KurExSet
proofend;

theorem :: KURATO_1:42
Cl (Int KurExSet) <> Int (Cl (Int KurExSet))
proofend;

theorem Th43: :: KURATO_1:43
Int (Cl (Int KurExSet)) <> Int KurExSet
proofend;

theorem :: KURATO_1:44
Cl (Int KurExSet) <> Int KurExSet
proofend;

begin

theorem Th45: :: KURATO_1:45
Int (Cl (Int KurExSet)) <> Int (Cl KurExSet)
proofend;

theorem Th46: :: KURATO_1:46
Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)) are_mutually_different
proofend;

theorem Th47: :: KURATO_1:47
Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different
proofend;

theorem Th48: :: KURATO_1:48
for X being set st X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} holds
X is non empty open Subset of R^1
proofend;

theorem Th49: :: KURATO_1:49
for X being set st X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} holds
X <> REAL
proofend;

theorem :: KURATO_1:50
for X being set st X in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} holds
X <> REAL
proofend;

theorem Th51: :: KURATO_1:51
{(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} misses {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))}
proofend;

theorem Th52: :: KURATO_1:52
Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different by Th46, Th47, Th51, BORSUK_5:6;

registration
cluster KurExSet  ->  non open non closed ;
coherence
 ( not KurExSet is closed &amp; not KurExSet is open ) by Th40, Th41, PRE_TOPC:22, TOPS_1:23;
end;

theorem Th53: :: KURATO_1:53
{(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet))),(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} misses {KurExSet}
proofend;

theorem Th54: :: KURATO_1:54
KurExSet , Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different
proofend;

theorem :: KURATO_1:55
card (Kurat7Set KurExSet) = 7
proofend;

begin

registration
cluster Kurat14ClPart KurExSet ->  with_proper_subsets ;
coherence
 Kurat14ClPart KurExSet is with_proper_subsets
proofend;
cluster Kurat14OpPart KurExSet ->  with_proper_subsets ;
coherence
 Kurat14OpPart KurExSet is with_proper_subsets
proofend;
end;

registration
cluster Kurat14Set KurExSet ->  with_proper_subsets ;
coherence
 Kurat14Set KurExSet is with_proper_subsets
proofend;
end;

registration
cluster Kurat14Set KurExSet ->  with_non-empty_elements ;
coherence
 Kurat14Set KurExSet is with_non-empty_elements
proofend;
end;

theorem Th56: :: KURATO_1:56
for A being with_non-empty_elements set
for B being set st B c= A holds
B is with_non-empty_elements
proofend;

registration
cluster Kurat14ClPart KurExSet ->  with_non-empty_elements ;
coherence
 Kurat14ClPart KurExSet is with_non-empty_elements
proofend;
cluster Kurat14OpPart KurExSet ->  with_non-empty_elements ;
coherence
 Kurat14OpPart KurExSet is with_non-empty_elements
proofend;
end;

registration
cluster with_non-empty_elements with_proper_subsets for Element of bool (bool the carrier of R^1);
existence
 ex b1 being Subset-Family of R^1 st
( b1 is with_proper_subsets &amp; b1 is with_non-empty_elements )
proofend;
end;

theorem Th57: :: KURATO_1:57
for F, G being with_non-empty_elements with_proper_subsets Subset-Family of R^1 st F is open &amp; G is closed holds
F misses G
proofend;

registration
cluster Kurat14ClPart KurExSet ->  closed ;
coherence
 Kurat14ClPart KurExSet is closed
proofend;
cluster Kurat14OpPart KurExSet ->  open ;
coherence
 Kurat14OpPart KurExSet is open
proofend;
end;

theorem :: KURATO_1:58
Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th57;

registration
let T be non empty TopSpace;
let A be Subset of T;
cluster Kurat14ClPart A ->  finite ;
coherence
 Kurat14ClPart A is finite ;
cluster Kurat14OpPart A ->  finite ;
coherence
 Kurat14OpPart A is finite ;
end;

theorem Th59: :: KURATO_1:59
card (Kurat14ClPart KurExSet) = 6
proofend;

theorem Th60: :: KURATO_1:60
card (Kurat14OpPart KurExSet) = 6
proofend;

theorem Th61: :: KURATO_1:61
{KurExSet,(KurExSet `)} misses Kurat14ClPart KurExSet
proofend;

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

theorem Th62: :: KURATO_1:62
KurExSet <> KurExSet `
proofend;

theorem Th63: :: KURATO_1:63
{KurExSet,(KurExSet `)} misses Kurat14OpPart KurExSet
proofend;

:: [WP: ] Kuratowski_closure-complement_problem
theorem :: KURATO_1:64
card (Kurat14Set KurExSet) = 14
proofend;

begin

definition
let T be TopStruct ;
let A be Subset-Family of T;
attrA is Cl-closed  means :: KURATO_1:def 7
 for P being Subset of T st P in A holds
Cl P in A;
attrA is Int-closed  means :: KURATO_1:def 8
 for P being Subset of T st P in A holds
Int P in A;
end;

:: deftheorem  defines Cl-closed KURATO_1:def_7_:_
 for T being TopStruct
for A being Subset-Family of T holds
( A is Cl-closed iff for P being Subset of T st P in A holds
Cl P in A );

:: deftheorem  defines Int-closed KURATO_1:def_8_:_
 for T being TopStruct
for A being Subset-Family of T holds
( A is Int-closed iff for P being Subset of T st P in A holds
Int P in A );

registration
let T be non empty TopSpace;
let A be Subset of T;
cluster Kurat14Set A ->  non empty ;
coherence
 not Kurat14Set A is empty ;
cluster Kurat14Set A ->  Cl-closed ;
coherence
 Kurat14Set A is Cl-closed
proofend;
cluster Kurat14Set A ->  compl-closed ;
coherence
 Kurat14Set A is compl-closed
proofend;
end;

registration
let T be non empty TopSpace;
let A be Subset of T;
cluster Kurat7Set A ->  non empty ;
coherence
 not Kurat7Set A is empty ;
cluster Kurat7Set A ->  Int-closed ;
coherence
 Kurat7Set A is Int-closed
proofend;
cluster Kurat7Set A ->  Cl-closed ;
coherence
 Kurat7Set A is Cl-closed
proofend;
end;

registration
let T be non empty TopSpace;
cluster non empty Cl-closed Int-closed for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is Int-closed &amp; b1 is Cl-closed &amp; not b1 is empty )
proofend;
cluster non empty compl-closed Cl-closed for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is compl-closed &amp; b1 is Cl-closed &amp; not b1 is empty )
proofend;
end;