:: NAGATA_2 semantic presentation

REAL is non empty non trivial non finite V76() V77() V78() V82() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() Element of bool REAL

bool REAL is non empty non trivial non finite set

{} is set

the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() real ext-real non positive non negative finite V49() cardinal {} -element FinSequence-membered V76() V77() V78() V79() V80() V81() V82() set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() real ext-real non positive non negative finite V49() cardinal {} -element FinSequence-membered V76() V77() V78() V79() V80() V81() V82() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

{{},1} is finite set

COMPLEX is non empty non trivial non finite V76() V82() set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() set

bool omega is non empty non trivial non finite set

[:NAT,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is non empty non trivial non finite set

bool (bool REAL) is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

K115(NAT) is V26() set

RAT is non empty non trivial non finite V76() V77() V78() V79() V82() set

INT is non empty non trivial non finite V76() V77() V78() V79() V80() V82() set

[:1,1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

bool [:1,1:] is non empty finite V49() set

[:[:1,1:],1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

bool [:[:1,1:],1:] is non empty finite V49() set

[:[:1,1:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:1,1:],REAL:] is non empty non trivial non finite set

[:REAL,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

[:[:REAL,REAL:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

[:2,2:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

[:[:2,2:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:2,2:],REAL:] is non empty non trivial non finite set

K546() is non empty strict TopSpace-like V162() TopStruct

the carrier of K546() is non empty V76() V77() V78() set

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V162() MetrStruct

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V162() TopStruct

K553() is non empty strict TopSpace-like V162() SubSpace of R^1

[:COMPLEX,COMPLEX:] is non empty non trivial non finite complex-valued set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:COMPLEX,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:COMPLEX,REAL:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite complex-valued set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

bool [:REAL,REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

K680(2) is V222() L15()

the carrier of K680(2) is set

[: the carrier of K680(2),REAL:] is complex-valued ext-real-valued real-valued set

bool [: the carrier of K680(2),REAL:] is non empty set

bool the carrier of K680(2) is non empty set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

MetrStruct(# REAL,real_dist #) is strict MetrStruct

the carrier of RealSpace is non empty V76() V77() V78() set

TopSpaceMetr RealSpace is TopStruct

the carrier of R^1 is non empty V76() V77() V78() set

dom {} is set

rng {} is set

4 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

T + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

0 * 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(0 * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

1 * ((0 * 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn mod 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set

2 * bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * bbcT) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ 0) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn mod 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set

2 * bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * bbcT) + 0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

PM + PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

FB is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ FB is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

TPM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * TPM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * TPM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ FB) * ((2 * TPM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * (2 |^ FB) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * (2 |^ FB)) * ((2 * TPM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

FB + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ (FB + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ (FB + 1)) * ((2 * TPM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn mod 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ bbcT) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * Bn) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ T) * ((2 * Bn) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

((2 |^ T) * ((2 * Bn) + 1)) - 1 is V35() real ext-real Element of REAL

T is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]

Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

[Bn,bbcT] is Element of [:NAT,NAT:]

{Bn,bbcT} is finite V49() V76() V77() V78() V79() V80() V81() set

{Bn} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set

{{Bn,bbcT},{Bn}} is finite V49() set

T . [Bn,bbcT] is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * bbcT) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ Bn) * ((2 * bbcT) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

((2 |^ Bn) * ((2 * bbcT) + 1)) - 1 is V35() real ext-real Element of REAL

T . (Bn,bbcT) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

[Bn,bbcT] is set

T . [Bn,bbcT] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set

In ((((2 |^ Bn) * ((2 * bbcT) + 1)) - 1),NAT) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

T is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]

Bn is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]

bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

[bbcT,PM] is Element of [:NAT,NAT:]

{bbcT,PM} is finite V49() V76() V77() V78() V79() V80() V81() set

{bbcT} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set

{{bbcT,PM},{bbcT}} is finite V49() set

T . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ bbcT) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

((2 |^ bbcT) * ((2 * PM) + 1)) - 1 is V35() real ext-real Element of REAL

T . (bbcT,PM) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

[bbcT,PM] is set

T . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set

Bn . (bbcT,PM) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set

() is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]

T is set

Bn is set

() . T is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL

() . Bn is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL

bbcT is set

PM is set

[bbcT,PM] is set

{bbcT,PM} is finite set

{bbcT} is non empty trivial finite 1 -element set

{{bbcT,PM},{bbcT}} is finite V49() set

FB is set

TPM is set

[FB,TPM] is set

{FB,TPM} is finite set

{FB} is non empty trivial finite 1 -element set

{{FB,TPM},{FB}} is finite V49() set

UX is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ UX is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * k is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ UX) * ((2 * k) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

((2 |^ UX) * ((2 * k) + 1)) - 1 is V35() real ext-real Element of REAL

Un is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ Un is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

UXk is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * UXk is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * UXk) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ Un) * ((2 * UXk) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

((2 |^ Un) * ((2 * UXk) + 1)) - 1 is V35() real ext-real Element of REAL

T is set

Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 |^ bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

(2 |^ bbcT) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

Bn - 0 is V35() real ext-real Element of REAL

((2 |^ bbcT) * ((2 * PM) + 1)) - 1 is V35() real ext-real Element of REAL

dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

bool [:NAT,NAT:] is non empty non trivial non finite set

[bbcT,PM] is Element of [:NAT,NAT:]

{bbcT,PM} is finite V49() V76() V77() V78() V79() V80() V81() set

{bbcT} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set

{{bbcT,PM},{bbcT}} is finite V49() set

() . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT

rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT

T is set

[:T,T:] is set

[:[:T,T:],REAL:] is complex-valued ext-real-valued real-valued set

bool [:[:T,T:],REAL:] is non empty set

[:T,REAL:] is complex-valued ext-real-valued real-valued set

bool [:T,REAL:] is non empty set

Bn is Relation-like [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]

bbcT is Element of T

PM is set

Bn . (bbcT,PM) is set

[bbcT,PM] is set

{bbcT,PM} is finite set

{bbcT} is non empty trivial finite 1 -element set

{{bbcT,PM},{bbcT}} is finite V49() set

Bn . [bbcT,PM] is V35() real ext-real set

Bn . [bbcT,PM] is V35() real ext-real Element of REAL

PM is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

FB is Element of T

[bbcT,FB] is set

{bbcT,FB} is finite set

{bbcT} is non empty trivial finite 1 -element set

{{bbcT,FB},{bbcT}} is finite V49() set

dom Bn is Relation-like T -defined T -valued Element of bool [:T,T:]

bool [:T,T:] is non empty set

Bn . [bbcT,FB] is V35() real ext-real Element of REAL

dom PM is Element of bool T

bool T is non empty set

Bn . (bbcT,FB) is V35() real ext-real Element of REAL

Bn . [bbcT,FB] is V35() real ext-real set

PM . FB is V35() real ext-real Element of REAL

FB is Element of T

PM . FB is V35() real ext-real Element of REAL

Bn . (bbcT,FB) is V35() real ext-real Element of REAL

[bbcT,FB] is set

{bbcT,FB} is finite set

{bbcT} is non empty trivial finite 1 -element set

{{bbcT,FB},{bbcT}} is finite V49() set

Bn . [bbcT,FB] is V35() real ext-real set

PM is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

FB is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

TPM is Element of T

PM . TPM is V35() real ext-real Element of REAL

Bn . (bbcT,TPM) is V35() real ext-real Element of REAL

[bbcT,TPM] is set

{bbcT,TPM} is finite set

{bbcT} is non empty trivial finite 1 -element set

{{bbcT,TPM},{bbcT}} is finite V49() set

Bn . [bbcT,TPM] is V35() real ext-real set

FB . TPM is V35() real ext-real Element of REAL

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

Bn is non empty TopSpace-like TopStruct

[:T,Bn:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,Bn:] is non empty set

bool the carrier of [:T,Bn:] is non empty set

the carrier of Bn is non empty set

bool the carrier of Bn is non empty set

[: the carrier of T, the carrier of Bn:] is non empty set

pr1 ( the carrier of T, the carrier of Bn) is Relation-like [: the carrier of T, the carrier of Bn:] -defined the carrier of T -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of Bn:], the carrier of T:]

[:[: the carrier of T, the carrier of Bn:], the carrier of T:] is non empty set

bool [:[: the carrier of T, the carrier of Bn:], the carrier of T:] is non empty set

pr2 ( the carrier of T, the carrier of Bn) is Relation-like [: the carrier of T, the carrier of Bn:] -defined the carrier of Bn -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of Bn:], the carrier of Bn:]

