:: KURATO_1 semantic presentation

notation
let c1 be non empty TopSpace;
let c2 be Subset of c1;
synonym c2 - for Cl c2;
end;

theorem Th1: :: KURATO_1:1
for b1 being non empty TopSpace
for b2 being Subset of b1 holds ((((((b2 - ) ` ) - ) ` ) - ) ` ) - = ((b2 - ) ` ) -
proof end;

Lemma2: for b1 being 1-sorted
for b2, b3 being Subset-Family of b1 holds b2 \/ b3 is Subset-Family of b1
;

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

:: deftheorem Def1 defines Kurat14Part KURATO_1:def 1 :
for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat14Part b2 = {b2,(b2 - ),((b2 - ) ` ),(((b2 - ) ` ) - ),((((b2 - ) ` ) - ) ` ),(((((b2 - ) ` ) - ) ` ) - ),((((((b2 - ) ` ) - ) ` ) - ) ` )};

registration
let c1 be non empty TopSpace;
let c2 be Subset of c1;
cluster Kurat14Part a2 -> finite ;
coherence
Kurat14Part c2 is finite ;
end;

definition
let c1 be non empty TopSpace;
let c2 be Subset of c1;
func Kurat14Set c2 -> Subset-Family of a1 equals :: KURATO_1:def 2
{a2,(a2 - ),((a2 - ) ` ),(((a2 - ) ` ) - ),((((a2 - ) ` ) - ) ` ),(((((a2 - ) ` ) - ) ` ) - ),((((((a2 - ) ` ) - ) ` ) - ) ` )} \/ {(a2 ` ),((a2 ` ) - ),(((a2 ` ) - ) ` ),((((a2 ` ) - ) ` ) - ),(((((a2 ` ) - ) ` ) - ) ` ),((((((a2 ` ) - ) ` ) - ) ` ) - ),(((((((a2 ` ) - ) ` ) - ) ` ) - ) ` )};
coherence
{c2,(c2 - ),((c2 - ) ` ),(((c2 - ) ` ) - ),((((c2 - ) ` ) - ) ` ),(((((c2 - ) ` ) - ) ` ) - ),((((((c2 - ) ` ) - ) ` ) - ) ` )} \/ {(c2 ` ),((c2 ` ) - ),(((c2 ` ) - ) ` ),((((c2 ` ) - ) ` ) - ),(((((c2 ` ) - ) ` ) - ) ` ),((((((c2 ` ) - ) ` ) - ) ` ) - ),(((((((c2 ` ) - ) ` ) - ) ` ) - ) ` )} is Subset-Family of c1
proof end;
end;

:: deftheorem Def2 defines Kurat14Set KURATO_1:def 2 :
for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat14Set b2 = {b2,(b2 - ),((b2 - ) ` ),(((b2 - ) ` ) - ),((((b2 - ) ` ) - ) ` ),(((((b2 - ) ` ) - ) ` ) - ),((((((b2 - ) ` ) - ) ` ) - ) ` )} \/ {(b2 ` ),((b2 ` ) - ),(((b2 ` ) - ) ` ),((((b2 ` ) - ) ` ) - ),(((((b2 ` ) - ) ` ) - ) ` ),((((((b2 ` ) - ) ` ) - ) ` ) - ),(((((((b2 ` ) - ) ` ) - ) ` ) - ) ` )};

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

theorem Th3: :: KURATO_1:3
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 in Kurat14Set b2 & b2 - in Kurat14Set b2 & (b2 - ) ` in Kurat14Set b2 & ((b2 - ) ` ) - in Kurat14Set b2 & (((b2 - ) ` ) - ) ` in Kurat14Set b2 & ((((b2 - ) ` ) - ) ` ) - in Kurat14Set b2 & (((((b2 - ) ` ) - ) ` ) - ) ` in Kurat14Set b2 )
proof end;

theorem Th4: :: KURATO_1:4
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 ` in Kurat14Set b2 & (b2 ` ) - in Kurat14Set b2 & ((b2 ` ) - ) ` in Kurat14Set b2 & (((b2 ` ) - ) ` ) - in Kurat14Set b2 & ((((b2 ` ) - ) ` ) - ) ` in Kurat14Set b2 & (((((b2 ` ) - ) ` ) - ) ` ) - in Kurat14Set b2 & ((((((b2 ` ) - ) ` ) - ) ` ) - ) ` in Kurat14Set b2 )
proof end;

definition
let c1 be non empty TopSpace;
let c2 be Subset of c1;
func Kurat14ClPart c2 -> Subset-Family of a1 equals :: KURATO_1:def 3
{(a2 - ),(((a2 - ) ` ) - ),(((((a2 - ) ` ) - ) ` ) - ),((a2 ` ) - ),((((a2 ` ) - ) ` ) - ),((((((a2 ` ) - ) ` ) - ) ` ) - )};
coherence
{(c2 - ),(((c2 - ) ` ) - ),(((((c2 - ) ` ) - ) ` ) - ),((c2 ` ) - ),((((c2 ` ) - ) ` ) - ),((((((c2 ` ) - ) ` ) - ) ` ) - )} is Subset-Family of c1
proof end;
func Kurat14OpPart c2 -> Subset-Family of a1 equals :: KURATO_1:def 4
{((a2 - ) ` ),((((a2 - ) ` ) - ) ` ),((((((a2 - ) ` ) - ) ` ) - ) ` ),(((a2 ` ) - ) ` ),(((((a2 ` ) - ) ` ) - ) ` ),(((((((a2 ` ) - ) ` ) - ) ` ) - ) ` )};
coherence
{((c2 - ) ` ),((((c2 - ) ` ) - ) ` ),((((((c2 - ) ` ) - ) ` ) - ) ` ),(((c2 ` ) - ) ` ),(((((c2 ` ) - ) ` ) - ) ` ),(((((((c2 ` ) - ) ` ) - ) ` ) - ) ` )} is Subset-Family of c1
proof end;
end;

:: deftheorem Def3 defines Kurat14ClPart KURATO_1:def 3 :
for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat14ClPart b2 = {(b2 - ),(((b2 - ) ` ) - ),(((((b2 - ) ` ) - ) ` ) - ),((b2 ` ) - ),((((b2 ` ) - ) ` ) - ),((((((b2 ` ) - ) ` ) - ) ` ) - )};

:: deftheorem Def4 defines Kurat14OpPart KURATO_1:def 4 :
for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat14OpPart b2 = {((b2 - ) ` ),((((b2 - ) ` ) - ) ` ),((((((b2 - ) ` ) - ) ` ) - ) ` ),(((b2 ` ) - ) ` ),(((((b2 ` ) - ) ` ) - ) ` ),(((((((b2 ` ) - ) ` ) - ) ` ) - ) ` )};

Lemma5: for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat14Set b2 = ({(Cl b2),(Cl ((Cl b2) ` )),(Cl ((Cl ((Cl b2) ` )) ` )),(Cl (b2 ` )),(Cl ((Cl (b2 ` )) ` )),(Cl ((Cl ((Cl (b2 ` )) ` )) ` ))} \/ {b2,(b2 ` )}) \/ {((Cl b2) ` ),((Cl ((Cl b2) ` )) ` ),((Cl ((Cl ((Cl b2) ` )) ` )) ` ),((Cl (b2 ` )) ` ),((Cl ((Cl (b2 ` )) ` )) ` ),((Cl ((Cl ((Cl (b2 ` )) ` )) ` )) ` )}
proof end;

theorem Th5: :: KURATO_1:5
for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat14Set b2 = ({b2,(b2 ` )} \/ (Kurat14ClPart b2)) \/ (Kurat14OpPart b2) by Lemma5;

registration
let c1 be non empty TopSpace;
let c2 be Subset of c1;
cluster Kurat14Set a2 -> finite ;
coherence
Kurat14Set c2 is finite ;
end;

theorem Th6: :: KURATO_1:6
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b3 in Kurat14Set b2 holds
( b3 ` in Kurat14Set b2 & b3 - in Kurat14Set b2 )
proof end;

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

definition
let c1 be non empty TopSpace;
let c2 be Subset of c1;
func Kurat7Set c2 -> Subset-Family of a1 equals :: KURATO_1:def 5
{a2,(Int a2),(Cl a2),(Int (Cl a2)),(Cl (Int a2)),(Cl (Int (Cl a2))),(Int (Cl (Int a2)))};
coherence
{c2,(Int c2),(Cl c2),(Int (Cl c2)),(Cl (Int c2)),(Cl (Int (Cl c2))),(Int (Cl (Int c2)))} is Subset-Family of c1
proof end;
end;

:: deftheorem Def5 defines Kurat7Set KURATO_1:def 5 :
for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat7Set b2 = {b2,(Int b2),(Cl b2),(Int (Cl b2)),(Cl (Int b2)),(Cl (Int (Cl b2))),(Int (Cl (Int b2)))};

theorem Th8: :: KURATO_1:8
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 in Kurat7Set b2 & Int b2 in Kurat7Set b2 & Cl b2 in Kurat7Set b2 & Int (Cl b2) in Kurat7Set b2 & Cl (Int b2) in Kurat7Set b2 & Cl (Int (Cl b2)) in Kurat7Set b2 & Int (Cl (Int b2)) in Kurat7Set b2 ) by ENUMSET1:def 5;

theorem Th9: :: KURATO_1:9
for b1 being non empty TopSpace
for b2 being Subset of b1 holds Kurat7Set b2 = ({b2} \/ {(Int b2),(Int (Cl b2)),(Int (Cl (Int b2)))}) \/ {(Cl b2),(Cl (Int b2)),(Cl (Int (Cl b2)))}
proof end;

registration
let c1 be non empty TopSpace;
let c2 be Subset of c1;
cluster Kurat7Set a2 -> finite ;
coherence
Kurat7Set c2 is finite ;
end;

theorem Th10: :: KURATO_1:10
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b3 in Kurat7Set b2 holds
( Int b3 in Kurat7Set b2 & Cl b3 in Kurat7Set b2 )
proof end;

theorem Th11: :: KURATO_1:11
for b1 being non empty TopSpace
for b2 being Subset of b1 holds card (Kurat7Set b2) <= 7 by CARD_2:74;

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:24;
end;

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

theorem Th12: :: KURATO_1:12
Cl KurExSet = {1} \/ [.2,+infty.[
proof end;

theorem Th13: :: KURATO_1:13
(Cl KurExSet ) ` = ].-infty,1.[ \/ ].1,2.[ by Th12, BORSUK_5:95;

theorem Th14: :: KURATO_1:14
Cl ((Cl KurExSet ) ` ) = ].-infty,2.] by Th13, BORSUK_5:96;

theorem Th15: :: KURATO_1:15
(Cl ((Cl KurExSet ) ` )) ` = ].2,+infty.[ by Th14, BORSUK_5:98;

theorem Th16: :: KURATO_1:16
Cl ((Cl ((Cl KurExSet ) ` )) ` ) = [.2,+infty.[ by Th15, BORSUK_5:75;

theorem Th17: :: KURATO_1:17
(Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` = ].-infty,2.[ by Th16, BORSUK_5:99;

theorem Th18: :: KURATO_1:18
KurExSet ` = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT 2,4)) \/ {4}) \/ {5}
proof end;

theorem Th19: :: KURATO_1:19
Cl (KurExSet ` ) = ].-infty,4.] \/ {5} by Th18, BORSUK_5:101;

theorem Th20: :: KURATO_1:20
(Cl (KurExSet ` )) ` = ].4,5.[ \/ ].5,+infty.[ by Th19, BORSUK_5:102;

theorem Th21: :: KURATO_1:21
Cl ((Cl (KurExSet ` )) ` ) = [.4,+infty.[ by Th20, BORSUK_5:81;

theorem Th22: :: KURATO_1:22
(Cl ((Cl (KurExSet ` )) ` )) ` = ].-infty,4.[ by Th21, BORSUK_5:99;

theorem Th23: :: KURATO_1:23
Cl ((Cl ((Cl (KurExSet ` )) ` )) ` ) = ].-infty,4.] by Th22, BORSUK_5:77;

theorem Th24: :: KURATO_1:24
(Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` = ].4,+infty.[ by Th23, BORSUK_5:98;

theorem Th25: :: KURATO_1:25
Int KurExSet = ].4,5.[ \/ ].5,+infty.[ by Th20, TOPS_1:def 1;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th42: :: KURATO_1:42
Cl KurExSet <> KurExSet
proof end;

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

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

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

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

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

theorem Th48: :: KURATO_1:48
Int KurExSet , Int (Cl KurExSet ), Int (Cl (Int KurExSet )) are_mutually_different
proof end;

theorem Th49: :: KURATO_1:49
Cl KurExSet , Cl (Int KurExSet ), Cl (Int (Cl KurExSet )) are_mutually_different
proof end;

theorem Th50: :: KURATO_1:50
for b1 being set st b1 in {(Int KurExSet ),(Int (Cl KurExSet )),(Int (Cl (Int KurExSet )))} holds
b1 is non empty open Subset of R^1
proof end;

theorem Th51: :: KURATO_1:51
canceled;

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

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

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

theorem Th55: :: KURATO_1:55
Int KurExSet , Int (Cl KurExSet ), Int (Cl (Int KurExSet )), Cl KurExSet , Cl (Int KurExSet ), Cl (Int (Cl KurExSet )) are_mutually_different by Th48, Th49, Th54, BORSUK_5:7;

registration
cluster KurExSet -> non open non closed ;
coherence
( not KurExSet is closed & not KurExSet is open ) by Th42, Th43, PRE_TOPC:52, TOPS_1:55;
end;

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

theorem Th57: :: KURATO_1:57
KurExSet , Int KurExSet , Int (Cl KurExSet ), Int (Cl (Int KurExSet )), Cl KurExSet , Cl (Int KurExSet ), Cl (Int (Cl KurExSet )) are_mutually_different
proof end;

theorem Th58: :: KURATO_1:58
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 -> finite with_proper_subsets ;
coherence
Kurat14Set KurExSet is with_proper_subsets
proof end;
end;

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

theorem Th59: :: KURATO_1:59
for b1 being with_non-empty_elements set
for b2 being set st b2 c= b1 holds
b2 is with_non-empty_elements
proof end;

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

registration
cluster with_proper_subsets with_non-empty_elements Element of K10(K10(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 Th60: :: KURATO_1:60
for b1, b2 being with_proper_subsets with_non-empty_elements Subset-Family of R^1 st b1 is open & b2 is closed holds
b1 misses b2
proof end;

registration
cluster Kurat14ClPart KurExSet -> with_proper_subsets closed with_non-empty_elements ;
coherence
Kurat14ClPart KurExSet is closed
proof end;
cluster Kurat14OpPart KurExSet -> with_proper_subsets open with_non-empty_elements ;
coherence
Kurat14OpPart KurExSet is open
proof end;
end;

theorem Th61: :: KURATO_1:61
Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th60;

registration
let c1 be non empty TopSpace;
let c2 be Subset of c1;
cluster Kurat14ClPart a2 -> finite ;
coherence
Kurat14ClPart c2 is finite ;
cluster Kurat14OpPart a2 -> finite ;
coherence
Kurat14OpPart c2 is finite ;
end;

theorem Th62: :: KURATO_1:62
card (Kurat14ClPart KurExSet ) = 6
proof end;

theorem Th63: :: KURATO_1:63
card (Kurat14OpPart KurExSet ) = 6
proof end;

theorem Th64: :: KURATO_1:64
{KurExSet ,(KurExSet ` )} misses Kurat14ClPart KurExSet
proof end;

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

theorem Th65: :: KURATO_1:65
KurExSet <> KurExSet `
proof end;

theorem Th66: :: KURATO_1:66
{KurExSet ,(KurExSet ` )} misses Kurat14OpPart KurExSet
proof end;

theorem Th67: :: KURATO_1:67
card (Kurat14Set KurExSet ) = 14
proof end;

definition
let c1 be TopStruct ;
let c2 be Subset-Family of c1;
attr a2 is Cl-closed means :: KURATO_1:def 7
for b1 being Subset of a1 st b1 in a2 holds
Cl b1 in a2;
attr a2 is Int-closed means :: KURATO_1:def 8
for b1 being Subset of a1 st b1 in a2 holds
Int b1 in a2;
end;

:: deftheorem Def7 defines Cl-closed KURATO_1:def 7 :
for b1 being TopStruct
for b2 being Subset-Family of b1 holds
( b2 is Cl-closed iff for b3 being Subset of b1 st b3 in b2 holds
Cl b3 in b2 );

:: deftheorem Def8 defines Int-closed KURATO_1:def 8 :
for b1 being TopStruct
for b2 being Subset-Family of b1 holds
( b2 is Int-closed iff for b3 being Subset of b1 st b3 in b2 holds
Int b3 in b2 );

registration
let c1 be non empty TopSpace;
let c2 be Subset of c1;
cluster Kurat14Set a2 -> non empty finite ;
coherence
not Kurat14Set c2 is empty by Th3;
cluster Kurat14Set a2 -> finite Cl-closed ;
coherence
Kurat14Set c2 is Cl-closed
proof end;
cluster Kurat14Set a2 -> finite compl-closed ;
coherence
Kurat14Set c2 is compl-closed
proof end;
end;

registration
let c1 be non empty TopSpace;
let c2 be Subset of c1;
cluster Kurat7Set a2 -> non empty finite ;
coherence
not Kurat7Set c2 is empty by Th8;
cluster Kurat7Set a2 -> finite Int-closed ;
coherence
Kurat7Set c2 is Int-closed
proof end;
cluster Kurat7Set a2 -> finite Cl-closed ;
coherence
Kurat7Set c2 is Cl-closed
proof end;
end;

registration
let c1 be non empty TopSpace;
cluster non empty Cl-closed Int-closed Element of K10(K10(the carrier of a1));
existence
ex b1 being Subset-Family of c1 st
( b1 is Int-closed & b1 is Cl-closed & not b1 is empty )
proof end;
cluster non empty compl-closed Cl-closed Element of K10(K10(the carrier of a1));
existence
ex b1 being Subset-Family of c1 st
( b1 is compl-closed & b1 is Cl-closed & not b1 is empty )
proof end;
end;