REAL is non empty non trivial non finite non countable V208() V209() V210() V214() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal countable denumerable V208() V209() V210() V211() V212() V213() V214() Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is non empty non trivial ordinal non finite cardinal limit_cardinal countable denumerable V208() V209() V210() V211() V212() V213() V214() set
bool omega is non empty non trivial non finite set
K179() is non empty strict TopSpace-like TopStruct
the carrier of K179() is non empty set
COMPLEX is V208() V214() set
[:NAT,REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
RAT is countable V208() V209() V210() V211() V214() set
INT is V208() V209() V210() V211() V212() V214() set
bool NAT is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is Relation-like complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued complex-yielding V199() V200() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued complex-yielding V199() V200() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like RAT -valued INT -valued complex-yielding V199() V200() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued complex-yielding V199() V200() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-yielding V199() V200() V201() set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-yielding V199() V200() V201() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
[:1,1:] is non empty Relation-like RAT -valued INT -valued finite countable complex-yielding V199() V200() V201() set
bool [:1,1:] is non empty finite V32() countable set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued finite countable complex-yielding V199() V200() V201() set
bool [:[:1,1:],1:] is non empty finite V32() countable set
[:[:1,1:],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
2 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
[:2,2:] is non empty Relation-like RAT -valued INT -valued finite countable complex-yielding V199() V200() V201() set
[:[:2,2:],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
TOP-REAL 2 is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() L20()
the carrier of (TOP-REAL 2) is non empty set
{} is empty trivial Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element V83() real ext-real non positive non negative Cardinal-yielding countable integer complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() set
the empty trivial Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element V83() real ext-real non positive non negative Cardinal-yielding countable integer complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() set is empty trivial Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element V83() real ext-real non positive non negative Cardinal-yielding countable integer complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() set
0 is empty trivial Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element V83() real ext-real non positive non negative Cardinal-yielding countable integer V197() complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() Element of NAT
+infty is non empty non real ext-real positive non negative set
union {} is finite countable set
Euclid 1 is non empty strict Reflexive discerning V236() triangle MetrStruct
REAL 1 is non empty FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
Pitag_dist 1 is Relation-like [:(REAL 1),(REAL 1):] -defined REAL -valued Function-like V18([:(REAL 1),(REAL 1):], REAL ) complex-yielding V199() V200() Element of bool [:[:(REAL 1),(REAL 1):],REAL:]
[:(REAL 1),(REAL 1):] is non empty Relation-like set
[:[:(REAL 1),(REAL 1):],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[:(REAL 1),(REAL 1):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL 1),(Pitag_dist 1) #) is strict MetrStruct
the carrier of (Euclid 1) is non empty set
- 1 is V83() real ext-real non positive integer Element of REAL
n is set
bool n is non empty set
bool (bool n) is non empty set
n is set
bool n is non empty set
bool (bool n) is non empty set
TM is Element of bool (bool n)
cTM is Element of bool (bool n)
card cTM is ordinal cardinal set
meet cTM is Element of bool n
TM is Element of bool (bool n)
cTM is finite countable Element of bool (bool n)
card cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A1 is Element of bool (bool n)
card A1 is ordinal cardinal set
meet A1 is Element of bool n
card TM is ordinal cardinal set
n is set
bool n is non empty set
bool (bool n) is non empty set
TM is Element of bool (bool n)
cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
cTM - 1 is V83() real ext-real set
K194(cTM,1) is V83() real ext-real integer set
A is V83() real ext-real set
A + 1 is V83() real ext-real set
K190(A,1) is V83() real ext-real set
A1 is Element of bool (bool n)
card A1 is ordinal cardinal set
meet A1 is Element of bool n
A1 is Element of bool (bool n)
card A1 is ordinal cardinal set
meet A1 is Element of bool n
A1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A1 + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
card (A1 + 1) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card (card (A1 + 1)) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A2 is Element of bool (bool n)
card A2 is ordinal cardinal set
meet A2 is Element of bool n
card A1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card (card A1) is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
nextcard A1 is ordinal cardinal set
card cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A12 is Relation-like Function-like set
proj1 A12 is set
proj2 A12 is set
T912 is Element of bool (bool n)
card T912 is ordinal cardinal set
meet T912 is Element of bool n
A1 + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
cTM is V83() real ext-real set
cTM + 1 is V83() real ext-real set
K190(cTM,1) is V83() real ext-real set
A is Element of bool (bool n)
card A is ordinal cardinal set
meet A is Element of bool n
cTM is ext-real set
cTM + 1 is ext-real set
A is ext-real set
A + 1 is ext-real set
A1 is Element of bool (bool n)
card A1 is ordinal cardinal set
meet A1 is Element of bool n
A2 is Element of bool (bool n)
card A2 is ordinal cardinal set
meet A2 is Element of bool n
A1 is Element of bool (bool n)
card A1 is ordinal cardinal set
meet A1 is Element of bool n
A2 is Element of bool (bool n)
card A2 is ordinal cardinal set
meet A2 is Element of bool n
A12 is Element of bool (bool n)
card A12 is ordinal cardinal set
meet A12 is Element of bool n
T912 is Element of bool (bool n)
card T912 is ordinal cardinal set
meet T912 is Element of bool n
n is set
bool n is non empty set
bool (bool n) is non empty set
TM is (n) Element of bool (bool n)
(n,TM) is ext-real set
(n,TM) + 1 is ext-real set
cTM is Element of bool (bool n)
card cTM is ordinal cardinal set
meet cTM is Element of bool n
A is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
card A is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card (card A) is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A1 is finite countable (n) Element of bool (bool n)
card A1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
(card A1) - 1 is V83() real ext-real set
K194((card A1),1) is V83() real ext-real integer set
((card A1) - 1) + 1 is V83() real ext-real set
K190(((card A1) - 1),1) is V83() real ext-real set
cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
cTM - 1 is V83() real ext-real set
K194(cTM,1) is V83() real ext-real integer set
(cTM - 1) + 1 is V83() real ext-real set
K190((cTM - 1),1) is V83() real ext-real set
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TM is set
bool TM is non empty set
bool (bool TM) is non empty set
cTM is Element of bool (bool TM)
(TM,cTM) is ext-real set
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
n + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
TM is set
bool TM is non empty set
bool (bool TM) is non empty set
cTM is Element of bool (bool TM)
(TM,cTM) is ext-real set
card (n + 1) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card (card (n + 1)) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
n + 2 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
card (n + 2) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card (card (n + 2)) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A is (TM) Element of bool (bool TM)
(TM,A) is V83() real ext-real integer set
(TM,A) + 1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
K190((TM,A),1) is V83() real ext-real integer set
(n + 1) + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A1 is Element of bool (bool TM)
card A1 is ordinal cardinal set
meet A1 is Element of bool TM
nextcard (n + 1) is ordinal cardinal set
card ((n + 1) + 1) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
n + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
TM is set
bool TM is non empty set
bool (bool TM) is non empty set
cTM is Element of bool (bool TM)
(TM,cTM) is ext-real set
(n + 1) + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
card ((n + 1) + 1) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card (card ((n + 1) + 1)) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A1 is Element of bool (bool TM)
card A1 is ordinal cardinal set
card (n + 1) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card (card (n + 1)) is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
nextcard (n + 1) is ordinal cardinal set
A2 is Relation-like Function-like set
proj1 A2 is set
proj2 A2 is set
A12 is Element of bool (bool TM)
card A12 is ordinal cardinal set
T912 is finite countable (TM) Element of bool (bool TM)
card T912 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
meet T912 is Element of bool TM
meet A1 is Element of bool TM
A1 is (TM) Element of bool (bool TM)
(TM,A1) is V83() real ext-real integer set
(TM,A1) + 1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
K190((TM,A1),1) is V83() real ext-real integer set
A2 is Element of bool (bool TM)
card A2 is ordinal cardinal set
meet A2 is Element of bool TM
n is TopSpace-like TopStruct
the carrier of n is set
bool the carrier of n is non empty set
TM is with_finite_small_inductive_dimension Element of bool the carrier of n
ind TM is V83() real ext-real integer set
(ind TM) + 1 is V83() real ext-real set
K190((ind TM),1) is V83() real ext-real integer set
bool the carrier of n is non empty Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty set
Seq_of_ind n is Relation-like NAT -defined bool (bool the carrier of n) -valued Function-like V18( NAT , bool (bool the carrier of n)) non-descending Element of bool [:NAT,(bool (bool the carrier of n)):]
bool (bool the carrier of n) is non empty Element of bool (bool (bool the carrier of n))
bool (bool the carrier of n) is non empty set
bool (bool (bool the carrier of n)) is non empty set
[:NAT,(bool (bool the carrier of n)):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of n)):] is non empty non trivial non finite set
1 + (ind TM) is V83() real ext-real set
K190(1,(ind TM)) is V83() real ext-real integer set
(Seq_of_ind n) . (1 + (ind TM)) is Element of bool (bool the carrier of n)
dom (Seq_of_ind n) is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty Element of bool (bool the carrier of TM)
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
[:NAT,(bool the carrier of TM):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the carrier of TM):] is non empty non trivial non finite set
cTM is Relation-like NAT -defined bool the carrier of TM -valued Function-like V18( NAT , bool the carrier of TM) Element of bool [:NAT,(bool the carrier of TM):]
Union cTM is Element of bool the carrier of TM
proj2 cTM is set
union (proj2 cTM) is set
bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))
bool (bool the carrier of TM) is non empty set
bool (bool (bool the carrier of TM)) is non empty set
A is set
A1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
cTM . A1 is Element of bool the carrier of TM
A2 is closed countable Element of bool (bool the carrier of TM)
union A2 is Element of bool the carrier of TM
A12 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
T912 is Element of bool (bool the carrier of TM)
union T912 is Element of bool the carrier of TM
cTM . A12 is Element of bool the carrier of TM
[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set
A is Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V18( NAT , bool (bool the carrier of TM)) Element of bool [:NAT,(bool (bool the carrier of TM)):]
Union A is Element of bool (bool the carrier of TM)
proj2 A is set
union (proj2 A) is set
A1 is Element of bool (bool the carrier of TM)
ind A1 is V83() real ext-real integer set
union A1 is Element of bool the carrier of TM
A2 is Element of bool the carrier of TM
A12 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A . A12 is Element of bool (bool the carrier of TM)
A2 is Element of bool the carrier of TM
ind A2 is V83() real ext-real integer set
A12 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A . A12 is Element of bool (bool the carrier of TM)
union (A . A12) is Element of bool the carrier of TM
cTM . A12 is Element of bool the carrier of TM
ind (cTM . A12) is V83() real ext-real integer set
dom A is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
A2 is set
A . A2 is Element of bool (bool the carrier of TM)
A2 is set
A12 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
cTM . A12 is Element of bool the carrier of TM
A . A12 is Element of bool (bool the carrier of TM)
union (A . A12) is Element of bool the carrier of TM
T912 is set
A2 is set
A12 is set
T912 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A . T912 is Element of bool (bool the carrier of TM)
union (A . T912) is Element of bool the carrier of TM
cTM . T912 is Element of bool the carrier of TM
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
n - 1 is V83() real ext-real set
K194(n,1) is V83() real ext-real integer set
TM is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TM + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
(TM + 1) - 1 is V83() real ext-real set
K194((TM + 1),1) is V83() real ext-real integer set
cTM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
ind cTM is V83() real ext-real integer set
[#] cTM is non proper open closed F_sigma G_delta dense Element of bool the carrier of cTM
the carrier of cTM is set
bool the carrier of cTM is non empty set
ind ([#] cTM) is V83() real ext-real integer set
bool (bool the carrier of cTM) is non empty set
A is open V85(cTM) Element of bool (bool the carrier of cTM)
A1 is open V85(cTM) Element of bool (bool the carrier of cTM)
{ H1(b1) where b1 is Element of bool the carrier of cTM : S4[b1] } is set
A2 is Element of bool (bool the carrier of cTM)
union A2 is Element of bool the carrier of cTM
cTM | (union A2) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of cTM
[#] (cTM | (union A2)) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (cTM | (union A2))
the carrier of (cTM | (union A2)) is set
bool the carrier of (cTM | (union A2)) is non empty set
bool (bool the carrier of (cTM | (union A2))) is non empty set
(union A2) ` is Element of bool the carrier of cTM
the carrier of cTM \ (union A2) is set
cTM | ((union A2) `) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of cTM
A19 is Element of bool (bool the carrier of (cTM | (union A2)))
A29 is Element of bool the carrier of (cTM | (union A2))
ind A29 is V83() real ext-real integer set
A9 is Element of bool the carrier of cTM
Fr A9 is closed G_delta Element of bool the carrier of cTM
Cl A9 is closed G_delta Element of bool the carrier of cTM
A9 ` is Element of bool the carrier of cTM
the carrier of cTM \ A9 is set
Cl (A9 `) is closed G_delta Element of bool the carrier of cTM
(Cl A9) /\ (Cl (A9 `)) is closed G_delta Element of bool the carrier of cTM
ind (Fr A9) is V83() real ext-real integer set
ind A19 is V83() real ext-real integer set
A29 is Element of the carrier of cTM
A9 is open F_sigma Element of bool the carrier of cTM
A29 is Element of bool the carrier of cTM
the topology of cTM is non empty Element of bool (bool the carrier of cTM)
A19 is open F_sigma Element of bool the carrier of cTM
Fr A19 is closed G_delta boundary nowhere_dense Element of bool the carrier of cTM
Cl A19 is closed G_delta Element of bool the carrier of cTM
A19 ` is closed G_delta Element of bool the carrier of cTM
the carrier of cTM \ A19 is set
Cl (A19 `) is closed G_delta Element of bool the carrier of cTM
(Cl A19) /\ (Cl (A19 `)) is closed G_delta Element of bool the carrier of cTM
ind (union A2) is V83() real ext-real integer set
(union A2) \/ ((union A2) `) is Element of bool the carrier of cTM
ind ((union A2) `) is V83() real ext-real integer set
{ H1(b1) where b1 is Element of bool the carrier of cTM : ( b1 in A1 & S3[b1] ) } is set
card { H1(b1) where b1 is Element of bool the carrier of cTM : ( b1 in A1 & S3[b1] ) } is ordinal cardinal set
card A1 is ordinal cardinal set
card A2 is ordinal cardinal set
A29 is Element of bool the carrier of (cTM | (union A2))
A9 is Element of bool the carrier of cTM
Fr A9 is closed G_delta Element of bool the carrier of cTM
Cl A9 is closed G_delta Element of bool the carrier of cTM
A9 ` is Element of bool the carrier of cTM
the carrier of cTM \ A9 is set
Cl (A9 `) is closed G_delta Element of bool the carrier of cTM
(Cl A9) /\ (Cl (A9 `)) is closed G_delta Element of bool the carrier of cTM
ind (cTM | (union A2)) is V83() real ext-real integer set
ind ([#] (cTM | (union A2))) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
cTM is Element of bool (bool the carrier of TM)
ind cTM is V83() real ext-real integer set
ind TM is V83() real ext-real integer set
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
ind ([#] TM) is V83() real ext-real integer set
TM is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TM + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
cTM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of cTM is set
bool the carrier of cTM is non empty set
bool (bool the carrier of cTM) is non empty set
ind cTM is V83() real ext-real integer set
[#] cTM is non proper open closed F_sigma G_delta dense Element of bool the carrier of cTM
ind ([#] cTM) is V83() real ext-real integer set
A is Element of bool (bool the carrier of cTM)
ind A is V83() real ext-real integer set
[:NAT,A:] is Relation-like set
bool [:NAT,A:] is non empty set
A2 is Relation-like NAT -defined A -valued Function-like V18( NAT ,A) Element of bool [:NAT,A:]
rng A2 is Element of bool A
bool A is non empty set
dom A2 is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
bool the carrier of cTM is non empty Element of bool (bool the carrier of cTM)
[:NAT,(bool the carrier of cTM):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the carrier of cTM):] is non empty non trivial non finite set
A12 is Relation-like NAT -defined bool the carrier of cTM -valued Function-like V18( NAT , bool the carrier of cTM) Element of bool [:NAT,(bool the carrier of cTM):]
rng A12 is Element of bool (bool the carrier of cTM)
bool (bool the carrier of cTM) is non empty set
union (rng A12) is Element of bool the carrier of cTM
T912 is Relation-like NAT -defined bool the carrier of cTM -valued Function-like V18( NAT , bool the carrier of cTM) Element of bool [:NAT,(bool the carrier of cTM):]
rng T912 is Element of bool (bool the carrier of cTM)
union (rng T912) is Element of bool the carrier of cTM
[:(bool the carrier of cTM),(bool the carrier of cTM):] is non empty Relation-like set
A19 is set
A29 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
T912 . A29 is Element of bool the carrier of cTM
dom A12 is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
A12 . A29 is Element of bool the carrier of cTM
{ (A12 . b1) where b1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT : not A29 <= b1 } is set
A29 is finite countable ( the carrier of cTM) Element of bool (bool the carrier of cTM)
union A29 is Element of bool the carrier of cTM
(A12 . A29) \ (union A29) is Element of bool the carrier of cTM
ind (T912 . A29) is V83() real ext-real integer set
ind (A12 . A29) is V83() real ext-real integer set
A9 is Element of bool the carrier of cTM
cTM | A9 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of cTM
ind (cTM | A9) is V83() real ext-real integer set
[#] (cTM | A9) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (cTM | A9)
the carrier of (cTM | A9) is set
bool the carrier of (cTM | A9) is non empty set
ind ([#] (cTM | A9)) is V83() real ext-real integer set
ind A9 is V83() real ext-real integer set
(TM + 1) - 1 is V83() real ext-real set
K194((TM + 1),1) is V83() real ext-real integer set
A29 is Element of bool the carrier of (cTM | A9)
A19 is Element of bool the carrier of (cTM | A9)
A29 \/ A19 is Element of bool the carrier of (cTM | A9)
ind A29 is V83() real ext-real integer set
ind A19 is V83() real ext-real integer set
U is Element of bool the carrier of cTM
ind U is V83() real ext-real integer set
[:(bool the carrier of cTM),(bool the carrier of cTM):] is non empty Relation-like set
L is Element of bool the carrier of cTM
[L,U] is non empty V15() Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
{L,U} is non empty finite countable set
{L} is non empty trivial finite 1 -element countable set
{{L,U},{L}} is non empty finite V32() countable set
W is non empty V15() Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
L9 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
T912 . L9 is Element of bool the carrier of cTM
U9 is Element of bool the carrier of cTM
W9 is Element of bool the carrier of cTM
[U9,W9] is non empty V15() Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
{U9,W9} is non empty finite countable set
{U9} is non empty trivial finite 1 -element countable set
{{U9,W9},{U9}} is non empty finite V32() countable set
U9 \/ W9 is Element of bool the carrier of cTM
ind U9 is V83() real ext-real integer set
ind W9 is V83() real ext-real integer set
L \/ U is Element of bool the carrier of cTM
[:NAT,[:(bool the carrier of cTM),(bool the carrier of cTM):]:] is non empty non trivial Relation-like non finite set
bool [:NAT,[:(bool the carrier of cTM),(bool the carrier of cTM):]:] is non empty non trivial non finite set
A19 is Relation-like NAT -defined [:(bool the carrier of cTM),(bool the carrier of cTM):] -valued Function-like V18( NAT ,[:(bool the carrier of cTM),(bool the carrier of cTM):]) Element of bool [:NAT,[:(bool the carrier of cTM),(bool the carrier of cTM):]:]
pr1 A19 is Relation-like NAT -defined bool the carrier of cTM -valued Function-like V18( NAT , bool the carrier of cTM) Element of bool [:NAT,(bool the carrier of cTM):]
pr2 A19 is Relation-like NAT -defined bool the carrier of cTM -valued Function-like V18( NAT , bool the carrier of cTM) Element of bool [:NAT,(bool the carrier of cTM):]
Union (pr1 A19) is Element of bool the carrier of cTM
proj2 (pr1 A19) is set
union (proj2 (pr1 A19)) is set
Union (pr2 A19) is Element of bool the carrier of cTM
proj2 (pr2 A19) is set
union (proj2 (pr2 A19)) is set
cTM | (Union (pr1 A19)) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of cTM
cTM | (Union (pr2 A19)) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of cTM
dom (pr1 A19) is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
W is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
[#] W is non proper open closed F_sigma G_delta dense Element of bool the carrier of W
the carrier of W is set
bool the carrier of W is non empty set
bool the carrier of W is non empty Element of bool (bool the carrier of W)
bool (bool the carrier of W) is non empty set
[:NAT,(bool the carrier of W):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the carrier of W):] is non empty non trivial non finite set
dom (pr2 A19) is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
W9 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
T912 . W9 is Element of bool the carrier of cTM
{ (A12 . b1) where b1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT : not W9 <= b1 } is set
A12 . W9 is Element of bool the carrier of cTM
U9 is finite countable ( the carrier of cTM) Element of bool (bool the carrier of cTM)
union U9 is Element of bool the carrier of cTM
(A12 . W9) \ (union U9) is Element of bool the carrier of cTM
W9 is Element of bool the carrier of cTM
dom A12 is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
X2 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A12 . X2 is Element of bool the carrier of cTM
dom A12 is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
(union U9) ` is Element of bool the carrier of cTM
the carrier of cTM \ (union U9) is set
((union U9) `) /\ (A12 . W9) is Element of bool the carrier of cTM
([#] cTM) /\ (A12 . W9) is Element of bool the carrier of cTM
(([#] cTM) /\ (A12 . W9)) \ (union U9) is Element of bool the carrier of cTM
L9 is Relation-like NAT -defined bool the carrier of W -valued Function-like V18( NAT , bool the carrier of W) Element of bool [:NAT,(bool the carrier of W):]
W9 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
L9 . W9 is Element of bool the carrier of W
ind (L9 . W9) is V83() real ext-real integer set
A19 . W9 is Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
U9 is set
W9 is set
[U9,W9] is non empty V15() set
{U9,W9} is non empty finite countable set
{U9} is non empty trivial finite 1 -element countable set
{{U9,W9},{U9}} is non empty finite V32() countable set
X2 is Element of bool the carrier of cTM
ind X2 is V83() real ext-real integer set
[X2,W9] is non empty V15() set
{X2,W9} is non empty finite countable set
{X2} is non empty trivial finite 1 -element countable set
{{X2,W9},{X2}} is non empty finite V32() countable set
[X2,W9] `1 is set
dom A19 is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
T912 . W9 is Element of bool the carrier of cTM
(Union (pr1 A19)) /\ (T912 . W9) is Element of bool the carrier of cTM
X1 is set
gV1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
L9 . gV1 is Element of bool the carrier of W
A19 . gV1 is Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
gV2 is set
h is set
[gV2,h] is non empty V15() set
{gV2,h} is non empty finite countable set
{gV2} is non empty trivial finite 1 -element countable set
{{gV2,h},{gV2}} is non empty finite V32() countable set
[gV2,h] `1 is set
gV2 \/ h is set
T912 . gV1 is Element of bool the carrier of cTM
X2 \/ W9 is set
Union L9 is Element of bool the carrier of W
proj2 L9 is set
union (proj2 L9) is set
W9 is Element of bool (bool the carrier of W)
ind W9 is V83() real ext-real integer set
union W9 is Element of bool the carrier of W
U9 is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
[#] U9 is non proper open closed F_sigma G_delta dense Element of bool the carrier of U9
the carrier of U9 is set
bool the carrier of U9 is non empty set
bool the carrier of U9 is non empty Element of bool (bool the carrier of U9)
bool (bool the carrier of U9) is non empty set
[:NAT,(bool the carrier of U9):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool the carrier of U9):] is non empty non trivial non finite set
U9 is Relation-like NAT -defined bool the carrier of U9 -valued Function-like V18( NAT , bool the carrier of U9) Element of bool [:NAT,(bool the carrier of U9):]
W9 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
U9 . W9 is Element of bool the carrier of U9
ind (U9 . W9) is V83() real ext-real integer set
A19 . W9 is Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
X2 is set
X1 is set
[X2,X1] is non empty V15() set
{X2,X1} is non empty finite countable set
{X2} is non empty trivial finite 1 -element countable set
{{X2,X1},{X2}} is non empty finite V32() countable set
gV1 is Element of bool the carrier of cTM
ind gV1 is V83() real ext-real integer set
[X2,gV1] is non empty V15() set
{X2,gV1} is non empty finite countable set
{{X2,gV1},{X2}} is non empty finite V32() countable set
[X2,gV1] `2 is set
dom A19 is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
T912 . W9 is Element of bool the carrier of cTM
(Union (pr2 A19)) /\ (T912 . W9) is Element of bool the carrier of cTM
gV2 is set
h is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
U9 . h is Element of bool the carrier of U9
A19 . h is Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
gh is set
a is set
[gh,a] is non empty V15() set
{gh,a} is non empty finite countable set
{gh} is non empty trivial finite 1 -element countable set
{{gh,a},{gh}} is non empty finite V32() countable set
[gh,a] `2 is set
gh \/ a is set
T912 . h is Element of bool the carrier of cTM
X2 \/ gV1 is set
Union U9 is Element of bool the carrier of U9
proj2 U9 is set
union (proj2 U9) is set
W9 is Element of bool (bool the carrier of U9)
ind W9 is V83() real ext-real integer set
union W9 is Element of bool the carrier of U9
ind W is V83() real ext-real integer set
ind ([#] W) is V83() real ext-real integer set
ind (Union (pr1 A19)) is V83() real ext-real integer set
(ind (Union (pr1 A19))) + 1 is V83() real ext-real set
K190((ind (Union (pr1 A19))),1) is V83() real ext-real integer set
(Union (pr1 A19)) \/ (Union (pr2 A19)) is Element of bool the carrier of cTM
X2 is set
dom A19 is countable V208() V209() V210() V211() V212() V213() Element of bool NAT
Union T912 is Element of bool the carrier of cTM
proj2 T912 is set
union (proj2 T912) is set
X1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
T912 . X1 is Element of bool the carrier of cTM
A19 . X1 is Element of [:(bool the carrier of cTM),(bool the carrier of cTM):]
gV1 is set
gV2 is set
[gV1,gV2] is non empty V15() set
{gV1,gV2} is non empty finite countable set
{gV1} is non empty trivial finite 1 -element countable set
{{gV1,gV2},{gV1}} is non empty finite V32() countable set
[gV1,gV2] `1 is set
L9 . X1 is Element of bool the carrier of W
[gV1,gV2] `2 is set
U9 . X1 is Element of bool the carrier of U9
gV1 \/ gV2 is set
ind U9 is V83() real ext-real integer set
ind ([#] U9) is V83() real ext-real integer set
ind (Union (pr2 A19)) is V83() real ext-real integer set
ind ((Union (pr1 A19)) \/ (Union (pr2 A19))) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
ind TM is V83() real ext-real integer set
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
ind ([#] TM) is V83() real ext-real integer set
cTM is Element of bool (bool the carrier of TM)
ind cTM is V83() real ext-real integer set
{} TM is empty trivial Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element open closed V83() real ext-real non positive non negative Cardinal-yielding countable F_sigma G_delta boundary nowhere_dense integer complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() with_finite_small_inductive_dimension Element of bool the carrier of TM
ind ({} TM) is V83() real ext-real integer set
({} TM) \/ ([#] TM) is open closed F_sigma G_delta Element of bool the carrier of TM
cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
cTM + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of A is set
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
A1 is Element of bool (bool the carrier of A)
ind A1 is V83() real ext-real integer set
ind A is V83() real ext-real integer set
[#] A is non proper open closed F_sigma G_delta dense Element of bool the carrier of A
ind ([#] A) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
cTM is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
ind cTM is V83() real ext-real integer set
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
ind TM is V83() real ext-real integer set
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
ind ([#] TM) is V83() real ext-real integer set
n is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of n is set
bool the carrier of n is non empty set
TM is V83() real ext-real integer set
cTM is with_finite_small_inductive_dimension Element of bool the carrier of n
A is with_finite_small_inductive_dimension Element of bool the carrier of n
cTM \/ A is Element of bool the carrier of n
n | (cTM \/ A) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
ind cTM is V83() real ext-real integer set
ind A is V83() real ext-real integer set
ind (cTM \/ A) is V83() real ext-real integer set
- 1 is non empty V83() real ext-real non positive negative set
K192(1) is V83() real ext-real non positive integer set
A1 is Element of bool the carrier of n
n | A1 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
[#] (n | A1) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (n | A1)
the carrier of (n | A1) is set
bool the carrier of (n | A1) is non empty set
cTM /\ ([#] (n | A1)) is Element of bool the carrier of (n | A1)
A12 is Element of bool the carrier of (n | A1)
bool (bool the carrier of (n | A1)) is non empty set
A12 ` is Element of bool the carrier of (n | A1)
the carrier of (n | A1) \ A12 is set
A19 is closed countable Element of bool (bool the carrier of (n | A1))
union A19 is Element of bool the carrier of (n | A1)
T912 is Element of bool the carrier of (n | A1)
A29 is with_finite_small_inductive_dimension Element of bool the carrier of (n | A1)
{A29} is non empty trivial finite 1 -element countable ( the carrier of (n | A1)) Element of bool (bool the carrier of (n | A1))
A29 is Element of bool (bool the carrier of (n | A1))
A29 \/ A19 is Element of bool (bool the carrier of (n | A1))
union (A29 \/ A19) is Element of bool the carrier of (n | A1)
union A29 is Element of bool the carrier of (n | A1)
(union A29) \/ (union A19) is Element of bool the carrier of (n | A1)
A29 ` is Element of bool the carrier of (n | A1)
the carrier of (n | A1) \ A29 is set
A29 \/ (A29 `) is Element of bool the carrier of (n | A1)
A19 is Element of bool the carrier of (n | A1)
A19 is Element of bool the carrier of (n | A1)
ind A19 is V83() real ext-real integer set
A9 is with_finite_small_inductive_dimension Element of bool the carrier of (n | A1)
A9 \ A29 is Element of bool the carrier of (n | A1)
ind A9 is V83() real ext-real integer set
ind (A29 \/ A19) is V83() real ext-real integer set
ind (n | A1) is V83() real ext-real integer set
ind ([#] (n | A1)) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
ind TM is V83() real ext-real integer set
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
the carrier of TM is set
bool the carrier of TM is non empty set
ind ([#] TM) is V83() real ext-real integer set
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
n - 1 is V83() real ext-real set
K194(n,1) is V83() real ext-real integer set
n is V83() real ext-real integer set
n + 1 is V83() real ext-real set
K190(n,1) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
ind TM is V83() real ext-real integer set
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
the carrier of TM is set
bool the carrier of TM is non empty set
ind ([#] TM) is V83() real ext-real integer set
bool (bool the carrier of TM) is non empty set
- 1 is non empty V83() real ext-real non positive negative set
K192(1) is V83() real ext-real non positive integer set
(- 1) + 1 is V83() real ext-real set
K190((- 1),1) is V83() real ext-real set
A is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
A - 1 is V83() real ext-real set
K194(A,1) is V83() real ext-real integer set
A + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
(A + 1) - 1 is V83() real ext-real set
K194((A + 1),1) is V83() real ext-real integer set
A1 is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
ind A1 is V83() real ext-real integer set
[#] A1 is non proper open closed F_sigma G_delta dense Element of bool the carrier of A1
the carrier of A1 is set
bool the carrier of A1 is non empty set
ind ([#] A1) is V83() real ext-real integer set
bool (bool the carrier of A1) is non empty set
A2 is Element of bool the carrier of A1
A12 is Element of bool the carrier of A1
A2 \/ A12 is Element of bool the carrier of A1
ind A2 is V83() real ext-real integer set
ind A12 is V83() real ext-real integer set
{A12} is non empty trivial finite 1 -element countable ( the carrier of A1) Element of bool (bool the carrier of A1)
A19 is Element of bool the carrier of A1
ind A19 is V83() real ext-real integer set
ind {A12} is V83() real ext-real integer set
A1 | A2 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of A1
ind (A1 | A2) is V83() real ext-real integer set
[#] (A1 | A2) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (A1 | A2)
the carrier of (A1 | A2) is set
bool the carrier of (A1 | A2) is non empty set
ind ([#] (A1 | A2)) is V83() real ext-real integer set
bool (bool the carrier of (A1 | A2)) is non empty set
A29 is finite countable ( the carrier of (A1 | A2)) Element of bool (bool the carrier of (A1 | A2))
ind A29 is V83() real ext-real integer set
card A29 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
bool ([#] (A1 | A2)) is non empty Element of bool (bool ([#] (A1 | A2)))
bool ([#] (A1 | A2)) is non empty set
bool (bool ([#] (A1 | A2))) is non empty set
bool ([#] A1) is non empty Element of bool (bool ([#] A1))
bool ([#] A1) is non empty set
bool (bool ([#] A1)) is non empty set
A9 is finite countable ( the carrier of A1) Element of bool (bool the carrier of A1)
A9 \/ {A12} is non empty finite countable ( the carrier of A1) Element of bool (bool the carrier of A1)
A29 is non empty finite countable ( the carrier of A1) Element of bool (bool the carrier of A1)
ind A29 is V83() real ext-real integer set
card A29 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
union A9 is Element of bool the carrier of A1
union A29 is Element of bool the carrier of A1
union {A12} is Element of bool the carrier of A1
A2 \/ (union {A12}) is Element of bool the carrier of A1
ind A9 is V83() real ext-real integer set
card {A12} is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card A9 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
(card A9) + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A19 is Element of bool the carrier of A1
L is Element of bool the carrier of A1
0 - 1 is non empty V83() real ext-real non positive negative set
K194(0,1) is non empty V83() real ext-real non positive negative integer set
A is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
ind A is V83() real ext-real integer set
[#] A is non proper open closed F_sigma G_delta dense Element of bool the carrier of A
the carrier of A is set
bool the carrier of A is non empty set
ind ([#] A) is V83() real ext-real integer set
bool (bool the carrier of A) is non empty set
{} A is empty trivial Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element open closed V83() real ext-real non positive non negative Cardinal-yielding countable F_sigma G_delta boundary nowhere_dense integer complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() with_finite_small_inductive_dimension Element of bool the carrier of A
A1 is empty trivial proper Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element open closed V83() real ext-real non positive non negative Cardinal-yielding countable integer complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() with_finite_small_inductive_dimension ( the carrier of A) Element of bool (bool the carrier of A)
ind A1 is V83() real ext-real integer set
card A1 is empty trivial Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ordinal natural finite finite-yielding V32() cardinal {} -element V83() real ext-real non positive non negative Cardinal-yielding countable integer V197() complex-yielding V199() V200() V201() V202() V203() V204() V205() V208() V209() V210() V211() V212() V213() V214() Element of omega
{({} A)} is non empty trivial functional finite V32() 1 -element with_common_domain countable V208() V209() V210() V211() V212() V213() ( the carrier of A) Element of bool (bool the carrier of A)
A2 is Element of bool the carrier of A
A12 is Element of bool the carrier of A
cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
cTM - 1 is V83() real ext-real set
K194(cTM,1) is V83() real ext-real integer set
A is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
ind A is V83() real ext-real integer set
[#] A is non proper open closed F_sigma G_delta dense Element of bool the carrier of A
the carrier of A is set
bool the carrier of A is non empty set
ind ([#] A) is V83() real ext-real integer set
bool (bool the carrier of A) is non empty set
n is V83() real ext-real integer set
n + 1 is V83() real ext-real set
K190(n,1) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
bool (bool the carrier of TM) is non empty set
ind TM is V83() real ext-real integer set
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
ind ([#] TM) is V83() real ext-real integer set
cTM is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
ind cTM is V83() real ext-real integer set
card cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
0 - 1 is non empty V83() real ext-real non positive negative set
K194(0,1) is non empty V83() real ext-real non positive negative integer set
A1 is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of A1 is set
bool the carrier of A1 is non empty set
bool (bool the carrier of A1) is non empty set
ind A1 is V83() real ext-real integer set
[#] A1 is non proper open closed F_sigma G_delta dense Element of bool the carrier of A1
ind ([#] A1) is V83() real ext-real integer set
A2 is finite countable ( the carrier of A1) Element of bool (bool the carrier of A1)
ind A2 is V83() real ext-real integer set
card A2 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A1 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
A1 - 1 is V83() real ext-real set
K194(A1,1) is V83() real ext-real integer set
A1 + 1 is non empty ordinal natural finite cardinal V83() real ext-real positive non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
(A1 + 1) - 1 is V83() real ext-real set
K194((A1 + 1),1) is V83() real ext-real integer set
A2 is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of A2 is set
bool the carrier of A2 is non empty set
bool (bool the carrier of A2) is non empty set
ind A2 is V83() real ext-real integer set
[#] A2 is non proper open closed F_sigma G_delta dense Element of bool the carrier of A2
ind ([#] A2) is V83() real ext-real integer set
A12 is finite countable ( the carrier of A2) Element of bool (bool the carrier of A2)
ind A12 is V83() real ext-real integer set
card A12 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
T912 is set
A19 is Element of bool the carrier of A2
{A19} is non empty trivial finite 1 -element countable ( the carrier of A2) Element of bool (bool the carrier of A2)
A12 \ {A19} is finite countable ( the carrier of A2) Element of bool (bool the carrier of A2)
(A12 \ {A19}) \/ {A19} is non empty finite countable ( the carrier of A2) Element of bool (bool the carrier of A2)
union A12 is Element of bool the carrier of A2
union (A12 \ {A19}) is Element of bool the carrier of A2
union {A19} is Element of bool the carrier of A2
(union (A12 \ {A19})) \/ (union {A19}) is Element of bool the carrier of A2
(union (A12 \ {A19})) \/ A19 is Element of bool the carrier of A2
ind (A12 \ {A19}) is V83() real ext-real integer set
card (A12 \ {A19}) is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
A29 is Element of bool the carrier of A2
A2 | A29 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of A2
[#] (A2 | A29) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (A2 | A29)
the carrier of (A2 | A29) is set
bool the carrier of (A2 | A29) is non empty set
bool (bool the carrier of (A2 | A29)) is non empty set
A2 | A19 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of A2
L is Element of bool (bool the carrier of (A2 | A29))
ind L is V83() real ext-real integer set
ind (A2 | A29) is V83() real ext-real integer set
ind ([#] (A2 | A29)) is V83() real ext-real integer set
ind A29 is V83() real ext-real integer set
(ind A29) + 1 is V83() real ext-real set
K190((ind A29),1) is V83() real ext-real integer set
(A1 - 1) + 1 is V83() real ext-real set
K190((A1 - 1),1) is V83() real ext-real set
ind A19 is V83() real ext-real integer set
A is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A - 1 is V83() real ext-real set
K194(A,1) is V83() real ext-real integer set
A1 is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of A1 is set
bool the carrier of A1 is non empty set
bool (bool the carrier of A1) is non empty set
A2 is finite countable ( the carrier of A1) Element of bool (bool the carrier of A1)
ind A2 is V83() real ext-real integer set
card A2 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
ind A1 is V83() real ext-real integer set
[#] A1 is non proper open closed F_sigma G_delta dense Element of bool the carrier of A1
ind ([#] A1) is V83() real ext-real integer set
n is TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable TopStruct
the carrier of n is set
bool the carrier of n is non empty set
TM is Element of bool the carrier of n
ind TM is V83() real ext-real integer set
cTM is Element of bool the carrier of n
TM \/ cTM is Element of bool the carrier of n
n | (TM \/ cTM) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
ind (TM \/ cTM) is V83() real ext-real integer set
ind cTM is V83() real ext-real integer set
(ind TM) + (ind cTM) is V83() real ext-real set
K190((ind TM),(ind cTM)) is V83() real ext-real integer set
((ind TM) + (ind cTM)) + 1 is V83() real ext-real set
K190(((ind TM) + (ind cTM)),1) is V83() real ext-real set
[#] (n | (TM \/ cTM)) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (n | (TM \/ cTM))
the carrier of (n | (TM \/ cTM)) is set
bool the carrier of (n | (TM \/ cTM)) is non empty set
A2 is Element of bool the carrier of (n | (TM \/ cTM))
(n | (TM \/ cTM)) | A2 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n | (TM \/ cTM)
ind ((n | (TM \/ cTM)) | A2) is V83() real ext-real integer set
[#] ((n | (TM \/ cTM)) | A2) is non proper open closed F_sigma G_delta dense Element of bool the carrier of ((n | (TM \/ cTM)) | A2)
the carrier of ((n | (TM \/ cTM)) | A2) is set
bool the carrier of ((n | (TM \/ cTM)) | A2) is non empty set
ind ([#] ((n | (TM \/ cTM)) | A2)) is V83() real ext-real integer set
ind A2 is V83() real ext-real integer set
A12 is Element of bool the carrier of (n | (TM \/ cTM))
(n | (TM \/ cTM)) | A12 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n | (TM \/ cTM)
[#] ((n | (TM \/ cTM)) | A12) is non proper open closed F_sigma G_delta dense Element of bool the carrier of ((n | (TM \/ cTM)) | A12)
the carrier of ((n | (TM \/ cTM)) | A12) is set
bool the carrier of ((n | (TM \/ cTM)) | A12) is non empty set
bool ([#] ((n | (TM \/ cTM)) | A12)) is non empty Element of bool (bool ([#] ((n | (TM \/ cTM)) | A12)))
bool ([#] ((n | (TM \/ cTM)) | A12)) is non empty set
bool (bool ([#] ((n | (TM \/ cTM)) | A12))) is non empty set
bool ([#] (n | (TM \/ cTM))) is non empty Element of bool (bool ([#] (n | (TM \/ cTM))))
bool ([#] (n | (TM \/ cTM))) is non empty set
bool (bool ([#] (n | (TM \/ cTM)))) is non empty set
bool (bool the carrier of ((n | (TM \/ cTM)) | A12)) is non empty set
ind ((n | (TM \/ cTM)) | A12) is V83() real ext-real integer set
ind ([#] ((n | (TM \/ cTM)) | A12)) is V83() real ext-real integer set
(ind ((n | (TM \/ cTM)) | A12)) + 1 is V83() real ext-real set
K190((ind ((n | (TM \/ cTM)) | A12)),1) is V83() real ext-real integer set
T912 is finite countable ( the carrier of ((n | (TM \/ cTM)) | A12)) Element of bool (bool the carrier of ((n | (TM \/ cTM)) | A12))
ind T912 is V83() real ext-real integer set
card T912 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
bool (bool the carrier of ((n | (TM \/ cTM)) | A2)) is non empty set
(ind ((n | (TM \/ cTM)) | A2)) + 1 is V83() real ext-real set
K190((ind ((n | (TM \/ cTM)) | A2)),1) is V83() real ext-real integer set
A19 is finite countable ( the carrier of ((n | (TM \/ cTM)) | A2)) Element of bool (bool the carrier of ((n | (TM \/ cTM)) | A2))
ind A19 is V83() real ext-real integer set
card A19 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
bool ([#] ((n | (TM \/ cTM)) | A2)) is non empty Element of bool (bool ([#] ((n | (TM \/ cTM)) | A2)))
bool ([#] ((n | (TM \/ cTM)) | A2)) is non empty set
bool (bool ([#] ((n | (TM \/ cTM)) | A2))) is non empty set
bool (bool the carrier of (n | (TM \/ cTM))) is non empty set
A9 is finite countable ( the carrier of (n | (TM \/ cTM))) Element of bool (bool the carrier of (n | (TM \/ cTM)))
ind A12 is V83() real ext-real integer set
A29 is finite countable ( the carrier of (n | (TM \/ cTM))) Element of bool (bool the carrier of (n | (TM \/ cTM)))
A29 \/ A9 is finite countable ( the carrier of (n | (TM \/ cTM))) Element of bool (bool the carrier of (n | (TM \/ cTM)))
card (A29 \/ A9) is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card A29 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
card A9 is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of omega
(card A29) + (card A9) is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
(ind TM) + 1 is V83() real ext-real set
K190((ind TM),1) is V83() real ext-real integer set
(ind cTM) + 1 is V83() real ext-real set
K190((ind cTM),1) is V83() real ext-real integer set
((