[:[: the carrier of T, the carrier of Bn:], the carrier of Bn:] is non empty set

bool [:[: the carrier of T, the carrier of Bn:], the carrier of Bn:] is non empty set

FB is Element of bool the carrier of [:T,Bn:]

bool (bool the carrier of [:T,Bn:]) is non empty set

TPM is Element of bool (bool the carrier of [:T,Bn:])

union TPM is Element of bool the carrier of [:T,Bn:]

Un is Element of the carrier of T

{Un} is non empty trivial finite 1 -element Element of bool the carrier of T

[:{Un}, the carrier of Bn:] is non empty set

FB /\ [:{Un}, the carrier of Bn:] is Element of bool the carrier of [:T,Bn:]

(pr2 ( the carrier of T, the carrier of Bn)) .: (FB /\ [:{Un}, the carrier of Bn:]) is Element of bool the carrier of Bn

UX is Element of the carrier of Bn

{UX} is non empty trivial finite 1 -element Element of bool the carrier of Bn

[: the carrier of T,{UX}:] is non empty set

FB /\ [: the carrier of T,{UX}:] is Element of bool the carrier of [:T,Bn:]

(pr1 ( the carrier of T, the carrier of Bn)) .: (FB /\ [: the carrier of T,{UX}:]) is Element of bool the carrier of T

