TOPDIM_2

:: TOPDIM_2 semantic presentation

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)
{ H₁(b₁) where b₁ is Element of bool the carrier of cTM : S₄[b₁] } 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
{ H₁(b₁) where b₁ is Element of bool the carrier of cTM : ( b₁ in A1 & S₃[b₁] ) } is set
card { H₁(b₁) where b₁ is Element of bool the carrier of cTM : ( b₁ in A1 & S₃[b₁] ) } 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 . b₁) where b₁ 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 <= b₁ } 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 . b₁) where b₁ 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 <= b₁ } 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
((ind TM) + 1) + ((ind cTM) + 1) is V83() real ext-real set
K190(((ind TM) + 1),((ind cTM) + 1)) is V83() real ext-real set
((ind TM) + 1) + (ind cTM) is V83() real ext-real set
K190(((ind TM) + 1),(ind cTM)) is V83() real ext-real set
(((ind TM) + 1) + (ind cTM)) + 1 is V83() real ext-real set
K190((((ind TM) + 1) + (ind cTM)),1) is V83() real ext-real set
union (A29 \/ A9) is Element of bool the carrier of (n | (TM \/ cTM))
union A19 is Element of bool the carrier of ((n | (TM \/ cTM)) | A2)
union T912 is Element of bool the carrier of ((n | (TM \/ cTM)) | A12)
(union A19) \/ (union T912) is set
([#] ((n | (TM \/ cTM)) | A2)) \/ (union T912) is set
([#] ((n | (TM \/ cTM)) | A2)) \/ ([#] ((n | (TM \/ cTM)) | A12)) is set
A2 \/ ([#] ((n | (TM \/ cTM)) | A12)) is set
A2 \/ A12 is Element of bool the carrier of (n | (TM \/ cTM))
ind A9 is V83() real ext-real integer set
ind A29 is V83() real ext-real integer set
ind (A29 \/ A9) is V83() real ext-real integer set
ind (n | (TM \/ cTM)) is V83() real ext-real integer set
ind ([#] (n | (TM \/ cTM))) is V83() real ext-real integer set
n is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable 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
cTM is with_finite_small_inductive_dimension 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 second-countable Lindelof metrizable SubSpace of n
A is Element of bool the carrier of n
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
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 TM 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 is TopSpace-like TopStruct
the carrier of n is set
bool the carrier of n is non empty set
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
[:n,TM:] is strict TopSpace-like TopStruct
the carrier of [:n,TM:] is set
cTM is Element of bool the carrier of n
Fr cTM is closed Element of bool the carrier of n
Cl cTM is closed Element of bool the carrier of n
cTM ` is Element of bool the carrier of n
the carrier of n \ cTM is set
Cl (cTM `) is closed Element of bool the carrier of n
(Cl cTM) /\ (Cl (cTM `)) is closed Element of bool the carrier of n
A is Element of bool the carrier of TM
[:cTM,A:] is Relation-like Element of bool the carrier of [:n,TM:]
bool the carrier of [:n,TM:] is non empty set
Fr [:cTM,A:] is closed Element of bool the carrier of [:n,TM:]
Cl [:cTM,A:] is closed Element of bool the carrier of [:n,TM:]
[:cTM,A:] ` is Element of bool the carrier of [:n,TM:]
the carrier of [:n,TM:] \ [:cTM,A:] is set
Cl ([:cTM,A:] `) is closed Element of bool the carrier of [:n,TM:]
(Cl [:cTM,A:]) /\ (Cl ([:cTM,A:] `)) is closed Element of bool the carrier of [:n,TM:]
Cl A is closed Element of bool the carrier of TM
[:(Fr cTM),(Cl A):] is Relation-like Element of bool the carrier of [:n,TM:]
Fr A is closed Element of bool the carrier of TM
A ` is Element of bool the carrier of TM
the carrier of TM \ A is set
Cl (A `) is closed Element of bool the carrier of TM
(Cl A) /\ (Cl (A `)) is closed Element of bool the carrier of TM
[:(Cl cTM),(Fr A):] is Relation-like Element of bool the carrier of [:n,TM:]
[:(Fr cTM),(Cl A):] \/ [:(Cl cTM),(Fr A):] is Relation-like Element of bool the carrier of [:n,TM:]
[:(Cl cTM),(Cl A):] is Relation-like Element of bool the carrier of [:n,TM:]
[#] TM is non proper open closed dense Element of bool the carrier of TM
[:(Cl (cTM `)),([#] TM):] is Relation-like Element of bool the carrier of [:n,TM:]
[:(Cl cTM),(Cl A):] /\ [:(Cl (cTM `)),([#] TM):] is Relation-like Element of bool the carrier of [:n,TM:]
(Cl A) /\ ([#] TM) is closed Element of bool the carrier of TM
[:((Cl cTM) /\ (Cl (cTM `))),((Cl A) /\ ([#] TM)):] is Relation-like Element of bool the carrier of [:n,TM:]
[#] n is non proper open closed dense Element of bool the carrier of n
[:([#] n),(Cl (A `)):] is Relation-like Element of bool the carrier of [:n,TM:]
[:(Cl cTM),(Cl A):] /\ [:([#] n),(Cl (A `)):] is Relation-like Element of bool the carrier of [:n,TM:]
(Cl cTM) /\ ([#] n) is closed Element of bool the carrier of n
[:((Cl cTM) /\ ([#] n)),((Cl A) /\ (Cl (A `))):] is Relation-like Element of bool the carrier of [:n,TM:]
Cl ([#] n) is closed Element of bool the carrier of n
[:([#] n),(A `):] is Relation-like Element of bool the carrier of [:n,TM:]
Cl [:([#] n),(A `):] is closed Element of bool the carrier of [:n,TM:]
Cl ([#] TM) is closed Element of bool the carrier of TM
[:(cTM `),([#] TM):] is Relation-like Element of bool the carrier of [:n,TM:]
Cl [:(cTM `),([#] TM):] is closed Element of bool the carrier of [:n,TM:]
[:([#] n),([#] TM):] is Relation-like Element of bool the carrier of [:n,TM:]
[:([#] n),([#] TM):] \ [:cTM,A:] is Relation-like Element of bool the carrier of [:n,TM:]
Cl ([:([#] n),([#] TM):] \ [:cTM,A:]) is closed Element of bool the carrier of [:n,TM:]
([#] n) \ cTM is Element of bool the carrier of n
[:(([#] n) \ cTM),([#] TM):] is Relation-like Element of bool the carrier of [:n,TM:]
([#] TM) \ A is Element of bool the carrier of TM
[:([#] n),(([#] TM) \ A):] is Relation-like Element of bool the carrier of [:n,TM:]
[:(([#] n) \ cTM),([#] TM):] \/ [:([#] n),(([#] TM) \ A):] is Relation-like Element of bool the carrier of [:n,TM:]
Cl ([:(([#] n) \ cTM),([#] TM):] \/ [:([#] n),(([#] TM) \ A):]) is closed Element of bool the carrier of [:n,TM:]
[:(Cl (cTM `)),([#] TM):] \/ [:([#] n),(Cl (A `)):] is Relation-like Element of bool the carrier of [:n,TM:]
[:(Cl cTM),(Cl A):] /\ ([:(Cl (cTM `)),([#] TM):] \/ [:([#] n),(Cl (A `)):]) is Relation-like Element of bool the carrier of [:n,TM:]
n is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind n is V83() real ext-real integer set
[#] n is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of n
the carrier of n is set
bool the carrier of n is non empty set
ind ([#] n) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
[:n,TM:] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable TopStruct
ind [:n,TM:] is V83() real ext-real integer set
[#] [:n,TM:] is non proper open closed F_sigma G_delta dense Element of bool the carrier of [:n,TM:]
the carrier of [:n,TM:] is set
bool the carrier of [:n,TM:] is non empty set
ind ([#] [:n,TM:]) 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 with_finite_small_inductive_dimension 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
(ind n) + (ind TM) is V83() real ext-real set
K190((ind n),(ind TM)) is V83() real ext-real integer set
(ind n) + 1 is V83() real ext-real set
K190((ind n),1) 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
A1 is ordinal natural finite cardinal V83() real ext-real non negative countable 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
A2 is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind A2 is V83() real ext-real integer set
[#] A2 is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of A2
the carrier of A2 is set
bool the carrier of A2 is non empty set
ind ([#] A2) is V83() real ext-real integer set
A12 is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind A12 is V83() real ext-real integer set
[#] A12 is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of A12
the carrier of A12 is set
bool the carrier of A12 is non empty set
ind ([#] A12) is V83() real ext-real integer set
(ind A2) + (ind A12) is V83() real ext-real set
K190((ind A2),(ind A12)) is V83() real ext-real integer set
((ind A2) + (ind A12)) + 2 is V83() real ext-real set
K190(((ind A2) + (ind A12)),2) is V83() real ext-real set
[:A2,A12:] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable TopStruct
ind [:A2,A12:] is V83() real ext-real integer set
[#] [:A2,A12:] is non proper open closed F_sigma G_delta dense Element of bool the carrier of [:A2,A12:]
the carrier of [:A2,A12:] is set
bool the carrier of [:A2,A12:] is non empty set
ind ([#] [:A2,A12:]) 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
0 + (- 1) is non empty V83() real ext-real non positive negative set
K190(0,(- 1)) is non empty V83() real ext-real non positive negative set
(ind A12) + (ind A2) is V83() real ext-real set
K190((ind A12),(ind A2)) 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
0 + (- 1) is non empty V83() real ext-real non positive negative set
K190(0,(- 1)) is non empty V83() real ext-real non positive negative set
A19 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
A29 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
A19 + A29 is V83() real ext-real non negative set
K190(A19,A29) is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
(A19 + A29) - 1 is V83() real ext-real set
K194((A19 + A29),1) is V83() real ext-real set
A9 is Element of the carrier of [:A2,A12:]
A29 is open F_sigma Element of bool the carrier of [:A2,A12:]
bool (bool the carrier of [:A2,A12:]) is non empty set
A19 is Element of bool (bool the carrier of [:A2,A12:])
union A19 is Element of bool the carrier of [:A2,A12:]
L is set
U is with_finite_small_inductive_dimension Element of bool the carrier of A2
W is with_finite_small_inductive_dimension Element of bool the carrier of A12
[:U,W:] is Relation-like Element of bool the carrier of [:A2,A12:]
L9 is set
U9 is set
[L9,U9] is non empty V15() set
{L9,U9} is non empty finite countable set
{L9} is non empty trivial finite 1 -element countable set
{{L9,U9},{L9}} is non empty finite V32() countable set
W9 is Element of the carrier of A2
A19 - 1 is V83() real ext-real set
K194(A19,1) is V83() real ext-real integer set
U9 is open F_sigma with_finite_small_inductive_dimension Element of bool the carrier of A2
Fr U9 is closed G_delta boundary nowhere_dense with_finite_small_inductive_dimension Element of bool the carrier of A2
Cl U9 is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A2
U9 ` is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A2
the carrier of A2 \ U9 is set
Cl (U9 `) is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A2
(Cl U9) /\ (Cl (U9 `)) is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A2
ind (Fr U9) is V83() real ext-real integer set
A2 | (Cl U9) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable SubSpace of A2
ind (A2 | (Cl U9)) is V83() real ext-real integer set
[#] (A2 | (Cl U9)) is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of (A2 | (Cl U9))
the carrier of (A2 | (Cl U9)) is set
bool the carrier of (A2 | (Cl U9)) is non empty set
ind ([#] (A2 | (Cl U9))) is V83() real ext-real integer set
ind (Cl U9) is V83() real ext-real integer set
X2 is Element of the carrier of A12
A29 - 1 is V83() real ext-real set
K194(A29,1) is V83() real ext-real integer set
X1 is open F_sigma with_finite_small_inductive_dimension Element of bool the carrier of A12
Fr X1 is closed G_delta boundary nowhere_dense with_finite_small_inductive_dimension Element of bool the carrier of A12
Cl X1 is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A12
X1 ` is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A12
the carrier of A12 \ X1 is set
Cl (X1 `) is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A12
(Cl X1) /\ (Cl (X1 `)) is closed G_delta with_finite_small_inductive_dimension Element of bool the carrier of A12
ind (Fr X1) is V83() real ext-real integer set
[:U9,X1:] is Relation-like Element of bool the carrier of [:A2,A12:]
gV1 is open F_sigma Element of bool the carrier of [:A2,A12:]
Fr gV1 is closed G_delta boundary nowhere_dense Element of bool the carrier of [:A2,A12:]
Cl gV1 is closed G_delta Element of bool the carrier of [:A2,A12:]
gV1 ` is closed G_delta Element of bool the carrier of [:A2,A12:]
the carrier of [:A2,A12:] \ gV1 is set
Cl (gV1 `) is closed G_delta Element of bool the carrier of [:A2,A12:]
(Cl gV1) /\ (Cl (gV1 `)) is closed G_delta Element of bool the carrier of [:A2,A12:]
ind (Fr gV1) is V83() real ext-real integer set
(A19 + A29) + 1 is non empty V83() real ext-real positive non negative set
K190((A19 + A29),1) is non empty V83() real ext-real positive non negative set
((A19 + A29) + 1) + 1 is non empty V83() real ext-real positive non negative set
K190(((A19 + A29) + 1),1) is non empty V83() real ext-real positive non negative set
A2 | (Fr U9) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable SubSpace of A2
ind (A2 | (Fr U9)) is V83() real ext-real integer set
[#] (A2 | (Fr U9)) is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of (A2 | (Fr U9))
the carrier of (A2 | (Fr U9)) is set
bool the carrier of (A2 | (Fr U9)) is non empty set
ind ([#] (A2 | (Fr U9))) is V83() real ext-real integer set
[:(Fr U9),(Cl X1):] is Relation-like Element of bool the carrier of [:A2,A12:]
A12 | (Cl X1) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable SubSpace of A12
[:(A2 | (Fr U9)),(A12 | (Cl X1)):] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable TopStruct
gh is Element of bool the carrier of [:A2,A12:]
[:A2,A12:] | gh is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable SubSpace of [:A2,A12:]
ind (A12 | (Cl X1)) is V83() real ext-real integer set
[#] (A12 | (Cl X1)) is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of (A12 | (Cl X1))
the carrier of (A12 | (Cl X1)) is set
bool the carrier of (A12 | (Cl X1)) is non empty set
ind ([#] (A12 | (Cl X1))) is V83() real ext-real integer set
ind (Cl X1) is V83() real ext-real integer set
(ind (A2 | (Fr U9))) + (ind (A12 | (Cl X1))) is V83() real ext-real set
K190((ind (A2 | (Fr U9))),(ind (A12 | (Cl X1)))) is V83() real ext-real integer set
(A19 - 1) + A29 is V83() real ext-real set
K190((A19 - 1),A29) is V83() real ext-real set
((ind (A2 | (Fr U9))) + (ind (A12 | (Cl X1)))) + 2 is V83() real ext-real set
K190(((ind (A2 | (Fr U9))) + (ind (A12 | (Cl X1)))),2) is V83() real ext-real set
((A19 + A29) - 1) + 2 is V83() real ext-real set
K190(((A19 + A29) - 1),2) is V83() real ext-real set
[:(Cl U9),(Fr X1):] is Relation-like Element of bool the carrier of [:A2,A12:]
A12 | (Fr X1) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable SubSpace of A12
[:(A2 | (Cl U9)),(A12 | (Fr X1)):] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable TopStruct
b is Element of bool the carrier of [:A2,A12:]
[:A2,A12:] | b is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable SubSpace of [:A2,A12:]
ind (A12 | (Fr X1)) is V83() real ext-real integer set
[#] (A12 | (Fr X1)) is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of (A12 | (Fr X1))
the carrier of (A12 | (Fr X1)) is set
bool the carrier of (A12 | (Fr X1)) is non empty set
ind ([#] (A12 | (Fr X1))) is V83() real ext-real integer set
(ind (A2 | (Cl U9))) + (ind (A12 | (Fr X1))) is V83() real ext-real set
K190((ind (A2 | (Cl U9))),(ind (A12 | (Fr X1)))) is V83() real ext-real integer set
A19 + (A29 - 1) is V83() real ext-real set
K190(A19,(A29 - 1)) is V83() real ext-real set
((ind (A2 | (Cl U9))) + (ind (A12 | (Fr X1)))) + 2 is V83() real ext-real set
K190(((ind (A2 | (Cl U9))) + (ind (A12 | (Fr X1)))),2) is V83() real ext-real set
(A19 + (A29 - 1)) + 2 is V83() real ext-real set
K190((A19 + (A29 - 1)),2) is V83() real ext-real set
ind [:(A2 | (Cl U9)),(A12 | (Fr X1)):] is V83() real ext-real integer set
[#] [:(A2 | (Cl U9)),(A12 | (Fr X1)):] is non proper open closed F_sigma G_delta dense Element of bool the carrier of [:(A2 | (Cl U9)),(A12 | (Fr X1)):]
the carrier of [:(A2 | (Cl U9)),(A12 | (Fr X1)):] is set
bool the carrier of [:(A2 | (Cl U9)),(A12 | (Fr X1)):] is non empty set
ind ([#] [:(A2 | (Cl U9)),(A12 | (Fr X1)):]) is V83() real ext-real integer set
ind b is V83() real ext-real integer set
b \/ gh is Element of bool the carrier of [:A2,A12:]
[:A2,A12:] | (b \/ gh) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable SubSpace of [:A2,A12:]
ind [:(A2 | (Fr U9)),(A12 | (Cl X1)):] is V83() real ext-real integer set
[#] [:(A2 | (Fr U9)),(A12 | (Cl X1)):] is non proper open closed F_sigma G_delta dense Element of bool the carrier of [:(A2 | (Fr U9)),(A12 | (Cl X1)):]
the carrier of [:(A2 | (Fr U9)),(A12 | (Cl X1)):] is set
bool the carrier of [:(A2 | (Fr U9)),(A12 | (Cl X1)):] is non empty set
ind ([#] [:(A2 | (Fr U9)),(A12 | (Cl X1)):]) is V83() real ext-real integer set
ind gh is V83() real ext-real integer set
ind (b \/ gh) is V83() real ext-real integer set
A1 is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind A1 is V83() real ext-real integer set
[#] A1 is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension 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
A2 is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind A2 is V83() real ext-real integer set
[#] A2 is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of A2
the carrier of A2 is set
bool the carrier of A2 is non empty set
ind ([#] A2) is V83() real ext-real integer set
(ind A1) + (ind A2) is V83() real ext-real set
K190((ind A1),(ind A2)) is V83() real ext-real integer set
((ind A1) + (ind A2)) + 2 is V83() real ext-real set
K190(((ind A1) + (ind A2)),2) is V83() real ext-real set
[:A1,A2:] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable TopStruct
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
(ind A1) + 1 is V83() real ext-real set
K190((ind A1),1) is V83() real ext-real integer set
(ind A2) + 1 is V83() real ext-real set
K190((ind A2),1) is V83() real ext-real integer set
A12 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
T912 is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
A12 + T912 is V83() real ext-real non negative set
K190(A12,T912) is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
((ind n) + (ind TM)) + 2 is V83() real ext-real set
K190(((ind n) + (ind TM)),2) is V83() real ext-real set
cTM is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
A is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
cTM + A is V83() real ext-real non negative set
K190(cTM,A) is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
n is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
[:n,TM:] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof metrizable TopStruct
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 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
cTM is Element of bool the carrier of TM
A is Element of bool the carrier of TM
A1 is Element of bool the carrier of TM
ind A1 is V83() real ext-real integer set
TM | A1 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
ind (TM | A1) is V83() real ext-real integer set
[#] (TM | A1) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (TM | A1)
the carrier of (TM | A1) is set
bool the carrier of (TM | A1) is non empty set
ind ([#] (TM | A1)) is V83() real ext-real integer set
A2 is Element of bool the carrier of (TM | A1)
A12 is Element of bool the carrier of (TM | A1)
A2 \/ A12 is Element of bool the carrier of (TM | A1)
ind A2 is V83() real ext-real integer set
ind A12 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
A19 is Element of bool the carrier of TM
T912 is Element of bool the carrier of TM
T912 \/ A19 is Element of bool the carrier of TM
A19 /\ A1 is Element of bool the carrier of TM
ind A19 is V83() real ext-real integer set
(TM | A1) | A12 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM | A1
TM | A19 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
A29 is Element of bool the carrier of TM
A29 /\ A1 is Element of bool the carrier of TM
ind (A29 /\ A1) is V83() real ext-real integer set
ind T912 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
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
TM | ([#] TM) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
cTM is Element of bool the carrier of TM
A is Element of bool the carrier of TM
A1 is Element of bool the carrier of TM
A1 /\ ([#] TM) is Element of bool the carrier of TM
ind (A1 /\ ([#] TM)) is V83() real ext-real integer set
ind A1 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
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
cTM is Element of bool the carrier of TM
TM | cTM is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
ind cTM is V83() real ext-real integer set
A is Element of the carrier of TM
A1 is open F_sigma Element of bool the carrier of TM
{A} is non empty trivial finite 1 -element countable set
A1 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ A1 is set
A2 is Element of bool the carrier of TM
A12 is Element of bool the carrier of TM
A12 /\ cTM is Element of bool the carrier of TM
ind (A12 /\ cTM) is V83() real ext-real integer set
T912 is open F_sigma Element of bool the carrier of TM
A19 is open F_sigma Element of bool the carrier of TM
T912 \/ A19 is open F_sigma Element of bool the carrier of TM
(T912 \/ A19) ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ (T912 \/ A19) is set
A29 is open F_sigma Element of bool the carrier of TM
A19 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ A19 is set
(A1 `) ` is open F_sigma Element of bool the carrier of TM
the carrier of TM \ (A1 `) is set
Cl A29 is closed G_delta Element of bool the carrier of TM
(Cl A29) \ A19 is Element of bool the carrier of TM
Fr A29 is closed G_delta boundary nowhere_dense Element of bool the carrier of TM
A29 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ A29 is set
Cl (A29 `) is closed G_delta Element of bool the carrier of TM
(Cl A29) /\ (Cl (A29 `)) is closed G_delta Element of bool the carrier of TM
((Cl A29) \ A19) \ A29 is Element of bool the carrier of TM
A29 \/ A19 is open F_sigma Element of bool the carrier of TM
(Cl A29) \ (A29 \/ A19) is Element of bool the carrier of TM
(Cl A29) /\ A12 is Element of bool the carrier of TM
cTM /\ (Fr A29) is Element of bool the carrier of TM
cTM /\ A12 is Element of bool the carrier of TM
ind (cTM /\ (Fr A29)) is V83() real ext-real integer set
ind (cTM /\ A12) is V83() real ext-real integer set
the carrier of (TM | cTM) is set
bool the carrier of (TM | cTM) is non empty set
[#] (TM | cTM) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (TM | cTM)
A1 is Element of the carrier of (TM | cTM)
A2 is open F_sigma Element of bool the carrier of (TM | cTM)
T912 is Element of bool the carrier of TM
T912 /\ the carrier of (TM | cTM) is Element of bool the carrier of TM
A12 is Element of the carrier of TM
A19 is open F_sigma Element of bool the carrier of TM
Fr A19 is closed G_delta boundary nowhere_dense Element of bool the carrier of TM
Cl A19 is closed G_delta Element of bool the carrier of TM
A19 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ A19 is set
Cl (A19 `) is closed G_delta Element of bool the carrier of TM
(Cl A19) /\ (Cl (A19 `)) is closed G_delta Element of bool the carrier of TM
cTM /\ (Fr A19) is Element of bool the carrier of TM
ind (cTM /\ (Fr A19)) is V83() real ext-real integer set
A19 /\ the carrier of (TM | cTM) is Element of bool the carrier of TM
A29 is Element of bool the carrier of (TM | cTM)
A9 is open F_sigma Element of bool the carrier of (TM | cTM)
Fr A9 is closed G_delta boundary nowhere_dense Element of bool the carrier of (TM | cTM)
Cl A9 is closed G_delta Element of bool the carrier of (TM | cTM)
A9 ` is closed G_delta Element of bool the carrier of (TM | cTM)
the carrier of (TM | cTM) \ A9 is set
Cl (A9 `) is closed G_delta Element of bool the carrier of (TM | cTM)
(Cl A9) /\ (Cl (A9 `)) is closed G_delta Element of bool the carrier of (TM | cTM)
ind (Fr A9) is V83() real ext-real integer set
A29 is Element of bool the carrier of TM
(Fr A19) /\ cTM is Element of bool the carrier of TM
ind A29 is V83() real ext-real integer set
ind ((Fr A19) /\ cTM) is V83() real ext-real integer set
ind (TM | cTM) is V83() real ext-real integer set
[#] (TM | cTM) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (TM | cTM)
ind ([#] (TM | cTM)) 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
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
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
the topology of TM is non empty Element of bool (bool the carrier of TM)
A1 is Element of bool the carrier of TM
TM | A1 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
ind A1 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
[:([#] TM), the topology of TM:] is Relation-like set
A2 is set
A12 is set
T912 is set
[A12,T912] is non empty V15() set
{A12,T912} is non empty finite countable set
{A12} is non empty trivial finite 1 -element countable set
{{A12,T912},{A12}} is non empty finite V32() countable set
A29 is Element of the carrier of TM
A19 is open F_sigma Element of bool the carrier of TM
A9 is Element of the carrier of TM
A29 is Element of bool the carrier of TM
[A9,A29] is non empty V15() set
{A9,A29} is non empty finite countable set
{A9} is non empty trivial finite 1 -element countable set
{{A9,A29},{A9}} is non empty finite V32() countable set
A29 is Element of the carrier of TM
A19 is open F_sigma Element of bool the carrier of TM
A9 is open F_sigma Element of bool the carrier of TM
Fr A9 is closed G_delta boundary nowhere_dense Element of bool the carrier of TM
Cl A9 is closed G_delta Element of bool the carrier of TM
A9 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ A9 is set
Cl (A9 `) is closed G_delta Element of bool the carrier of TM
(Cl A9) /\ (Cl (A9 `)) is closed G_delta Element of bool the carrier of TM
A1 /\ (Fr A9) is Element of bool the carrier of TM
ind (A1 /\ (Fr A9)) is V83() real ext-real integer set
A29 is Element of the carrier of TM
A19 is Element of bool the carrier of TM
[A29,A19] is non empty V15() set
{A29,A19} is non empty finite countable set
{A29} is non empty trivial finite 1 -element countable set
{{A29,A19},{A29}} is non empty finite V32() countable set
A29 is Element of the carrier of TM
A19 is open F_sigma Element of bool the carrier of TM
A2 is Relation-like Function-like set
proj1 A2 is set
proj2 A2 is set
A12 is set
T912 is set
A2 . T912 is set
A19 is set
A29 is set
[A19,A29] is non empty V15() set
{A19,A29} is non empty finite countable set
{A19} is non empty trivial finite 1 -element countable set
{{A19,A29},{A19}} is non empty finite V32() countable set
T912 is Element of bool the carrier of TM
A19 is Element of the carrier of TM
[A19,T912] is non empty V15() set
{A19,T912} is non empty finite countable set
{A19} is non empty trivial finite 1 -element countable set
{{A19,T912},{A19}} is non empty finite V32() countable set
A2 . [A19,T912] is set
A29 is open F_sigma Element of bool the carrier of TM
Fr A29 is closed G_delta boundary nowhere_dense Element of bool the carrier of TM
Cl A29 is closed G_delta Element of bool the carrier of TM
A29 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ A29 is set
Cl (A29 `) is closed G_delta Element of bool the carrier of TM
(Cl A29) /\ (Cl (A29 `)) is closed G_delta Element of bool the carrier of TM
A1 /\ (Fr A29) is Element of bool the carrier of TM
ind (A1 /\ (Fr A29)) is V83() real ext-real integer set
A9 is Element of bool the carrier of TM
A29 is Element of bool the carrier of TM
A12 is Element of bool (bool the carrier of TM)
T912 is open V85(TM) Element of bool (bool the carrier of TM)
A29 is Element of bool the carrier of TM
A19 is open V85(TM) Element of bool (bool the carrier of TM)
A9 is set
A2 . A9 is set
A29 is set
A19 is set
[A29,A19] is non empty V15() set
{A29,A19} is non empty finite countable set
{A29} is non empty trivial finite 1 -element countable set
{{A29,A19},{A29}} is non empty finite V32() countable set
L is open F_sigma Element of bool the carrier of TM
[A29,L] is non empty V15() set
{A29,L} is non empty finite countable set
{{A29,L},{A29}} is non empty finite V32() countable set
A2 . [A29,L] is set
Fr A29 is closed G_delta Element of bool the carrier of TM
Cl A29 is closed G_delta Element of bool the carrier of TM
A29 ` is Element of bool the carrier of TM
the carrier of TM \ A29 is set
Cl (A29 `) is closed G_delta Element of bool the carrier of TM
(Cl A29) /\ (Cl (A29 `)) is closed G_delta Element of bool the carrier of TM
A1 /\ (Fr A29) is Element of bool the carrier of TM
ind (A1 /\ (Fr A29)) is V83() real ext-real integer set
U is open F_sigma Element of bool the carrier of TM
Fr U is closed G_delta boundary nowhere_dense Element of bool the carrier of TM
Cl U is closed G_delta Element of bool the carrier of TM
U ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ U is set
Cl (U `) is closed G_delta Element of bool the carrier of TM
(Cl U) /\ (Cl (U `)) is closed G_delta Element of bool the carrier of TM
A1 /\ (Fr U) is Element of bool the carrier of TM
ind (A1 /\ (Fr U)) is V83() real ext-real integer set
L is open F_sigma Element of bool the carrier of TM
Fr A29 is closed G_delta Element of bool the carrier of TM
Cl A29 is closed G_delta Element of bool the carrier of TM
A29 ` is Element of bool the carrier of TM
the carrier of TM \ A29 is set
Cl (A29 `) is closed G_delta Element of bool the carrier of TM
(Cl A29) /\ (Cl (A29 `)) is closed G_delta Element of bool the carrier of TM
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 /\ (Fr A29) is Element of bool the carrier of TM
ind (A1 /\ (Fr A29)) is V83() real ext-real integer set
L is open F_sigma Element of bool the carrier of TM
A2 is open V85(TM) Element of bool (bool the carrier of TM)
A12 is Element of the carrier of TM
T912 is open F_sigma Element of bool the carrier of TM
A19 is Element of bool the carrier of TM
A29 is open F_sigma Element of bool the carrier of TM
Fr A29 is closed G_delta boundary nowhere_dense Element of bool the carrier of TM
Cl A29 is closed G_delta Element of bool the carrier of TM
A29 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ A29 is set
Cl (A29 `) is closed G_delta Element of bool the carrier of TM
(Cl A29) /\ (Cl (A29 `)) is closed G_delta Element of bool the carrier of TM
A1 /\ (Fr A29) is Element of bool the carrier of TM
ind (A1 /\ (Fr A29)) is V83() real ext-real integer set
n is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
[:n,TM:] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind [:n,TM:] is V83() real ext-real integer set
[#] [:n,TM:] is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of [:n,TM:]
the carrier of [:n,TM:] is set
bool the carrier of [:n,TM:] is non empty set
ind ([#] [:n,TM:]) is V83() real ext-real integer set
ind n is V83() real ext-real integer set
[#] n is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of n
the carrier of n is set
bool the carrier of n is non empty set
ind ([#] n) 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 with_finite_small_inductive_dimension 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
(ind n) + (ind TM) is V83() real ext-real set
K190((ind n),(ind TM)) is V83() real ext-real integer set
n is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind n is V83() real ext-real integer set
[#] n is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of n
the carrier of n is set
bool the carrier of n is non empty set
ind ([#] n) is V83() real ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
[:TM,n:] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind [:TM,n:] is V83() real ext-real integer set
[#] [:TM,n:] is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of [:TM,n:]
the carrier of [:TM,n:] is set
bool the carrier of [:TM,n:] is non empty set
ind ([#] [:TM,n:]) 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 with_finite_small_inductive_dimension 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
(ind TM) + 0 is V83() real ext-real set
K190((ind TM),0) is V83() real ext-real integer set
the Element of the carrier of n is Element of the carrier of n
{ the Element of the carrier of n} is non empty trivial finite 1 -element countable set
- 1 is non empty V83() real ext-real non positive negative set
K192(1) is V83() real ext-real non positive integer set
A is with_finite_small_inductive_dimension Element of bool the carrier of n
n | A is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable SubSpace of n
[:(n | A),TM:] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind [:(n | A),TM:] is V83() real ext-real integer set
[#] [:(n | A),TM:] is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of [:(n | A),TM:]
the carrier of [:(n | A),TM:] is set
bool the carrier of [:(n | A),TM:] is non empty set
ind ([#] [:(n | A),TM:]) is V83() real ext-real integer set
[:TM,(n | A):] is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable TopStruct
ind [:TM,(n | A):] is V83() real ext-real integer set
[#] [:TM,(n | A):] is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of [:TM,(n | A):]
the carrier of [:TM,(n | A):] is set
bool the carrier of [:TM,(n | A):] is non empty set
ind ([#] [:TM,(n | A):]) is V83() real ext-real integer set
A1 is with_finite_small_inductive_dimension Element of bool the carrier of [:TM,n:]
[:TM,n:] | A1 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 second-countable Lindelof with_finite_small_inductive_dimension metrizable SubSpace of [:TM,n:]
ind A1 is V83() real ext-real integer set
TOP-REAL 1 is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() L20()
the carrier of (TOP-REAL 1) is non empty set
n is Element of the carrier of (Euclid 1)
TM is V83() real ext-real set
<*TM*> is Relation-like Function-like set
cTM is V83() real ext-real set
cl_Ball (n,cTM) is Element of bool the carrier of (Euclid 1)
bool the carrier of (Euclid 1) is non empty set
TM - cTM is V83() real ext-real set
K194(TM,cTM) is V83() real ext-real set
TM + cTM is V83() real ext-real set
K190(TM,cTM) is V83() real ext-real set
{ <*b₁*> where b₁ is V83() real ext-real Element of REAL : ( TM - cTM <= b₁ & b₁ <= TM + cTM ) } is set
{ b₁ where b₁ is Element of the carrier of (Euclid 1) : dist (n,b₁) <= cTM } is set
A1 is V83() real ext-real Element of REAL
A1 - cTM is V83() real ext-real set
K194(A1,cTM) is V83() real ext-real set
A1 + cTM is V83() real ext-real set
K190(A1,cTM) is V83() real ext-real set
{ <*b₁*> where b₁ is V83() real ext-real Element of REAL : ( A1 - cTM <= b₁ & b₁ <= A1 + cTM ) } is set
A12 is set
T912 is Element of the carrier of (Euclid 1)
dist (n,T912) is V83() real ext-real Element of REAL
the distance of (Euclid 1) is Relation-like [: the carrier of (Euclid 1), the carrier of (Euclid 1):] -defined REAL -valued Function-like V18([: the carrier of (Euclid 1), the carrier of (Euclid 1):], REAL ) complex-yielding V199() V200() Element of bool [:[: the carrier of (Euclid 1), the carrier of (Euclid 1):],REAL:]
[: the carrier of (Euclid 1), the carrier of (Euclid 1):] is non empty Relation-like set
[:[: the carrier of (Euclid 1), the carrier of (Euclid 1):],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[: the carrier of (Euclid 1), the carrier of (Euclid 1):],REAL:] is non empty non trivial non finite set
the distance of (Euclid 1) . (n,T912) is V83() real ext-real Element of REAL
A19 is V83() real ext-real Element of REAL
<*A19*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
<*A1*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
<*A1*> - <*A19*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
A1 - A19 is V83() real ext-real set
K194(A1,A19) is V83() real ext-real set
<*(A1 - A19)*> is Relation-like Function-like set
sqr (<*A1*> - <*A19*>) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
(A1 - A19) ^2 is set
K191((A1 - A19),(A1 - A19)) is V83() real ext-real set
<*((A1 - A19) ^2)*> is Relation-like Function-like set
Sum (sqr (<*A1*> - <*A19*>)) is V83() real ext-real Element of REAL
sqrt (Sum (sqr (<*A1*> - <*A19*>))) is V83() real ext-real Element of REAL
abs (A1 - A19) is V83() real ext-real Element of REAL
|.(<*A1*> - <*A19*>).| is V83() real ext-real non negative Element of REAL
(A1 - A19) + A19 is V83() real ext-real set
K190((A1 - A19),A19) is V83() real ext-real set
cTM + A19 is V83() real ext-real set
K190(cTM,A19) is V83() real ext-real set
(cTM + A19) - cTM is V83() real ext-real set
K194((cTM + A19),cTM) is V83() real ext-real set
- cTM is V83() real ext-real set
K192(cTM) is V83() real ext-real set
(- cTM) + A19 is V83() real ext-real set
K190((- cTM),A19) is V83() real ext-real set
A19 - cTM is V83() real ext-real set
K194(A19,cTM) is V83() real ext-real set
(A19 - cTM) + cTM is V83() real ext-real set
K190((A19 - cTM),cTM) is V83() real ext-real set
<*A1*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
T912 is set
A19 is V83() real ext-real Element of REAL
<*A19*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
A19 - cTM is V83() real ext-real set
K194(A19,cTM) is V83() real ext-real set
(A1 + cTM) - cTM is V83() real ext-real set
K194((A1 + cTM),cTM) is V83() real ext-real set
- cTM is V83() real ext-real set
K192(cTM) is V83() real ext-real set
A19 + (- cTM) is V83() real ext-real set
K190(A19,(- cTM)) is V83() real ext-real set
(A19 + (- cTM)) - A19 is V83() real ext-real set
K194((A19 + (- cTM)),A19) is V83() real ext-real set
A1 - A19 is V83() real ext-real set
K194(A1,A19) is V83() real ext-real set
<*A1*> - <*A19*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
<*(A1 - A19)*> is Relation-like Function-like set
sqr (<*A1*> - <*A19*>) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
(A1 - A19) ^2 is set
K191((A1 - A19),(A1 - A19)) is V83() real ext-real set
<*((A1 - A19) ^2)*> is Relation-like Function-like set
Sum (sqr (<*A1*> - <*A19*>)) is V83() real ext-real Element of REAL
(A1 - cTM) + cTM is V83() real ext-real set
K190((A1 - cTM),cTM) is V83() real ext-real set
A19 + cTM is V83() real ext-real set
K190(A19,cTM) is V83() real ext-real set
(A19 + cTM) - A19 is V83() real ext-real set
K194((A19 + cTM),A19) is V83() real ext-real set
abs (A1 - A19) is V83() real ext-real Element of REAL
|.(<*A1*> - <*A19*>).| is V83() real ext-real non negative Element of REAL
sqrt (Sum (sqr (<*A1*> - <*A19*>))) is V83() real ext-real Element of REAL
the distance of (Euclid 1) is Relation-like [: the carrier of (Euclid 1), the carrier of (Euclid 1):] -defined REAL -valued Function-like V18([: the carrier of (Euclid 1), the carrier of (Euclid 1):], REAL ) complex-yielding V199() V200() Element of bool [:[: the carrier of (Euclid 1), the carrier of (Euclid 1):],REAL:]
[: the carrier of (Euclid 1), the carrier of (Euclid 1):] is non empty Relation-like set
[:[: the carrier of (Euclid 1), the carrier of (Euclid 1):],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[: the carrier of (Euclid 1), the carrier of (Euclid 1):],REAL:] is non empty non trivial non finite set
A9 is Element of the carrier of (Euclid 1)
the distance of (Euclid 1) . (n,A9) is V83() real ext-real Element of REAL
dist (n,A9) is V83() real ext-real Element of REAL
A12 is non empty trivial Relation-like NAT -defined REAL -valued Function-like constant finite 1 -element countable complex-yielding V199() V200() V202() V203() V204() V205() FinSequence-like Element of REAL 1
A29 is non empty trivial Relation-like NAT -defined REAL -valued Function-like constant finite 1 -element countable complex-yielding V199() V200() V202() V203() V204() V205() FinSequence-like Element of REAL 1
(Pitag_dist 1) . (A12,A29) is V83() real ext-real Element of REAL
the topology of (TOP-REAL 1) is non empty Element of bool (bool the carrier of (TOP-REAL 1))
bool the carrier of (TOP-REAL 1) is non empty set
bool (bool the carrier of (TOP-REAL 1)) is non empty set
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is non empty strict TopSpace-like second-countable Lindelof TopStruct
TopSpaceMetr (Euclid 1) is non empty strict TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 T_1/2 metrizable TopStruct
Family_open_set (Euclid 1) is Element of bool (bool the carrier of (Euclid 1))
bool the carrier of (Euclid 1) is non empty set
bool (bool the carrier of (Euclid 1)) is non empty set
TopStruct(# the carrier of (Euclid 1),(Family_open_set (Euclid 1)) #) is non empty strict TopStruct
n is non empty trivial finite 1 -element countable V200() FinSequence-like Element of the carrier of (TOP-REAL 1)
TM is V83() real ext-real set
<*TM*> is Relation-like Function-like set
cTM is V83() real ext-real set
Ball (n,cTM) is Element of bool the carrier of (TOP-REAL 1)
Fr (Ball (n,cTM)) is closed Element of bool the carrier of (TOP-REAL 1)
Cl (Ball (n,cTM)) is closed Element of bool the carrier of (TOP-REAL 1)
(Ball (n,cTM)) ` is Element of bool the carrier of (TOP-REAL 1)
the carrier of (TOP-REAL 1) \ (Ball (n,cTM)) is set
Cl ((Ball (n,cTM)) `) is closed Element of bool the carrier of (TOP-REAL 1)
(Cl (Ball (n,cTM))) /\ (Cl ((Ball (n,cTM)) `)) is closed Element of bool the carrier of (TOP-REAL 1)
TM - cTM is V83() real ext-real set
K194(TM,cTM) is V83() real ext-real set
<*(TM - cTM)*> is Relation-like Function-like set
TM + cTM is V83() real ext-real set
K190(TM,cTM) is V83() real ext-real set
<*(TM + cTM)*> is Relation-like Function-like set
{<*(TM - cTM)*>,<*(TM + cTM)*>} is non empty functional finite countable set
A is Element of the carrier of (Euclid 1)
Ball (A,cTM) is Element of bool the carrier of (Euclid 1)
{ <*b₁*> where b₁ is V83() real ext-real Element of REAL : ( not b₁ <= TM - cTM & not TM + cTM <= b₁ ) } is set
(Cl (Ball (n,cTM))) \ (Ball (n,cTM)) is Element of bool the carrier of (TOP-REAL 1)
cl_Ball (n,cTM) is Element of bool the carrier of (TOP-REAL 1)
(cl_Ball (n,cTM)) \ (Ball (n,cTM)) is Element of bool the carrier of (TOP-REAL 1)
cl_Ball (A,cTM) is Element of bool the carrier of (Euclid 1)
(cl_Ball (A,cTM)) \ (Ball (n,cTM)) is Element of bool the carrier of (Euclid 1)
(cl_Ball (A,cTM)) \ (Ball (A,cTM)) is Element of bool the carrier of (Euclid 1)
{ <*b₁*> where b₁ is V83() real ext-real Element of REAL : ( TM - cTM <= b₁ & b₁ <= TM + cTM ) } is set
A1 is set
A12 is V83() real ext-real Element of REAL
<*A12*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
A2 is Element of the carrier of (Euclid 1)
A1 is set
- cTM is V83() real ext-real set
K192(cTM) is V83() real ext-real set
TM + (- cTM) is V83() real ext-real set
K190(TM,(- cTM)) is V83() real ext-real set
A2 is V83() real ext-real Element of REAL
<*A2*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
n is TopSpace-like TopStruct
the carrier of n is set
bool the carrier of n is non empty set
TM is countable Element of bool the carrier of n
n | TM is strict TopSpace-like SubSpace of n
ind TM is V83() real ext-real integer set
{} n 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 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 n
cTM is non empty TopSpace-like TopStruct
the carrier of cTM is non empty set
bool the carrier of cTM is non empty set
A is non empty Element of bool the carrier of cTM
cTM | A is non empty strict TopSpace-like SubSpace of cTM
the carrier of (cTM | A) is non empty set
bool the carrier of (cTM | A) is non empty set
bool (bool the carrier of (cTM | A)) is non empty set
{ H₁(b₁) where b₁ is Element of the carrier of (cTM | A) : S₂[b₁] } is set
A2 is Element of bool (bool the carrier of (cTM | A))
A12 is Element of bool the carrier of (cTM | A)
ind A12 is V83() real ext-real integer set
T912 is Element of the carrier of (cTM | A)
{T912} is non empty trivial finite 1 -element countable with_finite_small_inductive_dimension Element of bool the carrier of (cTM | A)
card H₁(T912) 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
1 + 0 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
ind H₁(T912) is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
ind A2 is V83() real ext-real integer set
[#] (cTM | A) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (cTM | A)
union A2 is Element of bool the carrier of (cTM | A)
A12 is set
{A12} is non empty trivial finite 1 -element countable set
A12 is Element of bool the carrier of (cTM | A)
T912 is Element of the carrier of (cTM | A)
{T912} is non empty trivial finite 1 -element countable with_finite_small_inductive_dimension Element of bool the carrier of (cTM | A)
card TM is ordinal cardinal set
card { H₁(b₁) where b₁ is Element of the carrier of (cTM | A) : S₂[b₁] } is ordinal cardinal set
card A2 is ordinal cardinal set
ind (cTM | A) is V83() real ext-real integer set
ind ([#] (cTM | A)) is V83() real ext-real integer set
{} n 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 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 n
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
n | TM is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
TOP-REAL 0 is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() L20()
ind (TOP-REAL 0) is V83() real ext-real integer set
[#] (TOP-REAL 0) is non empty non proper non proper open open closed closed F_sigma F_sigma G_delta G_delta Borel Borel dense dense non boundary non boundary V224( TOP-REAL 0) a_component convex Element of bool the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is non empty set
bool the carrier of (TOP-REAL 0) is non empty set
ind ([#] (TOP-REAL 0)) is V83() real ext-real integer set
the topology of (TOP-REAL 0) is non empty Element of bool (bool the carrier of (TOP-REAL 0))
bool (bool the carrier of (TOP-REAL 0)) is non empty set
TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) is non empty strict TopSpace-like second-countable Lindelof TopStruct
Euclid 0 is non empty strict Reflexive discerning V236() triangle MetrStruct
REAL 0 is non empty FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
Pitag_dist 0 is Relation-like [:(REAL 0),(REAL 0):] -defined REAL -valued Function-like V18([:(REAL 0),(REAL 0):], REAL ) complex-yielding V199() V200() Element of bool [:[:(REAL 0),(REAL 0):],REAL:]
[:(REAL 0),(REAL 0):] is non empty Relation-like set
[:[:(REAL 0),(REAL 0):],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[:(REAL 0),(REAL 0):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL 0),(Pitag_dist 0) #) is strict MetrStruct
TopSpaceMetr (Euclid 0) is non empty strict TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid 0) is non empty set
Family_open_set (Euclid 0) is Element of bool (bool the carrier of (Euclid 0))
bool the carrier of (Euclid 0) is non empty set
bool (bool the carrier of (Euclid 0)) is non empty set
TopStruct(# the carrier of (Euclid 0),(Family_open_set (Euclid 0)) #) is non empty strict TopStruct
<*> REAL is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
{(<*> REAL)} is non empty trivial functional finite 1 -element with_common_domain countable ([:NAT,REAL:]) Element of bool (bool [:NAT,REAL:])
bool (bool [:NAT,REAL:]) is non empty non trivial non finite set
card {(<*> REAL)} 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
ind (TOP-REAL 1) is V83() real ext-real integer set
[#] (TOP-REAL 1) is non empty non proper non proper open open closed closed F_sigma F_sigma G_delta G_delta Borel Borel dense dense non boundary non boundary V224( TOP-REAL 1) a_component convex Element of bool the carrier of (TOP-REAL 1)
ind ([#] (TOP-REAL 1)) is V83() real ext-real integer set
1 - 1 is V83() real ext-real set
K194(1,1) is V83() real ext-real integer set
TM is non empty trivial finite 1 -element countable V200() FinSequence-like Element of the carrier of (TOP-REAL 1)
cTM is open Element of bool the carrier of (TOP-REAL 1)
the carrier of (TopSpaceMetr (Euclid 1)) is non empty set
the topology of (TopSpaceMetr (Euclid 1)) is non empty Element of bool (bool the carrier of (TopSpaceMetr (Euclid 1)))
bool the carrier of (TopSpaceMetr (Euclid 1)) is non empty set
bool (bool the carrier of (TopSpaceMetr (Euclid 1))) is non empty set
TopStruct(# the carrier of (TopSpaceMetr (Euclid 1)), the topology of (TopSpaceMetr (Euclid 1)) #) is non empty strict TopSpace-like TopStruct
A2 is Element of bool the carrier of (TopSpaceMetr (Euclid 1))
A is Element of the carrier of (Euclid 1)
A12 is V83() real ext-real set
Ball (A,A12) is Element of bool the carrier of (Euclid 1)
T912 is open Element of bool the carrier of (TOP-REAL 1)
Fr T912 is closed boundary nowhere_dense Element of bool the carrier of (TOP-REAL 1)
Cl T912 is closed Element of bool the carrier of (TOP-REAL 1)
T912 ` is closed Element of bool the carrier of (TOP-REAL 1)
the carrier of (TOP-REAL 1) \ T912 is set
Cl (T912 `) is closed Element of bool the carrier of (TOP-REAL 1)
(Cl T912) /\ (Cl (T912 `)) is closed Element of bool the carrier of (TOP-REAL 1)
ind (Fr T912) is V83() real ext-real integer set
A19 is V83() real ext-real Element of REAL
<*A19*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
Ball (TM,A12) is Element of bool the carrier of (TOP-REAL 1)
A19 - A12 is V83() real ext-real set
K194(A19,A12) is V83() real ext-real set
<*(A19 - A12)*> is Relation-like Function-like set
A19 + A12 is V83() real ext-real set
K190(A19,A12) is V83() real ext-real set
<*(A19 + A12)*> is Relation-like Function-like set
{<*(A19 - A12)*>,<*(A19 + A12)*>} is non empty functional finite countable set
[: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):] is non empty Relation-like set
[:[: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):],REAL:] is non empty non trivial non finite set
A29 is Relation-like [: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):] -defined REAL -valued Function-like V18([: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):], REAL ) complex-yielding V199() V200() Element of bool [:[: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):],REAL:]
SpaceMetr ( the carrier of (TOP-REAL 1),A29) is strict Reflexive discerning V236() triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of (TOP-REAL 1),A29)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of (TOP-REAL 1),A29)))
the carrier of (SpaceMetr ( the carrier of (TOP-REAL 1),A29)) is set
bool the carrier of (SpaceMetr ( the carrier of (TOP-REAL 1),A29)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of (TOP-REAL 1),A29))) is non empty set
(TOP-REAL 1) | (Fr T912) is strict TopSpace-like SubSpace of TOP-REAL 1
<*0*> is Relation-like NAT -defined NAT -valued Function-like complex-yielding V199() V200() V201() FinSequence-like FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like complex-yielding V199() V200() V201() FinSequence-like FinSequence of NAT
TM is Element of the carrier of (Euclid 1)
Ball (TM,1) is Element of bool the carrier of (Euclid 1)
A is non empty trivial finite 1 -element countable V200() FinSequence-like Element of the carrier of (TOP-REAL 1)
Ball (A,1) is Element of bool the carrier of (TOP-REAL 1)
1 + 0 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 open Element of bool the carrier of (TOP-REAL 1)
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
A2 is open Element of bool the carrier of (TOP-REAL 1)
Fr A2 is closed boundary nowhere_dense Element of bool the carrier of (TOP-REAL 1)
Cl A2 is closed Element of bool the carrier of (TOP-REAL 1)
A2 ` is closed Element of bool the carrier of (TOP-REAL 1)
the carrier of (TOP-REAL 1) \ A2 is set
Cl (A2 `) is closed Element of bool the carrier of (TOP-REAL 1)
(Cl A2) /\ (Cl (A2 `)) is closed Element of bool the carrier of (TOP-REAL 1)
ind (Fr A2) is V83() real ext-real integer set
{} (TOP-REAL 1) 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 F_sigma G_delta Borel 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 (TOP-REAL 1)
A2 \/ (A2 `) is Element of bool the carrier of (TOP-REAL 1)
0 + 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
{ <*b₁*> where b₁ is V83() real ext-real Element of REAL : ( not b₁ <= 0 - 1 & not 0 + 1 <= b₁ ) } is set
cTM is Element of the carrier of (Euclid 1)
A12 is V83() real ext-real Element of REAL
<*A12*> is Relation-like NAT -defined REAL -valued Function-like complex-yielding V199() V200() FinSequence-like FinSequence of REAL
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TOP-REAL n is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() L20()
ind (TOP-REAL n) is V83() real ext-real integer set
[#] (TOP-REAL n) is non empty non proper non proper open open closed closed F_sigma F_sigma G_delta G_delta Borel Borel dense dense non boundary non boundary V224( TOP-REAL n) convex Element of bool the carrier of (TOP-REAL n)
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
ind ([#] (TOP-REAL n)) is V83() real ext-real integer set
TM is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TOP-REAL TM is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() L20()
ind (TOP-REAL TM) is V83() real ext-real integer set
[#] (TOP-REAL TM) is non empty non proper non proper open open closed closed F_sigma F_sigma G_delta G_delta Borel Borel dense dense non boundary non boundary V224( TOP-REAL TM) convex Element of bool the carrier of (TOP-REAL TM)
the carrier of (TOP-REAL TM) is non empty set
bool the carrier of (TOP-REAL TM) is non empty set
ind ([#] (TOP-REAL TM)) is V83() real ext-real 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
TOP-REAL (TM + 1) is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() L20()
ind (TOP-REAL (TM + 1)) is V83() real ext-real integer set
[#] (TOP-REAL (TM + 1)) is non empty non proper non proper open open closed closed F_sigma F_sigma G_delta G_delta Borel Borel dense dense non boundary non boundary V224( TOP-REAL (TM + 1)) a_component convex Element of bool the carrier of (TOP-REAL (TM + 1))
the carrier of (TOP-REAL (TM + 1)) is non empty set
bool the carrier of (TOP-REAL (TM + 1)) is non empty set
ind ([#] (TOP-REAL (TM + 1))) is V83() real ext-real integer set
the topology of (TOP-REAL TM) is non empty Element of bool (bool the carrier of (TOP-REAL TM))
bool (bool the carrier of (TOP-REAL TM)) is non empty set
TopStruct(# the carrier of (TOP-REAL TM), the topology of (TOP-REAL TM) #) is non empty strict TopSpace-like second-countable Lindelof TopStruct
Euclid TM is non empty strict Reflexive discerning V236() triangle MetrStruct
REAL TM is non empty FinSequence-membered FinSequenceSet of REAL
TM -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
Pitag_dist TM is Relation-like [:(REAL TM),(REAL TM):] -defined REAL -valued Function-like V18([:(REAL TM),(REAL TM):], REAL ) complex-yielding V199() V200() Element of bool [:[:(REAL TM),(REAL TM):],REAL:]
[:(REAL TM),(REAL TM):] is non empty Relation-like set
[:[:(REAL TM),(REAL TM):],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[:(REAL TM),(REAL TM):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL TM),(Pitag_dist TM) #) is strict MetrStruct
TopSpaceMetr (Euclid TM) is non empty strict TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid TM) is non empty set
Family_open_set (Euclid TM) is Element of bool (bool the carrier of (Euclid TM))
bool the carrier of (Euclid TM) is non empty set
bool (bool the carrier of (Euclid TM)) is non empty set
TopStruct(# the carrier of (Euclid TM),(Family_open_set (Euclid TM)) #) is non empty strict TopStruct
the topology of (TOP-REAL (TM + 1)) is non empty Element of bool (bool the carrier of (TOP-REAL (TM + 1)))
bool (bool the carrier of (TOP-REAL (TM + 1))) is non empty set
TopStruct(# the carrier of (TOP-REAL (TM + 1)), the topology of (TOP-REAL (TM + 1)) #) is non empty strict TopSpace-like second-countable Lindelof TopStruct
Euclid (TM + 1) is non empty strict Reflexive discerning V236() triangle MetrStruct
REAL (TM + 1) is non empty FinSequence-membered FinSequenceSet of REAL
(TM + 1) -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
Pitag_dist (TM + 1) is Relation-like [:(REAL (TM + 1)),(REAL (TM + 1)):] -defined REAL -valued Function-like V18([:(REAL (TM + 1)),(REAL (TM + 1)):], REAL ) complex-yielding V199() V200() Element of bool [:[:(REAL (TM + 1)),(REAL (TM + 1)):],REAL:]
[:(REAL (TM + 1)),(REAL (TM + 1)):] is non empty Relation-like set
[:[:(REAL (TM + 1)),(REAL (TM + 1)):],REAL:] is non empty non trivial Relation-like non finite complex-yielding V199() V200() set
bool [:[:(REAL (TM + 1)),(REAL (TM + 1)):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL (TM + 1)),(Pitag_dist (TM + 1)) #) is strict MetrStruct
TopSpaceMetr (Euclid (TM + 1)) is non empty strict TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 T_1/2 metrizable TopStruct
the carrier of (Euclid (TM + 1)) is non empty set
Family_open_set (Euclid (TM + 1)) is Element of bool (bool the carrier of (Euclid (TM + 1)))
bool the carrier of (Euclid (TM + 1)) is non empty set
bool (bool the carrier of (Euclid (TM + 1))) is non empty set
TopStruct(# the carrier of (Euclid (TM + 1)),(Family_open_set (Euclid (TM + 1))) #) is non empty strict TopStruct
[:(TopSpaceMetr (Euclid TM)),(TopSpaceMetr (Euclid 1)):] is non empty strict TopSpace-like T_0 T_1 T_2 V59() normal T_3 T_4 T_1/2 metrizable TopStruct
ind (TopSpaceMetr (Euclid 1)) is V83() real ext-real integer set
[#] (TopSpaceMetr (Euclid 1)) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr (Euclid 1))
the carrier of (TopSpaceMetr (Euclid 1)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid 1)) is non empty set
ind ([#] (TopSpaceMetr (Euclid 1))) is V83() real ext-real integer set
ind (TopSpaceMetr (Euclid TM)) is V83() real ext-real integer set
[#] (TopSpaceMetr (Euclid TM)) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr (Euclid TM))
the carrier of (TopSpaceMetr (Euclid TM)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid TM)) is non empty set
ind ([#] (TopSpaceMetr (Euclid TM))) is V83() real ext-real integer set
ind [:(TopSpaceMetr (Euclid TM)),(TopSpaceMetr (Euclid 1)):] is V83() real ext-real integer set
[#] [:(TopSpaceMetr (Euclid TM)),(TopSpaceMetr (Euclid 1)):] is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of [:(TopSpaceMetr (Euclid TM)),(TopSpaceMetr (Euclid 1)):]
the carrier of [:(TopSpaceMetr (Euclid TM)),(TopSpaceMetr (Euclid 1)):] is non empty set
bool the carrier of [:(TopSpaceMetr (Euclid TM)),(TopSpaceMetr (Euclid 1)):] is non empty set
ind ([#] [:(TopSpaceMetr (Euclid TM)),(TopSpaceMetr (Euclid 1)):]) is V83() real ext-real integer set
(ind (TopSpaceMetr (Euclid TM))) + 1 is V83() real ext-real set
K190((ind (TopSpaceMetr (Euclid TM))),1) is V83() real ext-real integer set
ind (TopSpaceMetr (Euclid (TM + 1))) is V83() real ext-real integer set
[#] (TopSpaceMetr (Euclid (TM + 1))) is non empty non proper open closed F_sigma G_delta Borel dense non boundary Element of bool the carrier of (TopSpaceMetr (Euclid (TM + 1)))
the carrier of (TopSpaceMetr (Euclid (TM + 1))) is non empty set
bool the carrier of (TopSpaceMetr (Euclid (TM + 1))) is non empty set
ind ([#] (TopSpaceMetr (Euclid (TM + 1)))) is V83() real ext-real integer set
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TOP-REAL n is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() L20()
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TOP-REAL n is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() with_finite_small_inductive_dimension L20()
ind (TOP-REAL n) is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
[#] (TOP-REAL n) is non empty non proper non proper open open closed closed F_sigma F_sigma G_delta G_delta Borel Borel dense dense non boundary non boundary V224( TOP-REAL n) with_finite_small_inductive_dimension convex Element of bool the carrier of (TOP-REAL n)
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
ind ([#] (TOP-REAL n)) is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
n is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
TOP-REAL n is non empty TopSpace-like V253() V278() V279() V280() V281() V282() V283() V284() V290() V291() V292() with_finite_small_inductive_dimension L20()
ind (TOP-REAL n) is ordinal natural finite cardinal V83() real ext-real non negative countable integer set
[#] (TOP-REAL n) is non empty non proper non proper open open closed closed F_sigma F_sigma G_delta G_delta Borel Borel dense dense non boundary non boundary V224( TOP-REAL n) with_finite_small_inductive_dimension convex Element of bool the carrier of (TOP-REAL n)
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
ind ([#] (TOP-REAL n)) is ordinal natural finite cardinal V83() real ext-real non negative countable 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 with_finite_small_inductive_dimension Element of bool the carrier of n
n | TM is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 with_finite_small_inductive_dimension metrizable SubSpace of n
ind (n | TM) is V83() real ext-real integer set
[#] (n | TM) is non proper open closed F_sigma G_delta dense with_finite_small_inductive_dimension Element of bool the carrier of (n | TM)
the carrier of (n | TM) is set
bool the carrier of (n | TM) is non empty set
ind ([#] (n | TM)) is V83() real ext-real integer set
cTM is open F_sigma Element of bool the carrier of n
A is open F_sigma Element of bool the carrier of n
cTM \/ A is open F_sigma 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
[#] (n | (cTM \/ A)) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (n | (cTM \/ A))
the carrier of (n | (cTM \/ A)) is set
bool the carrier of (n | (cTM \/ A)) is non empty set
A19 is Element of bool the carrier of (n | (cTM \/ A))
A12 is Element of bool the carrier of (n | (cTM \/ A))
A12 ` is Element of bool the carrier of (n | (cTM \/ A))
the carrier of (n | (cTM \/ A)) \ A12 is set
T912 is Element of bool the carrier of (n | (cTM \/ A))
T912 ` is Element of bool the carrier of (n | (cTM \/ A))
the carrier of (n | (cTM \/ A)) \ T912 is set
A29 is set
A /\ (cTM \/ A) is open F_sigma Element of bool the carrier of n
cTM /\ (cTM \/ A) is open F_sigma Element of bool the carrier of n
ind A19 is V83() real ext-real integer set
ind TM is V83() real ext-real integer set
(n | (cTM \/ A)) | A19 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n | (cTM \/ A)
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
A29 is Element of bool the carrier of (n | (cTM \/ A))
A29 /\ A19 is Element of bool the carrier of (n | (cTM \/ A))
ind (A29 /\ A19) is V83() real ext-real integer set
A9 is open F_sigma Element of bool the carrier of (n | (cTM \/ A))
A29 is open F_sigma Element of bool the carrier of (n | (cTM \/ A))
A9 \/ A29 is open F_sigma Element of bool the carrier of (n | (cTM \/ A))
(A9 \/ A29) ` is closed G_delta Element of bool the carrier of (n | (cTM \/ A))
the carrier of (n | (cTM \/ A)) \ (A9 \/ A29) is set
A19 is Element of bool the carrier of n
L is Element of bool the carrier of n
W is open F_sigma Element of bool the carrier of n
U is open F_sigma Element of bool the carrier of n
W \/ U is open F_sigma Element of bool the carrier of n
- 1 is non empty V83() real ext-real non positive negative set
K192(1) is V83() real ext-real non positive 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
bool (bool the carrier of n) is non empty set
bool the carrier of n is non empty Element of bool (bool the carrier of n)
TM is Element of bool the carrier of n
n | TM is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
ind TM is V83() real ext-real integer set
cTM is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
[:cTM,(bool the carrier of n):] is Relation-like set
bool [:cTM,(bool the carrier of n):] is non empty set
A is ordinal natural finite cardinal V83() real ext-real non negative countable 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
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
ind A1 is V83() real ext-real integer set
A2 is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
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
[:A2,(bool the carrier of n):] is Relation-like set
bool [:A2,(bool the carrier of n):] is non empty set
A12 is set
{A12} is non empty trivial finite 1 -element countable set
A2 --> A12 is Relation-like A2 -defined {A12} -valued Function-like V18(A2,{A12}) finite countable Element of bool [:A2,{A12}:]
[:A2,{A12}:] is Relation-like finite countable set
bool [:A2,{A12}:] is non empty finite V32() countable set
dom (A2 --> A12) is finite countable Element of bool A2
bool A2 is non empty finite V32() countable set
rng (A2 --> A12) is trivial finite countable Element of bool {A12}
bool {A12} is non empty finite V32() countable set
A19 is Relation-like A2 -defined bool the carrier of n -valued Function-like V18(A2, bool the carrier of n) finite countable Element of bool [:A2,(bool the carrier of n):]
rng A19 is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty set
A29 is set
A19 . A29 is set
A29 is set
A9 is set
A19 . A29 is set
A19 . A9 is set
A - 1 is V83() real ext-real set
K194(A,1) is V83() real ext-real integer set
T912 is set
{T912} is non empty trivial finite 1 -element countable set
A2 \ {T912} is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
card (A2 \ {T912}) 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 ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
A12 + 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 set
A29 is open F_sigma Element of bool the carrier of n
{A29} is non empty trivial finite 1 -element countable ( the carrier of n) Element of bool (bool the carrier of n)
A9 is open F_sigma Element of bool the carrier of n
A29 \/ A9 is open F_sigma Element of bool the carrier of n
{A9} is non empty trivial finite 1 -element countable ( the carrier of n) Element of bool (bool the carrier of n)
{(A29 \/ A9)} is non empty trivial finite 1 -element countable ( the carrier of n) Element of bool (bool the carrier of n)
A2 \ {A29} is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
(A2 \ {A29}) \/ {A29} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
(A2 \ {A29}) \ {A9} is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
card ((A2 \ {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
((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
card {(A29 \/ A9)} 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 (((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}) 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 \ {A29}) \ {A9}) \/ {A9} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
U9 is Element of bool the carrier of n
[:((A2 \ {A29}) \ {A9}),(bool the carrier of n):] is Relation-like set
bool [:((A2 \ {A29}) \ {A9}),(bool the carrier of n):] is non empty set
U9 is Relation-like (A2 \ {A29}) \ {A9} -defined bool the carrier of n -valued Function-like V18((A2 \ {A29}) \ {A9}, bool the carrier of n) finite countable Element of bool [:((A2 \ {A29}) \ {A9}),(bool the carrier of n):]
rng U9 is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty set
union (rng U9) is Element of bool the carrier of n
{} n 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 n
(A29,A9) --> (({} n),({} n)) is Relation-like {A29,A9} -defined bool the carrier of n -valued Function-like V18({A29,A9}, bool the carrier of n) finite countable Element of bool [:{A29,A9},(bool the carrier of n):]
{A29,A9} is non empty finite countable set
[:{A29,A9},(bool the carrier of n):] is non empty Relation-like set
bool [:{A29,A9},(bool the carrier of n):] is non empty set
dom ((A29,A9) --> (({} n),({} n))) is finite countable Element of bool {A29,A9}
bool {A29,A9} is non empty finite V32() countable set
{A29,A9} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
rng ((A29,A9) --> (({} n),({} n))) is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
{({} n),({} n)} is non empty functional finite V32() countable V208() V209() V210() V211() V212() V213() ( the carrier of n) Element of bool (bool the carrier of n)
((A2 \ {A29}) \ {A9}) \/ {A29,A9} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
{A9} \/ {A29} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
((A2 \ {A29}) \ {A9}) \/ ({A9} \/ {A29}) is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
(((A2 \ {A29}) \ {A9}) \/ {A9}) \/ {A29} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
dom U9 is finite countable Element of bool ((A2 \ {A29}) \ {A9})
bool ((A2 \ {A29}) \ {A9}) is non empty finite V32() countable set
U9 +* ((A29,A9) --> (({} n),({} n))) is Relation-like Function-like finite countable set
proj2 (U9 +* ((A29,A9) --> (({} n),({} n)))) is finite countable set
(rng U9) \/ (rng ((A29,A9) --> (({} n),({} n)))) is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
proj1 (U9 +* ((A29,A9) --> (({} n),({} n)))) is finite countable set
U9 is Relation-like A2 -defined bool the carrier of n -valued Function-like V18(A2, bool the carrier of n) finite countable Element of bool [:A2,(bool the carrier of n):]
rng U9 is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
((A29,A9) --> (({} n),({} n))) . A9 is set
U9 . A9 is set
W9 is Element of bool the carrier of n
union (rng U9) is Element of bool the carrier of n
union (rng ((A29,A9) --> (({} n),({} n)))) is Element of bool the carrier of n
(union (rng U9)) \/ (union (rng ((A29,A9) --> (({} n),({} n))))) is Element of bool the carrier of n
{({} n)} is non empty trivial functional finite V32() 1 -element with_common_domain countable V208() V209() V210() V211() V212() V213() ( the carrier of n) Element of bool (bool the carrier of n)
union {({} n)} is finite countable with_finite_small_inductive_dimension Element of bool the carrier of n
(union (rng U9)) \/ (union {({} n)}) is Element of bool the carrier of n
(union (rng U9)) \/ ({} n) is Element of bool the carrier of n
((A29,A9) --> (({} n),({} n))) . A29 is set
U9 . A29 is set
W9 is set
U9 . W9 is set
U9 . W9 is set
U9 . W9 is set
W9 is set
X2 is set
U9 . W9 is set
U9 . X2 is set
U9 . W9 is set
U9 . X2 is set
union ((A2 \ {A29}) \ {A9}) is Element of bool the carrier of n
(union ((A2 \ {A29}) \ {A9})) \/ (A29 \/ A9) is Element of bool the carrier of n
union {(A29 \/ A9)} is Element of bool the carrier of n
(union ((A2 \ {A29}) \ {A9})) \/ (union {(A29 \/ A9)}) is Element of bool the carrier of n
union (((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}) is Element of bool the carrier of n
union A2 is Element of bool the carrier of n
union (A2 \ {A29}) is Element of bool the carrier of n
union {A29} is Element of bool the carrier of n
(union (A2 \ {A29})) \/ (union {A29}) is Element of bool the carrier of n
(union (A2 \ {A29})) \/ A29 is Element of bool the carrier of n
union {A9} is Element of bool the carrier of n
(union ((A2 \ {A29}) \ {A9})) \/ (union {A9}) is Element of bool the carrier of n
((union ((A2 \ {A29}) \ {A9})) \/ (union {A9})) \/ A29 is Element of bool the carrier of n
(union ((A2 \ {A29}) \ {A9})) \/ A9 is Element of bool the carrier of n
((union ((A2 \ {A29}) \ {A9})) \/ A9) \/ A29 is Element of bool the carrier of n
A9 \/ A29 is open F_sigma Element of bool the carrier of n
(union ((A2 \ {A29}) \ {A9})) \/ (A9 \/ A29) is Element of bool the carrier of n
[:(((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}),(bool the carrier of n):] is non empty Relation-like set
bool [:(((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}),(bool the carrier of n):] is non empty set
U9 is Relation-like ((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)} -defined bool the carrier of n -valued Function-like V18(((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}, bool the carrier of n) finite countable Element of bool [:(((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}),(bool the carrier of n):]
rng U9 is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty set
U9 | ((A2 \ {A29}) \ {A9}) is Relation-like (A2 \ {A29}) \ {A9} -defined ((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)} -defined bool the carrier of n -valued Function-like finite countable Element of bool [:(((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}),(bool the carrier of n):]
rng (U9 | ((A2 \ {A29}) \ {A9})) is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
U9 . (A29 \/ A9) is set
dom U9 is finite countable Element of bool (((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)})
bool (((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}) is non empty finite V32() countable set
dom (U9 | ((A2 \ {A29}) \ {A9})) is finite countable Element of bool (((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)})
(((A2 \ {A29}) \ {A9}) \/ {(A29 \/ A9)}) /\ ((A2 \ {A29}) \ {A9}) is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
W9 is open F_sigma Element of bool the carrier of n
W9 /\ A1 is Element of bool the carrier 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
W9 is Element of bool the carrier of (n | A1)
(n | A1) | W9 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n | A1
n | (W9 /\ A1) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
ind (W9 /\ A1) is V83() real ext-real integer set
ind (n | (W9 /\ A1)) is V83() real ext-real integer set
[#] (n | (W9 /\ A1)) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (n | (W9 /\ A1))
the carrier of (n | (W9 /\ A1)) is set
bool the carrier of (n | (W9 /\ A1)) is non empty set
ind ([#] (n | (W9 /\ A1))) is V83() real ext-real integer set
ind W9 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
X2 is open F_sigma Element of bool the carrier of n
X1 is open F_sigma Element of bool the carrier of n
X2 \/ X1 is open F_sigma Element of bool the carrier of n
W9 /\ X2 is open F_sigma Element of bool the carrier of n
W9 /\ X1 is open F_sigma Element of bool the carrier of n
gV1 is open F_sigma Element of bool the carrier of n
gV2 is open F_sigma Element of bool the carrier of n
(A29,A9) --> (gV1,gV2) is Relation-like {A29,A9} -defined bool the carrier of n -valued Function-like V18({A29,A9}, bool the carrier of n) finite countable Element of bool [:{A29,A9},(bool the carrier of n):]
{A29,A9} is non empty finite countable set
[:{A29,A9},(bool the carrier of n):] is non empty Relation-like set
bool [:{A29,A9},(bool the carrier of n):] is non empty set
dom ((A29,A9) --> (gV1,gV2)) is finite countable Element of bool {A29,A9}
bool {A29,A9} is non empty finite V32() countable set
{A29,A9} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
(U9 | ((A2 \ {A29}) \ {A9})) +* ((A29,A9) --> (gV1,gV2)) is Relation-like Function-like finite countable set
proj1 ((U9 | ((A2 \ {A29}) \ {A9})) +* ((A29,A9) --> (gV1,gV2))) is finite countable set
((A2 \ {A29}) \ {A9}) \/ {A29,A9} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
{A9} \/ {A29} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
((A2 \ {A29}) \ {A9}) \/ ({A9} \/ {A29}) is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
(((A2 \ {A29}) \ {A9}) \/ {A9}) \/ {A29} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
{gV1,gV2} is non empty finite countable ( the carrier of n) Element of bool (bool the carrier of n)
gh is Element of bool the carrier of n
proj2 ((U9 | ((A2 \ {A29}) \ {A9})) +* ((A29,A9) --> (gV1,gV2))) is finite countable set
rng ((A29,A9) --> (gV1,gV2)) is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
(rng (U9 | ((A2 \ {A29}) \ {A9}))) \/ (rng ((A29,A9) --> (gV1,gV2))) is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
gh is Relation-like A2 -defined bool the carrier of n -valued Function-like V18(A2, bool the carrier of n) finite countable Element of bool [:A2,(bool the carrier of n):]
dom gh is finite countable Element of bool A2
bool A2 is non empty finite V32() countable set
rng gh is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
((A29,A9) --> (gV1,gV2)) . A29 is set
gh . A29 is set
((A29,A9) --> (gV1,gV2)) . A9 is set
gh . A9 is set
a is set
b is set
gh . a is set
gh . b is set
(U9 | ((A2 \ {A29}) \ {A9})) . a is set
U9 . a is set
Gx is set
union (rng gh) is Element of bool the carrier of n
a is set
union (rng U9) is Element of bool the carrier of n
b is set
Gx is set
U9 . Gx is set
(U9 | ((A2 \ {A29}) \ {A9})) . Gx is set
gh . Gx is set
a is set
(U9 | ((A2 \ {A29}) \ {A9})) . a is set
U9 . a is set
gh . a is set
gh . a is set
a is set
b is set
gh . a is set
gh . b is set
(U9 | ((A2 \ {A29}) \ {A9})) . a is set
U9 . a is set
(U9 | ((A2 \ {A29}) \ {A9})) . b is set
U9 . b is set
A is Element of bool the carrier of n
n | A is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
ind A is V83() real ext-real integer set
A1 is finite countable ( the carrier of n) Element of bool (bool the carrier of 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
[:A1,(bool the carrier of n):] is Relation-like set
bool [:A1,(bool the carrier of n):] is non empty set
rng {} 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 with_non-empty_elements 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() Element of bool REAL
proj1 {} 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
A2 is Relation-like A1 -defined bool the carrier of n -valued Function-like V18(A1, bool the carrier of n) finite countable Element of bool [:A1,(bool the carrier of n):]
rng A2 is finite countable ( the carrier of n) Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty set
A12 is set
A2 . A12 is set
T912 is set
A19 is set
A2 . T912 is set
A2 . A19 is 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
A is Element of bool the carrier of n
n | A is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of n
ind A is V83() real ext-real integer set
A1 is finite countable ( the carrier of n) Element of bool (bool the carrier of 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
[:A1,(bool the carrier of n):] is Relation-like set
bool [:A1,(bool the carrier of n):] is non empty 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 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
cTM is V83() real ext-real integer set
cTM + 1 is V83() real ext-real set
K190(cTM,1) is V83() real ext-real integer set
A is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
ind A is V83() real ext-real 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
A2 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
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
(card A2) * (n + 1) is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
(n + 1) * (card A2) is ordinal natural finite cardinal V83() real ext-real non negative countable integer V197() V208() V209() V210() V211() V212() V213() Element of NAT
card ((n + 1) * (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
card (card ((n + 1) * (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
bool the carrier of TM is non empty Element of bool (bool the carrier of TM)
[:A2,(bool the carrier of TM):] is Relation-like set
bool [:A2,(bool the carrier of TM):] is non empty 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
A12 is set
T912 is Element of bool the carrier of TM
TM | T912 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
union A2 is Element of bool the carrier of TM
ind T912 is V83() real ext-real integer set
A19 is Relation-like A2 -defined bool the carrier of TM -valued Function-like V18(A2, bool the carrier of TM) finite countable Element of bool [:A2,(bool the carrier of TM):]
rng A19 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
A29 is Element of bool the carrier of TM
[:A,(bool (bool the carrier of TM)):] is Relation-like set
bool [:A,(bool (bool the carrier of TM)):] is non empty set
A12 is Relation-like A -defined bool (bool the carrier of TM) -valued Function-like V18(A, bool (bool the carrier of TM)) finite countable Element of bool [:A,(bool (bool the carrier of TM)):]
rng A12 is finite countable ( bool the carrier of TM) Element of bool (bool (bool the carrier of TM))
bool (bool (bool the carrier of TM)) is non empty set
union (rng A12) is Element of bool (bool the carrier of TM)
union (bool (bool the carrier of TM)) is Element of bool (bool the carrier of TM)
Union A12 is set
proj2 A12 is finite countable set
union (proj2 A12) is set
dom A12 is finite countable Element of bool A
bool A is non empty finite V32() countable set
A19 is set
A12 . A19 is Element of bool (bool the carrier of TM)
card (A12 . A19) is ordinal cardinal set
A29 is Element of bool the carrier of TM
A9 is Relation-like A2 -defined bool the carrier of TM -valued Function-like V18(A2, bool the carrier of TM) finite countable Element of bool [:A2,(bool the carrier of TM):]
rng A9 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
dom A9 is finite countable Element of bool A2
bool A2 is non empty finite V32() countable set
card (dom 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 Element of bool (bool the carrier of TM)
card T912 is ordinal cardinal set
(n + 1) *` (card A2) 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
card (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
A19 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
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
( the carrier of TM,A19) is V83() real ext-real integer set
A29 is Element of bool the carrier of TM
A9 is set
A29 is set
A12 . A29 is Element of bool (bool the carrier of TM)
A19 is Relation-like A2 -defined bool the carrier of TM -valued Function-like V18(A2, bool the carrier of TM) finite countable Element of bool [:A2,(bool the carrier of TM):]
rng A19 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
union A19 is Element of bool the carrier of TM
union A is Element of bool the carrier of TM
A29 is set
A9 is set
A12 . A9 is Element of bool (bool the carrier of TM)
A29 is Relation-like A2 -defined bool the carrier of TM -valued Function-like V18(A2, bool the carrier of TM) finite countable Element of bool [:A2,(bool the carrier of TM):]
rng A29 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
union (rng A29) is Element of bool the carrier of TM
A19 is set
A29 is set
A9 is set
A29 is set
A12 . A29 is Element of bool (bool the carrier of TM)
A19 is Relation-like A2 -defined bool the carrier of TM -valued Function-like V18(A2, bool the carrier of TM) finite countable Element of bool [:A2,(bool the carrier of TM):]
rng A19 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
dom A19 is finite countable Element of bool A2
bool A2 is non empty finite V32() countable set
L is set
A19 . L is set
A29 is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
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
A9 is set
A29 is set
A19 is set
L is set
A12 . L is Element of bool (bool the carrier of TM)
[:A29,A:] is Relation-like finite countable set
bool [:A29,A:] is non empty finite V32() countable set
A29 is Relation-like A29 -defined A -valued Function-like V18(A29,A) finite countable Element of bool [:A29,A:]
dom A29 is finite countable Element of bool A29
bool A29 is non empty finite V32() countable set
A19 is set
A12 . A19 is Element of bool (bool the carrier of TM)
meet A29 is Element of bool the carrier of TM
A19 is set
L is set
U is set
A29 . L is set
A29 . U is set
rng A29 is finite countable Element of bool A
A12 . (A29 . L) is Element of bool (bool the carrier of TM)
W is Relation-like A2 -defined bool the carrier of TM -valued Function-like V18(A2, bool the carrier of TM) finite countable Element of bool [:A2,(bool the carrier of TM):]
rng W is finite countable ( the carrier of TM) Element of bool (bool the carrier of TM)
dom W is finite countable Element of bool A2
bool A2 is non empty finite V32() countable set
L9 is set
W . L9 is set
U9 is set
W . U9 is set
rng A29 is finite countable Element of bool A
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 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
[#] TM is non proper open closed F_sigma G_delta dense Element of bool the carrier of TM
A is Element of bool the carrier of TM
A ` is Element of bool the carrier of TM
the carrier of TM \ A is set
ind (A `) is V83() real ext-real integer set
TM | (A `) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
A1 is closed G_delta Element of bool the carrier of TM
A2 is closed G_delta Element of bool the carrier of TM
A1 \/ A2 is closed G_delta Element of bool the carrier of TM
A1 /\ A2 is closed G_delta Element of bool the carrier of TM
([#] TM) \ (A1 /\ A2) is Element of bool the carrier of TM
TM | (([#] TM) \ (A1 /\ A2)) is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM
[#] (TM | (([#] TM) \ (A1 /\ A2))) is non proper open closed F_sigma G_delta dense Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
the carrier of (TM | (([#] TM) \ (A1 /\ A2))) is set
bool the carrier of (TM | (([#] TM) \ (A1 /\ A2))) is non empty set
A1 \ (A1 /\ A2) is Element of bool the carrier of TM
A2 \ (A1 /\ A2) is Element of bool the carrier of TM
A2 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) is Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
A2 /\ ([#] TM) is closed G_delta Element of bool the carrier of TM
(A2 /\ ([#] TM)) \ (A1 /\ A2) is Element of bool the carrier of TM
A29 is Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
A1 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) is Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
A1 /\ ([#] TM) is closed G_delta Element of bool the carrier of TM
(A1 /\ ([#] TM)) \ (A1 /\ A2) is Element of bool the carrier of TM
A19 is Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
A1 \ A2 is Element of bool the carrier of TM
A19 is closed G_delta Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
A29 is closed G_delta Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
A9 is Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
ind A9 is V83() real ext-real integer set
(TM | (([#] TM) \ (A1 /\ A2))) | A9 is strict TopSpace-like T_0 T_1 normal T_4 T_1/2 metrizable SubSpace of TM | (([#] TM) \ (A1 /\ A2))
L is Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
L /\ A9 is Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
ind (L /\ A9) is V83() real ext-real integer set
U is open F_sigma Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
W is open F_sigma Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
U \/ W is open F_sigma Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
(U \/ W) ` is closed G_delta Element of bool the carrier of (TM | (([#] TM) \ (A1 /\ A2)))
the carrier of (TM | (([#] TM) \ (A1 /\ A2))) \ (U \/ W) is set
(A1 \ (A1 /\ A2)) \/ (A1 /\ A2) is Element of bool the carrier of TM
(A2 \ (A1 /\ A2)) \/ (A1 /\ A2) is Element of bool the carrier of TM
U9 is set
L9 is Element of bool the carrier of TM
L9 \ A is Element of bool the carrier of TM
L /\ ([#] TM) is Element of bool the carrier of TM
(L /\ ([#] TM)) \ A is Element of bool the carrier of TM
([#] TM) \ (([#] TM) \ (A1 /\ A2)) is Element of bool the carrier of TM
([#] TM) /\ (A1 /\ A2) is closed G_delta Element of bool the carrier of TM
A1 \ (A1 \ (A1 /\ A2)) is Element of bool the carrier of TM
A1 /\ (A1 /\ A2) is closed G_delta Element of bool the carrier of TM
(A1 /\ A2) ` is open F_sigma Element of bool the carrier of TM
the carrier of TM \ (A1 /\ A2) is set
U9 is Element of bool the carrier of TM
W9 is Element of bool the carrier of TM
W9 is open F_sigma Element of bool the carrier of TM
W9 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ W9 is set
X2 is closed G_delta Element of bool the carrier of TM
X2 /\ A2 is closed G_delta Element of bool the carrier of TM
U9 is open F_sigma Element of bool the carrier of TM
U9 ` is closed G_delta Element of bool the carrier of TM
the carrier of TM \ U9 is set
X1 is closed G_delta Element of bool the carrier of TM
X2 \/ X1 is closed G_delta Element of bool the carrier of TM
A1 /\ X1 is closed G_delta Element of bool the carrier of TM
X2 /\ X1 is closed G_delta Element of bool the carrier of TM
(X2 /\ X1) \ (A1 /\ A2) is Element of bool the carrier of TM
ind ((X2 /\ X1) \ (A1 /\ A2)) is V83() real ext-real integer set
([#] TM) \ (U \/ W) is Element of bool the carrier of TM
W \/ (([#] TM) \ (U \/ W)) is set
X1 /\ X2 is closed G_delta Element of bool the carrier of TM
W \/ (X1 /\ X2) is set
W9 \/ X1 is Element of bool the carrier of TM
W \/ X2 is set
(W9 \/ X1) /\ (W \/ X2) is Element of bool the carrier of TM
(W9 \/ X1) /\ ([#] TM) is Element of bool the carrier of TM
X1 /\ ([#] TM) is closed G_delta Element of bool the carrier of TM
U9 /\ W9 is open F_sigma Element of bool the carrier of TM
([#] TM) \ (U9 /\ W9) is Element of bool the carrier of TM
([#] TM) \ {} is Element of bool the carrier of TM
U \/ (([#] TM) \ (U \/ W)) is set
U \/ (X1 /\ X2) is set
U9 \/ X1 is Element of bool the carrier of TM
U \/ X2 is set
(U9 \/ X1) /\ (U \/ X2) is Element of bool the carrier of TM
([#] TM) /\ (U \/ X2) is Element of bool the carrier of TM
([#] TM) /\ X2 is closed G_delta Element of bool the carrier of TM
([#] TM) /\ A1 is closed G_delta Element of bool the carrier of TM
(([#] TM) /\ A1) \ U9 is Element of bool the carrier of TM
A1 \ U9 is Element of bool the carrier of TM
A2 \ (A2 \ (A1 /\ A2)) is Element of bool the carrier of TM
A2 /\ (A1 /\ A2) is closed G_delta Element of bool the carrier of TM
A2 /\ X2 is closed G_delta Element of bool the carrier of TM
([#] TM) /\ A2 is closed G_delta Element of bool the carrier of TM
(([#] TM) /\ A2) \ W9 is Element of bool the carrier of TM
A2 \ W9 is Element of bool the carrier of TM
W9 \/ U9 is open F_sigma Element of bool the carrier of TM
([#] TM) \ (W9 \/ U9) is Element of bool the carrier of TM
(([#] TM) \ (W9 \/ U9)) \ (A1 /\ A2) is Element of bool the carrier of TM
(W9 \/ U9) \/ (A1 /\ A2) is Element of bool the carrier of TM
([#] TM) \ ((W9 \/ U9) \/ (A1 /\ A2)) is Element of bool the carrier of TM