begin
theorem Th1:
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
{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 - ) ` ) - ) ` ) - ) ` )};
definition
let T be non
empty TopSpace;
let A be
Subset of
T;
func Kurat14Set A -> Subset-Family of
T equals
{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
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
theorem Th3:
theorem Th4:
definition
let T be non
empty TopSpace;
let A be
Subset of
T;
func Kurat14ClPart A -> Subset-Family of
T equals
{(A - ),(((A - ) ` ) - ),(((((A - ) ` ) - ) ` ) - ),((A ` ) - ),((((A ` ) - ) ` ) - ),((((((A ` ) - ) ` ) - ) ` ) - )};
coherence
{(A - ),(((A - ) ` ) - ),(((((A - ) ` ) - ) ` ) - ),((A ` ) - ),((((A ` ) - ) ` ) - ),((((((A ` ) - ) ` ) - ) ` ) - )} is Subset-Family of T
func Kurat14OpPart A -> Subset-Family of
T equals
{((A - ) ` ),((((A - ) ` ) - ) ` ),((((((A - ) ` ) - ) ` ) - ) ` ),(((A ` ) - ) ` ),(((((A ` ) - ) ` ) - ) ` ),(((((((A ` ) - ) ` ) - ) ` ) - ) ` )};
coherence
{((A - ) ` ),((((A - ) ` ) - ) ` ),((((((A - ) ` ) - ) ` ) - ) ` ),(((A ` ) - ) ` ),(((((A ` ) - ) ` ) - ) ` ),(((((((A ` ) - ) ` ) - ) ` ) - ) ` )} is Subset-Family of T
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 ` )) ` )) ` )) ` )}
theorem
theorem Th6:
theorem
begin
definition
let T be non
empty TopSpace;
let A be
Subset of
T;
func Kurat7Set A -> Subset-Family of
T equals
{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
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
canceled;
theorem
theorem Th10:
begin
:: deftheorem defines KurExSet KURATO_1:def 6 :
KurExSet = (({1} \/ (RAT 2,4)) \/ ].4,5.[) \/ ].5,+infty .[;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
begin
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
theorem
theorem Th31:
theorem
theorem Th33:
theorem
theorem
theorem
theorem
theorem Th38:
theorem
theorem Th40:
theorem
theorem Th42:
theorem Th43:
theorem
theorem Th45:
theorem
begin
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
canceled;
theorem Th52:
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem
begin
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
begin
:: 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 );