UXk is Element of bool the carrier of T

k is Element of bool the carrier of Bn

UXk9 is set

dom (pr1 ( the carrier of T, the carrier of Bn)) is Relation-like the carrier of T -defined the carrier of Bn -valued Element of bool [: the carrier of T, the carrier of Bn:]

bool [: the carrier of T, the carrier of Bn:] is non empty set

nm is set

(pr1 ( the carrier of T, the carrier of Bn)) . nm is set

n is set

m is Element of bool the carrier of T

Unn is Element of bool the carrier of Bn

[:m,Unn:] is Element of bool the carrier of [:T,Bn:]

B is set

B1 is set

[B,B1] is set

{B,B1} is finite set

{B} is non empty trivial finite 1 -element set

{{B,B1},{B}} is finite V49() set

k is set

[k,UX] is set

{k,UX} is finite set

{k} is non empty trivial finite 1 -element set

{{k,UX},{k}} is finite V49() set

(pr1 ( the carrier of T, the carrier of Bn)) . (k,UX) is set

(pr1 ( the carrier of T, the carrier of Bn)) . [k,UX] is set

(pr1 ( the carrier of T, the carrier of Bn)) . (B,B1) is set

(pr1 ( the carrier of T, the carrier of Bn)) . [B,B1] is set

nm is Element of bool the carrier of T

n is Element of bool the carrier of T

UXk9 is set

dom (pr2 ( the carrier of T, the carrier of Bn)) is Relation-like the carrier of T -defined the carrier of Bn -valued Element of bool [: the carrier of T, the carrier of Bn:]

bool [: the carrier of T, the carrier of Bn:] is non empty set

nm is set

(pr2 ( the carrier of T, the carrier of Bn)) . nm is set

n is set

m is set

Unn is set

[m,Unn] is set

{m,Unn} is finite set

{m} is non empty trivial finite 1 -element set

{{m,Unn},{m}} is finite V49() set

(pr2 ( the carrier of T, the carrier of Bn)) . (m,Unn) is set

(pr2 ( the carrier of T, the carrier of Bn)) . [m,Unn] is set

B is Element of bool the carrier of T

B1 is Element of bool the carrier of Bn

[:B,B1:] is Element of bool the carrier of [:T,Bn:]

k is set

[Un,k] is set

{Un,k} is finite set

{Un} is non empty trivial finite 1 -element set

{{Un,k},{Un}} is finite V49() set

(pr2 ( the carrier of T, the carrier of Bn)) . (Un,k) is set

(pr2 ( the carrier of T, the carrier of Bn)) . [Un,k] is set

nm is Element of bool the carrier of Bn

n is Element of bool the carrier of Bn

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[: the carrier of T, the carrier of T:] is non empty set

[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set

[:T,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,T:] is non empty set

[: the carrier of [:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [: the carrier of [:T,T:],REAL:] is non empty non trivial non finite set

bbcT is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

[: the carrier of [:T,T:], the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set

bool [: the carrier of [:T,T:], the carrier of R^1:] is non empty set

PM is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]

TPM is Element of the carrier of T

( the carrier of T,bbcT,TPM) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [: the carrier of T,REAL:] is non empty non trivial non finite set

[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set

bool [: the carrier of T, the carrier of R^1:] is non empty set

FB is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:], the carrier of R^1:]

bool the carrier of R^1 is non empty set

Un is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]

UX is Element of the carrier of T

Un . UX is V35() real ext-real Element of the carrier of R^1

bool the carrier of T is non empty set

[TPM,UX] is Element of [: the carrier of T, the carrier of T:]

{TPM,UX} is finite set

{TPM} is non empty trivial finite 1 -element set

{{TPM,UX},{TPM}} is finite V49() set

pr2 ( the carrier of T, the carrier of T) is Relation-like [: the carrier of T, the carrier of T:] -defined the carrier of T -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of T:], the carrier of T:]

