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