:: KURATO_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

theorem Th1: :: KURATO_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T holds Kurat14Set A = (Kurat14Part A) \/ (Kurat14Part (A ` )) ;

theorem Th3: :: KURATO_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th5: :: KURATO_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th8: :: KURATO_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T holds
( A in Kurat7Set A & Int A in Kurat7Set A & Cl A in Kurat7Set A & Int (Cl A) in Kurat7Set A & Cl (Int A) in Kurat7Set A & Cl (Int (Cl A)) in Kurat7Set A & Int (Cl (Int A)) in Kurat7Set A ) by ENUMSET1:def 5;

theorem :: KURATO_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th10: :: KURATO_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: KURATO_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T holds card (Kurat7Set A) <= 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 defines KurExSet KURATO_1:def 6 :
KurExSet = (({1} \/ (RAT 2,4)) \/ ].4,5.[) \/ ].5,+infty.[;

theorem Th12: :: KURATO_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl KurExSet = {1} \/ [.2,+infty.[
proof end;

theorem Th13: :: KURATO_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(Cl KurExSet ) ` = ].-infty,1.[ \/ ].1,2.[ by Th12, BORSUK_5:95;

theorem Th14: :: KURATO_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl ((Cl KurExSet ) ` ) = ].-infty,2.] by Th13, BORSUK_5:96;

theorem Th15: :: KURATO_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(Cl ((Cl KurExSet ) ` )) ` = ].2,+infty.[ by Th14, BORSUK_5:98;

theorem Th16: :: KURATO_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl ((Cl ((Cl KurExSet ) ` )) ` ) = [.2,+infty.[ by Th15, BORSUK_5:75;

theorem Th17: :: KURATO_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` = ].-infty,2.[ by Th16, BORSUK_5:99;

theorem Th18: :: KURATO_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
KurExSet ` = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT 2,4)) \/ {4}) \/ {5}
proof end;

theorem Th19: :: KURATO_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (KurExSet ` ) = ].-infty,4.] \/ {5} by Th18, BORSUK_5:101;

theorem Th20: :: KURATO_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(Cl (KurExSet ` )) ` = ].4,5.[ \/ ].5,+infty.[ by Th19, BORSUK_5:102;

theorem Th21: :: KURATO_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl ((Cl (KurExSet ` )) ` ) = [.4,+infty.[ by Th20, BORSUK_5:81;

theorem Th22: :: KURATO_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(Cl ((Cl (KurExSet ` )) ` )) ` = ].-infty,4.[ by Th21, BORSUK_5:99;

theorem Th23: :: KURATO_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl ((Cl ((Cl (KurExSet ` )) ` )) ` ) = ].-infty,4.] by Th22, BORSUK_5:77;

theorem Th24: :: KURATO_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` = ].4,+infty.[ by Th23, BORSUK_5:98;

theorem Th25: :: KURATO_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int KurExSet = ].4,5.[ \/ ].5,+infty.[ by Th20, TOPS_1:def 1;

theorem Th26: :: KURATO_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int KurExSet ) = [.4,+infty.[
proof end;

theorem Th27: :: KURATO_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl (Int KurExSet )) = ].4,+infty.[
proof end;

theorem Th28: :: KURATO_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl KurExSet ) = ].2,+infty.[
proof end;

theorem Th29: :: KURATO_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int (Cl KurExSet )) = [.2,+infty.[
proof end;

theorem :: KURATO_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int (Cl KurExSet )) <> Int (Cl KurExSet )
proof end;

theorem Th31: :: KURATO_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int (Cl KurExSet )) <> Cl KurExSet
proof end;

theorem :: KURATO_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int (Cl KurExSet )) <> Int (Cl (Int KurExSet ))
proof end;

theorem Th33: :: KURATO_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int (Cl KurExSet )) <> Cl (Int KurExSet )
proof end;

theorem :: KURATO_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int (Cl KurExSet )) <> Int KurExSet
proof end;

theorem :: KURATO_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl KurExSet ) <> Cl KurExSet
proof end;

theorem :: KURATO_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl KurExSet ) <> Int (Cl (Int KurExSet ))
proof end;

theorem :: KURATO_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl KurExSet ) <> Cl (Int KurExSet )
proof end;

theorem Th38: :: KURATO_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl KurExSet ) <> Int KurExSet
proof end;

theorem :: KURATO_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl (Int KurExSet )) <> Cl KurExSet
proof end;

theorem Th40: :: KURATO_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int KurExSet ) <> Cl KurExSet
proof end;

theorem :: KURATO_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int KurExSet <> Cl KurExSet
proof end;

theorem Th42: :: KURATO_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl KurExSet <> KurExSet
proof end;

theorem Th43: :: KURATO_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
KurExSet <> Int KurExSet
proof end;

theorem :: KURATO_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int KurExSet ) <> Int (Cl (Int KurExSet ))
proof end;

theorem Th45: :: KURATO_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl (Int KurExSet )) <> Int KurExSet
proof end;

theorem :: KURATO_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl (Int KurExSet ) <> Int KurExSet
proof end;

theorem Th47: :: KURATO_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int (Cl (Int KurExSet )) <> Int (Cl KurExSet )
proof end;

theorem Th48: :: KURATO_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Int KurExSet , Int (Cl KurExSet ), Int (Cl (Int KurExSet )) are_mutually_different
proof end;

theorem Th49: :: KURATO_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Cl KurExSet , Cl (Int KurExSet ), Cl (Int (Cl KurExSet )) are_mutually_different
proof end;

theorem Th50: :: KURATO_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :: KURATO_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th52: :: KURATO_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X in {(Int KurExSet ),(Int (Cl KurExSet )),(Int (Cl (Int KurExSet )))} holds
X <> REAL
proof end;

theorem :: KURATO_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X in {(Cl KurExSet ),(Cl (Int KurExSet )),(Cl (Int (Cl KurExSet )))} holds
X <> REAL
proof end;

theorem Th54: :: KURATO_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{(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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{(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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :: KURATO_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being with_proper_subsets with_non-empty_elements Subset-Family of R^1 st F is open & G is closed holds
F misses G
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th60;

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 Th62: :: KURATO_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
card (Kurat14ClPart KurExSet ) = 6
proof end;

theorem Th63: :: KURATO_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
card (Kurat14OpPart KurExSet ) = 6
proof end;

theorem Th64: :: KURATO_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
KurExSet <> KurExSet `
proof end;

theorem Th66: :: KURATO_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{KurExSet ,(KurExSet ` )} misses Kurat14OpPart KurExSet
proof end;

theorem :: KURATO_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 finite ;
coherence
not Kurat14Set A is empty by Th3;
cluster Kurat14Set A -> finite Cl-closed ;
coherence
Kurat14Set A is Cl-closed
proof end;
cluster Kurat14Set A -> finite 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 finite ;
coherence
not Kurat7Set A is empty by Th8;
cluster Kurat7Set A -> finite Int-closed ;
coherence
Kurat7Set A is Int-closed
proof end;
cluster Kurat7Set A -> finite Cl-closed ;
coherence
Kurat7Set A is Cl-closed
proof end;
end;

registration
let T be non empty TopSpace;
cluster non empty Cl-closed Int-closed Element of K10(K10(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 Element of K10(K10(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;