environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PRE_TOPC, SUBSET_1, ARYTM_1, TOPS_1, TARSKI, STRUCT_0, SETFAM_1, FINSET_1, ZFMISC_1, CARD_1, XXREAL_0, ARYTM_3, TOPMETR, XXREAL_1, BORSUK_5, RCOMP_1, PROB_1, KURATO_1;
notations HIDDEN, XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, PRE_TOPC, TOPS_1, ENUMSET1, FINSET_1, RCOMP_1, NAT_1, SEQ_4, TOPMETR, TOPS_2, BORSUK_5, PROB_1;
definitions TARSKI, ZFMISC_1, SETFAM_1, TOPS_2;
theorems ENUMSET1, TOPS_1, PRE_TOPC, CARD_2, XBOOLE_0, TDLAT_1, TARSKI, TOPMETR, ZFMISC_1, XBOOLE_1, SETFAM_1, MEASURE1, BORSUK_5, TOPS_2, PROB_1, XREAL_1, XXREAL_0, XXREAL_1, XREAL_0;
schemes ;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, XXREAL_0, MEMBERED, TOPS_1, TOPMETR, BORSUK_5, STRUCT_0;
constructors HIDDEN, PROB_1, RCOMP_1, TOPS_1, TOPS_2, TOPMETR, BORSUK_5, SEQ_4, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, ZFMISC_1, TOPS_2;
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 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 `) -) `) -) `) -) `)};
definition
let T be non
empty TopSpace;
let A be
Subset of
T;
coherence
{(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)} is Subset-Family of T
coherence
{((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T
end;
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 `)) `)) `)) `)}