[:[: the carrier of T, the carrier of T:], the carrier of T:] is non empty set

bool [:[: the carrier of T, the carrier of T:], the carrier of T:] is non empty set

dom (pr2 ( the carrier of T, the carrier of T)) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

bool [: the carrier of T, the carrier of T:] is non empty set

UXk is Element of the carrier of [:T,T:]

bbcT . (TPM,UX) is V35() real ext-real Element of REAL

[TPM,UX] is set

bbcT . [TPM,UX] is V35() real ext-real set

k is V76() V77() V78() Element of bool the carrier of R^1

bool the carrier of [:T,T:] is non empty set

UXk9 is Element of bool the carrier of [:T,T:]

FB .: UXk9 is V76() V77() V78() Element of bool the carrier of R^1

{TPM} is non empty trivial finite 1 -element Element of bool the carrier of T

[:{TPM}, the carrier of T:] is non empty set

UXk9 /\ [:{TPM}, the carrier of T:] is Element of bool the carrier of [:T,T:]

(pr2 ( the carrier of T, the carrier of T)) .: (UXk9 /\ [:{TPM}, the carrier of T:]) is Element of bool the carrier of T

(pr2 ( the carrier of T, the carrier of T)) . (TPM,UX) is Element of the carrier of T

(pr2 ( the carrier of T, the carrier of T)) . [TPM,UX] is set

Un .: ((pr2 ( the carrier of T, the carrier of T)) .: (UXk9 /\ [:{TPM}, the carrier of T:])) is V76() V77() V78() Element of bool the carrier of R^1

n is set

dom Un is Element of bool the carrier of T

m is set

Un . m is V35() real ext-real Element of REAL

Unn is Element of the carrier of T

B is set

(pr2 ( the carrier of T, the carrier of T)) . B is set

B1 is set

k is set

[B1,k] is set

{B1,k} is finite set

{B1} is non empty trivial finite 1 -element set

{{B1,k},{B1}} is finite V49() set

q is Element of the carrier of T

s is Element of the carrier of T

[q,s] is Element of [: the carrier of T, the carrier of T:]

{q,s} is finite set

{q} is non empty trivial finite 1 -element set

{{q,s},{q}} is finite V49() set

(pr2 ( the carrier of T, the carrier of T)) . (q,s) is Element of the carrier of T

[q,s] is set

(pr2 ( the carrier of T, the carrier of T)) . [q,s] is set

bbcT . (q,s) is V35() real ext-real Element of REAL

bbcT . [q,s] is V35() real ext-real set

dom FB is Element of bool the carrier of [:T,T:]

T is non empty set

[:T,T:] is non empty set

[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:T,T:],REAL:] is non empty non trivial non finite set

bool T is non empty set

[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:T,REAL:] is non empty non trivial non finite set

Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]

bbcT is Element of bool T

PM is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

FB is Element of T

PM . FB is V35() real ext-real Element of REAL

(T,Bn,FB) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

(T,Bn,FB) .: bbcT is V76() V77() V78() Element of bool REAL

lower_bound ((T,Bn,FB) .: bbcT) is V35() real ext-real Element of REAL

PM is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

FB is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

TPM is Element of T

PM . TPM is V35() real ext-real Element of REAL

(T,Bn,TPM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

(T,Bn,TPM) .: bbcT is V76() V77() V78() Element of bool REAL

lower_bound ((T,Bn,TPM) .: bbcT) is V35() real ext-real Element of REAL

FB . TPM is V35() real ext-real Element of REAL

T is non empty set

[:T,T:] is non empty set

[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:T,T:],REAL:] is non empty non trivial non finite set

bool T is non empty set

Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]

PM is Element of T

(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:T,REAL:] is non empty non trivial non finite set

bbcT is non empty Element of bool T

