:: 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

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

card { H

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

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

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

((