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


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 -) `) -
proof end;

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
proof end;
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 )
proof end;

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 )
proof end;

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
proof end;
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
proof end;
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 `)) `)) `)) `)}

proof end;

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 )
proof end;

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

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
proof end;
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)))}
proof end;

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 & Cl Q in Kurat7Set A )
proof end;

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.[
proof end;

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}
proof end;

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;

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.[
proof end;

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

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

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

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

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

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

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

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

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

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
proof end;

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

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

theorem :: KURATO_1:39
Int KurExSet <> Cl KurExSet
proof end;

theorem Th40: :: KURATO_1:40
Cl KurExSet <> KurExSet
proof end;

theorem Th41: :: KURATO_1:41
KurExSet <> Int KurExSet
proof end;

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

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

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

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

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

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

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
proof end;

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

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

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

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_distinct by Th46, Th47, Th51, BORSUK_5:6;

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

theorem :: KURATO_1:53
{(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet))),(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} misses {KurExSet}
proof end;

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_distinct by Th52;

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

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

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

registration
cluster Kurat14Set KurExSet -> with_non-empty_elements ;
coherence
Kurat14Set KurExSet is with_non-empty_elements
proof end;
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
proof end;

registration
cluster Kurat14ClPart KurExSet -> with_non-empty_elements ;
coherence
Kurat14ClPart KurExSet is with_non-empty_elements
proof end;
cluster Kurat14OpPart KurExSet -> with_non-empty_elements ;
coherence
Kurat14OpPart KurExSet is with_non-empty_elements
proof end;
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 & b1 is with_non-empty_elements )
proof end;
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 & G is closed holds
F misses G
proof end;

registration
cluster Kurat14ClPart KurExSet -> closed ;
coherence
Kurat14ClPart KurExSet is closed
by ENUMSET1:def 4;
cluster Kurat14OpPart KurExSet -> open ;
coherence
Kurat14OpPart KurExSet is open
by ENUMSET1:def 4;
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
proof end;

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

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

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

theorem Th62: :: KURATO_1:62
KurExSet <> KurExSet ` by XBOOLE_1:66, XBOOLE_1:79;

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

:: WP: Kuratowski's closure-complement problem
theorem :: KURATO_1:64
card (Kurat14Set KurExSet) = 14
proof end;

definition
let T be TopStruct ;
let A be Subset-Family of T;
attr A is Cl-closed means :: KURATO_1:def 7
for P being Subset of T st P in A holds
Cl P in A;
attr A 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
by Th6;
cluster Kurat14Set A -> compl-closed ;
coherence
Kurat14Set A is compl-closed
proof end;
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
by Th9;
cluster Kurat7Set A -> Cl-closed ;
coherence
Kurat7Set A is Cl-closed
by Th9;
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 & b1 is Cl-closed & not b1 is empty )
proof end;
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 & b1 is Cl-closed & not b1 is empty )
proof end;
end;