(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL

FB is ext-real set

dom (T,Bn,PM) is Element of bool T

TPM is set

(T,Bn,PM) . TPM is V35() real ext-real Element of REAL

Un is Element of T

Bn . (PM,Un) is V35() real ext-real Element of REAL

[PM,Un] is set

{PM,Un} is finite set

{PM} is non empty trivial finite 1 -element set

{{PM,Un},{PM}} is finite V49() set

Bn . [PM,Un] is V35() real ext-real set

dom (T,Bn,PM) is Element of bool T

bbcT is set

dom Bn is Relation-like T -defined T -valued Element of bool [:T,T:]

bool [:T,T:] is non empty set

PM is set

FB is set

[PM,FB] is set

{PM,FB} is finite set

{PM} is non empty trivial finite 1 -element set

{{PM,FB},{PM}} is finite V49() set

TPM is Element of T

Un is Element of T

Bn . (TPM,Un) is V35() real ext-real Element of REAL

[TPM,Un] is set

{TPM,Un} is finite set

{TPM} is non empty trivial finite 1 -element set

{{TPM,Un},{TPM}} is finite V49() set

Bn . [TPM,Un] is V35() real ext-real set

- 1 is V35() real ext-real non positive Element of REAL

Bn . bbcT is V35() real ext-real Element of REAL

PM is Element of T

(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

bbcT is non empty Element of bool T

(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL

TPM is Element of T

(T,Bn,TPM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

FB is non empty Element of bool T

(T,Bn,TPM) .: FB is V76() V77() V78() Element of bool REAL

T is non empty set

[:T,T:] is non empty set

[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:T,T:],REAL:] is non empty non trivial non finite set

bool T is non empty set

Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]

bbcT is non empty Element of bool T

(T,Bn,bbcT) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:T,REAL:] is non empty non trivial non finite set

PM is Element of T

(T,Bn,bbcT) . PM is V35() real ext-real Element of REAL

FB is V35() real ext-real set

(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL

dom (T,Bn,PM) is Element of bool T

TPM is set

(T,Bn,PM) . TPM is V35() real ext-real Element of REAL

Bn . (PM,TPM) is set

[PM,TPM] is set

{PM,TPM} is finite set

{PM} is non empty trivial finite 1 -element set

{{PM,TPM},{PM}} is finite V49() set

Bn . [PM,TPM] is V35() real ext-real set

lower_bound ((T,Bn,PM) .: bbcT) is V35() real ext-real Element of REAL

T is non empty set

[:T,T:] is non empty set

[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:T,T:],REAL:] is non empty non trivial non finite set

bool T is non empty set

Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]

bbcT is Element of bool T

(T,Bn,bbcT) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:T,REAL:] is non empty non trivial non finite set

PM is Element of T

(T,Bn,bbcT) . PM is V35() real ext-real Element of REAL

(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

FB is non empty Element of bool T

(T,Bn,PM) .: FB is V76() V77() V78() Element of bool REAL

Bn . (PM,PM) is V35() real ext-real Element of REAL

[PM,PM] is set

{PM,PM} is finite set

{PM} is non empty trivial finite 1 -element set

{{PM,PM},{PM}} is finite V49() set

Bn . [PM,PM] is V35() real ext-real set

dom (T,Bn,PM) is Element of bool T

(T,Bn,PM) . PM is V35() real ext-real Element of REAL

lower_bound ((T,Bn,PM) .: FB) is V35() real ext-real Element of REAL

(T,Bn,FB) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]

(T,Bn,FB) . PM is V35() real ext-real Element of REAL

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[: the carrier of T, the carrier of T:] is non empty set

[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set

bool the carrier of T is non empty set

Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

bbcT is Element of the carrier of T

PM is Element of the carrier of T

Bn . (bbcT,PM) is V35() real ext-real Element of REAL

[bbcT,PM] is set

{bbcT,PM} is finite set

{bbcT} is non empty trivial finite 1 -element set

{{bbcT,PM},{bbcT}} is finite V49() set

Bn . [bbcT,PM] is V35() real ext-real set

FB is non empty Element of bool the carrier of T

( the carrier of T,Bn,FB) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [: the carrier of T,REAL:] is non empty non trivial non finite set

( the carrier of T,Bn,FB) . bbcT is V35() real ext-real Element of REAL

( the carrier of T,Bn,FB) . PM is V35() real ext-real Element of REAL

(( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM) is V35() real ext-real Element of REAL

abs ((( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM)) is V35() real ext-real Element of REAL

TPM is Element of the carrier of T

Un is Element of the carrier of T

Bn . (TPM,Un) is V35() real ext-real Element of REAL

[TPM,Un] is set

{TPM,Un} is finite set

{TPM} is non empty trivial finite 1 -element set

{{TPM,Un},{TPM}} is finite V49() set

Bn . [TPM,Un] is V35() real ext-real set

- (Bn . (TPM,Un)) is V35() real ext-real Element of REAL

( the carrier of T,Bn,FB) . Un is V35() real ext-real Element of REAL

( the carrier of T,Bn,FB) . TPM is V35() real ext-real Element of REAL

(( the carrier of T,Bn,FB) . Un) - (( the carrier of T,Bn,FB) . TPM) is V35() real ext-real Element of REAL

( the carrier of T,Bn,TPM) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

( the carrier of T,Bn,TPM) .: FB is V76() V77() V78() Element of bool REAL

( the carrier of T,Bn,Un) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

( the carrier of T,Bn,Un) .: FB is V76() V77() V78() Element of bool REAL

lower_bound (( the carrier of T,Bn,TPM) .: FB) is V35() real ext-real Element of REAL

(lower_bound (( the carrier of T,Bn,TPM) .: FB)) - (Bn . (TPM,Un)) is V35() real ext-real Element of REAL

UX is V35() real ext-real set

dom ( the carrier of T,Bn,Un) is Element of bool the carrier of T

UXk is set

( the carrier of T,Bn,Un) . UXk is V35() real ext-real Element of REAL

k is Element of the carrier of T

( the carrier of T,Bn,TPM) . k is V35() real ext-real Element of REAL

Bn . (TPM,k) is V35() real ext-real Element of REAL

[TPM,k] is set

{TPM,k} is finite set

{{TPM,k},{TPM}} is finite V49() set

Bn . [TPM,k] is V35() real ext-real set

Bn . (Un,k) is V35() real ext-real Element of REAL

[Un,k] is set

{Un,k} is finite set

{Un} is non empty trivial finite 1 -element set

{{Un,k},{Un}} is finite V49() set

Bn . [Un,k] is V35() real ext-real set

(Bn . (TPM,Un)) + (Bn . (Un,k)) is V35() real ext-real Element of REAL

dom ( the carrier of T,Bn,TPM) is Element of bool the carrier of T

(lower_bound (( the carrier of T,Bn,TPM) .: FB)) + 0 is V35() real ext-real Element of REAL

(Bn . (Un,k)) - 0 is V35() real ext-real Element of REAL

lower_bound (( the carrier of T,Bn,Un) .: FB) is V35() real ext-real Element of REAL

(lower_bound (( the carrier of T,Bn,Un) .: FB)) - 0 is V35() real ext-real Element of REAL

0 - (Bn . (TPM,Un)) is V35() real ext-real Element of REAL

(lower_bound (( the carrier of T,Bn,Un) .: FB)) - (lower_bound (( the carrier of T,Bn,TPM) .: FB)) is V35() real ext-real Element of REAL

- (Bn . (bbcT,PM)) is V35() real ext-real Element of REAL

(( the carrier of T,Bn,FB) . PM) - (( the carrier of T,Bn,FB) . bbcT) is V35() real ext-real Element of REAL

- ((( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM)) is V35() real ext-real Element of REAL

Bn . (PM,bbcT) is V35() real ext-real Element of REAL

[PM,bbcT] is set

{PM,bbcT} is finite set

{PM} is non empty trivial finite 1 -element set

{{PM,bbcT},{PM}} is finite V49() set

Bn . [PM,bbcT] is V35() real ext-real set

- (Bn . (PM,bbcT)) is V35() real ext-real Element of REAL

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[: the carrier of T, the carrier of T:] is non empty set

[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set

bool the carrier of T is non empty set

Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

bbcT is non empty Element of bool the carrier of T

( the carrier of T,Bn,bbcT) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [: the carrier of T,REAL:] is non empty non trivial non finite set

[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set

bool [: the carrier of T, the carrier of R^1:] is non empty set

FB is Element of the carrier of T

( the carrier of T,Bn,FB) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

bool the carrier of R^1 is non empty set

PM is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]

PM . FB is V35() real ext-real Element of the carrier of R^1

PM . FB is V35() real ext-real Element of REAL

TPM is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]

TPM . FB is V35() real ext-real Element of REAL

UXk is V76() V77() V78() Element of bool the carrier of R^1

Un is V35() real ext-real Element of the carrier of RealSpace

k is V35() real ext-real set

Ball (Un,k) is V76() V77() V78() Element of bool the carrier of RealSpace

bool the carrier of RealSpace is non empty set

UX is V35() real ext-real Element of the carrier of RealSpace

Ball (UX,k) is V76() V77() V78() Element of bool the carrier of RealSpace

TPM . FB is V35() real ext-real Element of the carrier of R^1

(TPM . FB) - (TPM . FB) is V35() real ext-real set

abs ((TPM . FB) - (TPM . FB)) is V35() real ext-real Element of REAL

dist (UX,UX) is V35() real ext-real Element of REAL

UXk9 is V76() V77() V78() Element of bool the carrier of R^1

nm is Element of bool the carrier of T

TPM .: nm is V76() V77() V78() Element of bool the carrier of R^1

PM .: nm is V76() V77() V78() Element of bool the carrier of R^1

n is set

dom PM is Element of bool the carrier of T

m is set

PM . m is V35() real ext-real Element of REAL

Unn is Element of the carrier of T

PM . Unn is V35() real ext-real Element of REAL

TPM . Unn is V35() real ext-real Element of REAL

Bn . (FB,Unn) is V35() real ext-real Element of REAL

[FB,Unn] is set

{FB,Unn} is finite set

{FB} is non empty trivial finite 1 -element set

{{FB,Unn},{FB}} is finite V49() set

Bn . [FB,Unn] is V35() real ext-real set

TPM . Unn is V35() real ext-real Element of the carrier of R^1

Bn . (FB,FB) is V35() real ext-real Element of REAL

[FB,FB] is set

{FB,FB} is finite set

{{FB,FB},{FB}} is finite V49() set

Bn . [FB,FB] is V35() real ext-real set

B1 is V35() real ext-real Element of the carrier of RealSpace

dist (UX,B1) is V35() real ext-real Element of REAL

0 - (TPM . Unn) is V35() real ext-real Element of REAL

abs (0 - (TPM . Unn)) is V35() real ext-real Element of REAL

dom TPM is Element of bool the carrier of T

- (0 - (TPM . Unn)) is V35() real ext-real Element of REAL

abs (- (0 - (TPM . Unn))) is V35() real ext-real Element of REAL

( the carrier of T,Bn,bbcT) . FB is V35() real ext-real Element of REAL

( the carrier of T,Bn,bbcT) . Unn is V35() real ext-real Element of REAL

(( the carrier of T,Bn,bbcT) . FB) - (( the carrier of T,Bn,bbcT) . Unn) is V35() real ext-real Element of REAL

abs ((( the carrier of T,Bn,bbcT) . FB) - (( the carrier of T,Bn,bbcT) . Unn)) is V35() real ext-real Element of REAL

B is V35() real ext-real Element of the carrier of RealSpace

dist (Un,B) is V35() real ext-real Element of REAL

T is set

[:T,T:] is set

[:[:T,T:],REAL:] is complex-valued ext-real-valued real-valued set

bool [:[:T,T:],REAL:] is non empty set

Bn is Relation-like [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]

bbcT is Element of T

Bn . (bbcT,bbcT) is V35() real ext-real Element of REAL

[bbcT,bbcT] is set

{bbcT,bbcT} is finite set

{bbcT} is non empty trivial finite 1 -element set

{{bbcT,bbcT},{bbcT}} is finite V49() set

Bn . [bbcT,bbcT] is V35() real ext-real set

PM is Element of T

FB is Element of T

Bn . (PM,FB) is V35() real ext-real Element of REAL

[PM,FB] is set

{PM,FB} is finite set

{PM} is non empty trivial finite 1 -element set

{{PM,FB},{PM}} is finite V49() set

Bn . [PM,FB] is V35() real ext-real set

Bn . (FB,PM) is V35() real ext-real Element of REAL

[FB,PM] is set

{FB,PM} is finite set

{FB} is non empty trivial finite 1 -element set

{{FB,PM},{FB}} is finite V49() set

Bn . [FB,PM] is V35() real ext-real set

TPM is Element of T

UX is Element of T

Bn . (TPM,UX) is V35() real ext-real Element of REAL

[TPM,UX] is set

{TPM,UX} is finite set

{TPM} is non empty trivial finite 1 -element set

{{TPM,UX},{TPM}} is finite V49() set

Bn . [TPM,UX] is V35() real ext-real set

Un is Element of T

Bn . (TPM,Un) is V35() real ext-real Element of REAL

[TPM,Un] is set

{TPM,Un} is finite set

{{TPM,Un},{TPM}} is finite V49() set

Bn . [TPM,Un] is V35() real ext-real set

Bn . (Un,UX) is V35() real ext-real Element of REAL

[Un,UX] is set

{Un,UX} is finite set

{Un} is non empty trivial finite 1 -element set

{{Un,UX},{Un}} is finite V49() set

Bn . [Un,UX] is V35() real ext-real set

(Bn . (TPM,Un)) + (Bn . (Un,UX)) is V35() real ext-real Element of REAL

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[: the carrier of T, the carrier of T:] is non empty set

[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set

bool the carrier of T is non empty set

Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

SpaceMetr ( the carrier of T,Bn) is strict Reflexive discerning symmetric triangle MetrStruct

PM is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of PM is non empty set

FB is Element of the carrier of PM

TPM is Element of the carrier of PM

Bn . (FB,TPM) is set

[FB,TPM] is set

{FB,TPM} is finite set

{FB} is non empty trivial finite 1 -element set

{{FB,TPM},{FB}} is finite V49() set

Bn . [FB,TPM] is V35() real ext-real set

dist (FB,TPM) is V35() real ext-real Element of REAL

MetrStruct(# the carrier of T,Bn #) is strict MetrStruct

Family_open_set PM is Element of bool (bool the carrier of PM)

bool the carrier of PM is non empty set

bool (bool the carrier of PM) is non empty set

the topology of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

FB is set

TPM is Element of bool the carrier of T

TPM ` is Element of bool the carrier of T

the carrier of T \ TPM is set

[#] T is non empty non proper open closed Element of bool the carrier of T

([#] T) ` is open closed Element of bool the carrier of T

the carrier of T \ ([#] T) is set

TPM is Element of bool the carrier of T

TPM ` is Element of bool the carrier of T

the carrier of T \ TPM is set

Un is set

UX is Element of the carrier of PM

UXk is V35() real ext-real Element of REAL

Ball (UX,UXk) is Element of bool the carrier of PM

UXk9 is Element of bool the carrier of T

UXk9 ` is Element of bool the carrier of T

the carrier of T \ UXk9 is set

( the carrier of T,Bn,(UXk9 `)) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [: the carrier of T,REAL:] is non empty non trivial non finite set

{ b

n is set

n is set

m is set

( the carrier of T,Bn,(UXk9 `)) . m is V35() real ext-real Element of REAL

m is set

Unn is Element of the carrier of T

( the carrier of T,Bn,(UXk9 `)) . Unn is V35() real ext-real Element of REAL

( the carrier of T,Bn,Unn) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

( the carrier of T,Bn,Unn) .: (UXk9 `) is V76() V77() V78() Element of bool REAL

B is Element of the carrier of PM

B1 is V35() real ext-real Element of REAL

Ball (B,B1) is Element of bool the carrier of PM

lower_bound (( the carrier of T,Bn,Unn) .: (UXk9 `)) is V35() real ext-real Element of REAL

0 + B1 is V35() real ext-real Element of REAL

k is V35() real ext-real set

dom ( the carrier of T,Bn,Unn) is Element of bool the carrier of T

q is set

( the carrier of T,Bn,Unn) . q is V35() real ext-real Element of REAL

s is Element of the carrier of T

Bn . (Unn,s) is V35() real ext-real Element of REAL

[Unn,s] is set

{Unn,s} is finite set

{Unn} is non empty trivial finite 1 -element set

{{Unn,s},{Unn}} is finite V49() set

Bn . [Unn,s] is V35() real ext-real set

b is Element of the carrier of PM

dist (B,b) is V35() real ext-real Element of REAL

Cl (UXk9 `) is closed Element of bool the carrier of T

k is Element of the carrier of T

Bn . (k,k) is V35() real ext-real Element of REAL

[k,k] is set

{k,k} is finite set

{k} is non empty trivial finite 1 -element set

{{k,k},{k}} is finite V49() set

Bn . [k,k] is V35() real ext-real set

dist (UX,UX) is V35() real ext-real Element of REAL

UX is Element of bool the carrier of T

UXk is Element of bool the carrier of T

TPM is Element of bool the carrier of T

TPM ` is Element of bool the carrier of T

the carrier of T \ TPM is set

FB is set

TPM is Element of bool the carrier of T

TPM ` is Element of bool the carrier of T

the carrier of T \ TPM is set

[#] T is non empty non proper open closed Element of bool the carrier of T

([#] T) ` is open closed Element of bool the carrier of T

the carrier of T \ ([#] T) is set

TPM is Element of bool the carrier of T

TPM ` is Element of bool the carrier of T

the carrier of T \ TPM is set

Un is Element of bool the carrier of PM

UX is Element of the carrier of PM

( the carrier of T,Bn,(TPM `)) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [: the carrier of T,REAL:] is non empty non trivial non finite set

UXk is Element of the carrier of T

( the carrier of T,Bn,(TPM `)) . UXk is V35() real ext-real Element of REAL

k is V35() real ext-real Element of REAL

Ball (UX,k) is Element of bool the carrier of PM

( the carrier of T,Bn,UXk) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]

( the carrier of T,Bn,UXk) .: (TPM `) is V76() V77() V78() Element of bool REAL

UXk9 is set

nm is Element of the carrier of PM

dist (UX,nm) is V35() real ext-real Element of REAL

dom ( the carrier of T,Bn,UXk) is Element of bool the carrier of T

n is Element of the carrier of T

( the carrier of T,Bn,UXk) . n is V35() real ext-real Element of REAL

lower_bound (( the carrier of T,Bn,UXk) .: (TPM `)) is V35() real ext-real Element of REAL

Bn . (UXk,n) is V35() real ext-real Element of REAL

[UXk,n] is set

{UXk,n} is finite set

{UXk} is non empty trivial finite 1 -element set