:: PCOMPS_1 semantic presentation

REAL is V36() V37() V38() V42() set

NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL

bool REAL is non empty set

COMPLEX is V36() V42() set

omega is V36() V37() V38() V39() V40() V41() V42() set

bool omega is non empty set

bool NAT is non empty set

1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT

[:1,1:] is non empty Relation-like set

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

[:[:1,1:],1:] is non empty Relation-like set

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

[:[:1,1:],REAL:] is Relation-like set

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

[:REAL,REAL:] is Relation-like set

[:[:REAL,REAL:],REAL:] is Relation-like set

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

2 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT

[:2,2:] is non empty Relation-like set

[:[:2,2:],REAL:] is Relation-like set

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

{} is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered set

3 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT

union {} is finite set

0 is empty Relation-like non-empty empty-yielding functional ordinal natural V27() real ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered Element of NAT

D is MetrStruct

the carrier of D is set

f is Element of the carrier of D

f is V27() real ext-real set

c

Ball (f,f) is Element of bool the carrier of D

bool the carrier of D is non empty set

Ball (f,c

b is Element of the carrier of D

dist (f,b) is V27() real ext-real Element of REAL

D is TopSpace-like TopStruct

the carrier of D is set

bool the carrier of D is non empty set

f is Element of bool the carrier of D

Cl f is closed Element of bool the carrier of D

the Element of f is Element of f

c

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

union f is Element of bool the carrier of D

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

f is Element of the carrier of D

c

b is Element of bool the carrier of D

D is set

1TopSp D is strict TopSpace-like TopStruct

bool D is non empty Element of bool (bool D)

bool D is non empty set

bool (bool D) is non empty set

[#] (bool D) is non empty non proper Element of bool (bool D)

bool (bool D) is non empty set

TopStruct(# D,([#] (bool D)) #) is strict TopStruct

the topology of (1TopSp D) is non empty open Element of bool (bool the carrier of (1TopSp D))

the carrier of (1TopSp D) is set

bool the carrier of (1TopSp D) is non empty set

bool (bool the carrier of (1TopSp D)) is non empty set

D is set

1TopSp D is strict TopSpace-like TopStruct

bool D is non empty Element of bool (bool D)

bool D is non empty set

bool (bool D) is non empty set

[#] (bool D) is non empty non proper Element of bool (bool D)

bool (bool D) is non empty set

TopStruct(# D,([#] (bool D)) #) is strict TopStruct

the carrier of (1TopSp D) is set

D is set

{D} is non empty finite set

1TopSp {D} is non empty finite strict TopSpace-like T_0 T_1 Hausdorff compact TopStruct

bool {D} is non empty finite V47() Element of bool (bool {D})

bool {D} is non empty finite V47() set

bool (bool {D}) is non empty finite V47() set

[#] (bool {D}) is non empty non proper finite V47() Element of bool (bool {D})

bool (bool {D}) is non empty finite V47() set

TopStruct(# {D},([#] (bool {D})) #) is non empty strict TopStruct

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

f is Element of the carrier of D

{f} is non empty finite compact Element of bool the carrier of D

bool the carrier of D is non empty set

D is TopStruct

the carrier of D is set

bool the carrier of D is non empty set

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

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

f is Element of bool the carrier of D

{ b

c

b is Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

c

b is Element of bool the carrier of D

{ b

c is Element of bool the carrier of D

{ b

c is set

V is Element of bool the carrier of D

W is Element of bool the carrier of D

V is Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

f is Element of the carrier of D

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

{ b

D is TopStruct

the carrier of D is set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

c

b is set

c is Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is Element of bool the carrier of D

b is set

c is Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is Element of bool the carrier of D

D is TopSpace-like TopStruct

the carrier of D is set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

f is Element of bool the carrier of D

c

Cl c

D is TopSpace-like TopStruct

the carrier of D is set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

f is set

the Element of f is Element of f

b is set

c is Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool the carrier of D

{f} is non empty finite Element of bool (bool the carrier of D)

Cl f is closed Element of bool the carrier of D

{(Cl f)} is non empty finite Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

c

b is set

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

c is Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

c

b is set

c is set

c is Element of bool the carrier of D

V is Element of bool the carrier of D

Cl V is closed Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

f \/ f is Element of bool (bool the carrier of D)

(D,(f \/ f)) is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

(D,f) \/ (D,f) is Element of bool (bool the carrier of D)

c

b is Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

b is Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

b is Element of bool the carrier of D

c is Element of bool the carrier of D

Cl c is closed Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

union f is Element of bool the carrier of D

Cl (union f) is closed Element of bool the carrier of D

(D,f) is Element of bool (bool the carrier of D)

union (D,f) is Element of bool the carrier of D

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng f is finite set

dom f is V36() V37() V38() V39() V40() V41() finite Element of bool NAT

c

Seg c

b is ordinal natural V27() real ext-real non negative set

Seg b is V36() V37() V38() V39() V40() V41() finite V50(b) Element of bool NAT

f .: (Seg b) is finite set

b + 1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT

Seg (b + 1) is non empty V36() V37() V38() V39() V40() V41() finite V50(b + 1) Element of bool NAT

f .: (Seg (b + 1)) is finite set

c is Element of bool (bool the carrier of D)

union c is Element of bool the carrier of D

Cl (union c) is closed Element of bool the carrier of D

(D,c) is Element of bool (bool the carrier of D)

union (D,c) is Element of bool the carrier of D

Im (f,(b + 1)) is set

{(b + 1)} is non empty V36() V37() V38() V39() V40() V41() finite set

f .: {(b + 1)} is finite set

c

0 + 1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT

c is Element of bool (bool the carrier of D)

f . (b + 1) is set

{(f . (b + 1))} is non empty finite set

union c is Element of bool the carrier of D

(D,c) is Element of bool (bool the carrier of D)

union (D,c) is Element of bool the carrier of D

W is Element of bool the carrier of D

Cl W is closed Element of bool the carrier of D

{(Cl W)} is non empty finite Element of bool (bool the carrier of D)

union {(Cl W)} is Element of bool the carrier of D

Cl (union c) is closed Element of bool the carrier of D

(Seg b) \/ {(b + 1)} is non empty V36() V37() V38() V39() V40() V41() finite set

f .: ((Seg b) \/ {(b + 1)}) is finite set

(f .: (Seg b)) \/ (f .: {(b + 1)}) is finite set

V is Element of bool (bool the carrier of D)

union V is Element of bool the carrier of D

(union V) \/ (union c) is Element of bool the carrier of D

Cl ((union V) \/ (union c)) is closed Element of bool the carrier of D

Cl (union V) is closed Element of bool the carrier of D

(Cl (union V)) \/ (Cl (union c)) is closed Element of bool the carrier of D

(D,V) is Element of bool (bool the carrier of D)

union (D,V) is Element of bool the carrier of D

(union (D,V)) \/ (union (D,c)) is Element of bool the carrier of D

(D,V) \/ (D,c) is Element of bool (bool the carrier of D)

union ((D,V) \/ (D,c)) is Element of bool the carrier of D

Seg 0 is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() V50( 0 ) FinSequence-like FinSequence-membered Element of bool NAT

f .: (Seg 0) is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered set

b is Element of bool (bool the carrier of D)

union b is Element of bool the carrier of D

Cl (union b) is closed Element of bool the carrier of D

(D,b) is Element of bool (bool the carrier of D)

union (D,b) is Element of bool the carrier of D

{} D is empty proper Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered open closed compact Element of bool the carrier of D

f .: (Seg c

f .: {} is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered set

{} D is empty proper Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered open closed compact Element of bool the carrier of D

0 + 1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

c

b is Element of bool the carrier of D

Cl b is closed Element of bool the carrier of D

c is set

F

the carrier of F

bool the carrier of F

bool (bool the carrier of F

F

F

[:F

bool [:F

D is set

F

D is Relation-like F

f is Element of bool the carrier of F

D . f is set

F

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

(D,f) is Element of bool (bool the carrier of D)

c

b is Element of bool the carrier of D

{ b

{ b

V is Element of bool the carrier of D

Cl V is closed Element of bool the carrier of D

[:f,(D,f):] is Relation-like set

bool [:f,(D,f):] is non empty set

V is Relation-like f -defined (D,f) -valued Function-like V33(f,(D,f)) Element of bool [:f,(D,f):]

dom V is set

V .: { b

W is set

W is Element of bool the carrier of D

V is Element of bool the carrier of D

Cl V is closed Element of bool the carrier of D

V . V is set

W /\ b is Element of bool the carrier of D

c

Cl c

b /\ (Cl c

Cl (b /\ (Cl c

b /\ c

Cl (b /\ c

c

c

W is set

V . W is set

W is set

V . W is set

V is Element of bool the carrier of D

V . V is set

Cl V is closed Element of bool the carrier of D

c

z is Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

union f is Element of bool the carrier of D

(D,f) is Element of bool (bool the carrier of D)

union (D,f) is Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

union f is Element of bool the carrier of D

Cl (union f) is closed Element of bool the carrier of D

(D,f) is Element of bool (bool the carrier of D)

union (D,f) is Element of bool the carrier of D

b is Element of the carrier of D

c is Element of bool the carrier of D

{ b

V is Element of bool (bool the carrier of D)

union V is Element of bool the carrier of D

Cl (union V) is closed Element of bool the carrier of D

(D,V) is Element of bool (bool the carrier of D)

union (D,V) is Element of bool the carrier of D

f \ V is Element of bool (bool the carrier of D)

union (f \ V) is Element of bool the carrier of D

Cl (union (f \ V)) is closed Element of bool the carrier of D

W is set

V is set

c

union W is set

V \/ (f \ V) is Element of bool (bool the carrier of D)

V \/ f is Element of bool (bool the carrier of D)

(union V) \/ (union (f \ V)) is Element of bool the carrier of D

Cl ((union V) \/ (union (f \ V))) is closed Element of bool the carrier of D

(Cl (union V)) \/ (Cl (union (f \ V))) is closed Element of bool the carrier of D

b is Element of the carrier of D

c is set

c is Element of bool the carrier of D

V is Element of bool the carrier of D

Cl V is closed Element of bool the carrier of D

W is Element of bool the carrier of D

(union f) /\ W is Element of bool the carrier of D

V /\ W is Element of bool the carrier of D

W is set

W is Element of the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

union f is Element of bool the carrier of D

(D,f) is Element of bool (bool the carrier of D)

union (D,f) is Element of bool the carrier of D

b is Element of the carrier of D

c is set

c is Element of bool the carrier of D

V is Element of bool the carrier of D

Cl V is closed Element of bool the carrier of D

W is Element of bool the carrier of D

Cl (union f) is closed Element of bool the carrier of D

{1} is non empty V36() V37() V38() V39() V40() V41() finite set

1TopSp {1} is non empty finite strict TopSpace-like T_0 T_1 Hausdorff compact TopStruct

bool {1} is non empty finite V47() Element of bool (bool {1})

bool {1} is non empty finite V47() set

bool (bool {1}) is non empty finite V47() set

[#] (bool {1}) is non empty non proper finite V47() Element of bool (bool {1})

bool (bool {1}) is non empty finite V47() set

TopStruct(# {1},([#] (bool {1})) #) is non empty strict TopStruct

D is non empty finite strict TopSpace-like T_0 T_1 Hausdorff compact TopStruct

the carrier of D is non empty finite set

bool the carrier of D is non empty finite V47() set

bool (bool the carrier of D) is non empty finite V47() set

f is finite V47() Element of bool (bool the carrier of D)

f is finite V47() Element of bool (bool the carrier of D)

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

c

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

f is Element of bool the carrier of D

f is Element of bool the carrier of D

f ` is Element of bool the carrier of D

the carrier of D \ f is set

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

c

b is Element of the carrier of D

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

f \/ (f `) is Element of bool the carrier of D

c is Element of bool the carrier of D

c is Element of bool the carrier of D

V is Element of bool the carrier of D

union c

c is Element of bool the carrier of D

c is Element of bool the carrier of D

union c

c is Element of bool the carrier of D

union c

union c

b is Element of bool the carrier of D

V is Element of the carrier of D

c is Element of bool the carrier of D

c is Element of bool the carrier of D

b is Element of bool (bool the carrier of D)

{ b

c is Element of bool (bool the carrier of D)

(D,c) is Element of bool (bool the carrier of D)

union (D,c) is Element of bool the carrier of D

(union (D,c)) ` is Element of bool the carrier of D

the carrier of D \ (union (D,c)) is set

V is Element of bool the carrier of D

union c is Element of bool the carrier of D

W is Element of bool the carrier of D

Cl (union c) is closed Element of bool the carrier of D

W is Element of bool the carrier of D

Cl W is closed Element of bool the carrier of D

f /\ (Cl W) is Element of bool the carrier of D

V is Element of bool the carrier of D

V is set

c

z is Element of bool the carrier of D

c

y is Element of the carrier of D

W is Element of bool the carrier of D

z is Element of bool the carrier of D

y is Element of the carrier of D

W is Element of bool the carrier of D

z is Element of bool the carrier of D

z /\ W is Element of bool the carrier of D

Cl (z /\ W) is closed Element of bool the carrier of D

{} D is empty proper Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered open closed compact Element of bool the carrier of D

Cl ({} D) is closed Element of bool the carrier of D

z /\ (Cl W) is Element of bool the carrier of D

Cl (z /\ (Cl W)) is closed Element of bool the carrier of D

c

W is set

V is Element of the carrier of D

c

z is Element of bool the carrier of D

f /\ z is Element of bool the carrier of D

W is Element of bool the carrier of D

Cl W is closed Element of bool the carrier of D

W is Element of the carrier of D

V is Element of bool the carrier of D

V is Element of bool the carrier of D

V ` is Element of bool the carrier of D

the carrier of D \ V is set

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

f is Element of the carrier of D

f is Element of bool the carrier of D

f ` is Element of bool the carrier of D

the carrier of D \ f is set

{f} is non empty finite compact Element of bool the carrier of D

b is Element of the carrier of D

c is Element of bool the carrier of D

c is Element of bool the carrier of D

b is Element of bool the carrier of D

c is Element of bool the carrier of D

D is non empty TopSpace-like TopStruct

the carrier of D is non empty set

bool the carrier of D is non empty set

f is Element of bool the carrier of D

f is Element of bool the carrier of D

c

f ` is Element of bool the carrier of D

the carrier of D \ f is set

b is Element of bool the carrier of D

c is Element of bool the carrier of D

c

b is Element of bool the carrier of D

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty set

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

f is Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

c

b is Element of the carrier of D

b is Element of the carrier of D

D is MetrStruct

the carrier of D is set

f is Element of the carrier of D

f is V27() real ext-real Element of REAL

Ball (f,f) is Element of bool the carrier of D

bool the carrier of D is non empty set

D is MetrStruct

the carrier of D is set

f is Element of the carrier of D

f is Element of the carrier of D

c

Ball (f,c

bool the carrier of D is non empty set

dist (f,f) is V27() real ext-real Element of REAL

b is V27() real ext-real Element of REAL

b - (dist (f,f)) is V27() real ext-real Element of REAL

Ball (f,(b - (dist (f,f)))) is Element of bool the carrier of D

c is Element of the carrier of D

dist (f,c) is V27() real ext-real Element of REAL

(dist (f,f)) + (dist (f,c)) is V27() real ext-real Element of REAL

dist (f,c) is V27() real ext-real Element of REAL

D is MetrStruct

the carrier of D is set

f is V27() real ext-real Element of REAL

f is V27() real ext-real Element of REAL

c

b is Element of the carrier of D

Ball (b,f) is Element of bool the carrier of D

bool the carrier of D is non empty set

c is Element of the carrier of D

Ball (c,f) is Element of bool the carrier of D

(Ball (b,f)) /\ (Ball (c,f)) is Element of bool the carrier of D

c is V27() real ext-real Element of REAL

Ball (c

V is V27() real ext-real Element of REAL

Ball (c

min (c,V) is V27() real ext-real Element of REAL

W is V27() real ext-real Element of REAL

Ball (c

D is MetrStruct

the carrier of D is set

(D) is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

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

f is Element of the carrier of D

f is V27() real ext-real set

Ball (f,f) is Element of bool the carrier of D

c

D is MetrStruct

the carrier of D is set

(D) is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

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

f is Element of the carrier of D

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty set

(D) is Element of bool (bool the carrier of D)

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

f is Element of bool the carrier of D

f is Element of bool the carrier of D

f /\ f is Element of bool the carrier of D

c

b is V27() real ext-real Element of REAL

Ball (c

c is V27() real ext-real Element of REAL

Ball (c

min (b,c) is V27() real ext-real Element of REAL

c is V27() real ext-real Element of REAL

Ball (c

D is MetrStruct

the carrier of D is set

bool the carrier of D is non empty set

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

(D) is Element of bool (bool the carrier of D)

f is Element of bool (bool the carrier of D)

union f is Element of bool the carrier of D

f is Element of the carrier of D

c

b is Element of bool the carrier of D

c is V27() real ext-real Element of REAL

Ball (f,c) is Element of bool the carrier of D

D is MetrStruct

the carrier of D is set

(D) is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

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

TopStruct(# the carrier of D,(D) #) is strict TopStruct

the carrier of TopStruct(# the carrier of D,(D) #) is set

bool the carrier of TopStruct(# the carrier of D,(D) #) is non empty set

the topology of TopStruct(# the carrier of D,(D) #) is open Element of bool (bool the carrier of TopStruct(# the carrier of D,(D) #))

bool (bool the carrier of TopStruct(# the carrier of D,(D) #)) is non empty set

f is Element of bool the carrier of TopStruct(# the carrier of D,(D) #)

c

f /\ c

f is Element of bool (bool the carrier of TopStruct(# the carrier of D,(D) #))

union f is Element of bool the carrier of TopStruct(# the carrier of D,(D) #)

D is MetrStruct

the carrier of D is set

(D) is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

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

TopStruct(# the carrier of D,(D) #) is strict TopStruct

D is MetrStruct

(D) is TopStruct

the carrier of D is set

(D) is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

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

TopStruct(# the carrier of D,(D) #) is strict TopStruct

D is non empty MetrStruct

(D) is strict TopSpace-like TopStruct

the carrier of D is non empty set

(D) is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

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

TopStruct(# the carrier of D,(D) #) is non empty strict TopStruct

D is non empty Reflexive discerning V96() triangle Discerning MetrStruct

(D) is non empty strict TopSpace-like TopStruct

the carrier of D is non empty set

(D) is Element of bool (bool the carrier of D)

bool the carrier of D is non empty set

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

TopStruct(# the carrier of D,(D) #) is non empty strict TopStruct

the carrier of (D) is non empty set

bool the carrier of (D) is non empty set

f is Element of the carrier of (D)

c

b is Element of the carrier of D

c is Element of the carrier of D

dist (b,c) is V27() real ext-real Element of REAL

(dist (b,c)) / 2 is V27() real ext-real Element of REAL

Ball (c,((dist (b,c)) / 2)) is Element of bool the carrier of D

Ball (b,((dist (b,c)) / 2)) is Element of bool the carrier of D

W is Element of bool the carrier of (D)

V is Element of bool the carrier of (D)

W /\ V is Element of bool the carrier of (D)

c

z is Element of the carrier of D

dist (c,z) is V27() real ext-real Element of REAL

dist (b,z) is V27() real ext-real Element of REAL

((dist (b,c)) / 2) + ((dist (b,c)) / 2) is V27() real ext-real Element of REAL

(dist (b,z)) + (dist (c,z)) is V27() real ext-real Element of REAL

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

dist (c,c) is V27() real ext-real Element of REAL

V is Element of bool the carrier of (D)

W is Element of bool the carrier of (D)

the non empty Reflexive discerning V96() triangle Discerning MetrStruct is non empty Reflexive discerning V96() triangle Discerning MetrStruct

( the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty strict TopSpace-like TopStruct

the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct is non empty set

( the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) is Element of bool (bool the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct )

bool the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct is non empty set

bool (bool the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty set

TopStruct(# the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct ,( the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) #) is non empty strict TopStruct

D is set

[:D,D:] is Relation-like set

[:[:D,D:],REAL:] is Relation-like set

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

D is set

[:D,D:] is Relation-like set

[:[:D,D:],REAL:] is Relation-like set

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

f is Relation-like [:D,D:] -defined REAL -valued Function-like V33([:D,D:], REAL ) Element of bool [:[:D,D:],REAL:]

MetrStruct(# D,f #) is strict MetrStruct

c

the carrier of c

the distance of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

b is Element of the carrier of c

c is Element of the carrier of c

the distance of c

the distance of c

c is Element of the carrier of c

the distance of c

the distance of c

( the distance of c

dist (b,c) is V27() real ext-real Element of REAL

dist (c,b) is V27() real ext-real Element of REAL

dist (b,c) is V27() real ext-real Element of REAL

dist (c,c) is V27() real ext-real Element of REAL

the carrier of MetrStruct(# D,f #) is set

c

b is Element of the carrier of MetrStruct(# D,f #)

dist (c

dist (b,c

c is Element of the carrier of MetrStruct(# D,f #)

dist (c

dist (b,c) is V27() real ext-real Element of REAL

(dist (c

the distance of MetrStruct(# D,f #) is Relation-like [: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):] -defined REAL -valued Function-like V33([: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):],REAL:]

[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):] is Relation-like set

[:[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):],REAL:] is Relation-like set

bool [:[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):],REAL:] is non empty set

the distance of MetrStruct(# D,f #) . (c

the distance of MetrStruct(# D,f #) . (b,c

the distance of MetrStruct(# D,f #) . (c

the distance of MetrStruct(# D,f #) . (b,c) is V27() real ext-real Element of REAL

D is set

[:D,D:] is Relation-like set

[:[:D,D:],REAL:] is Relation-like set

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

f is Relation-like [:D,D:] -defined REAL -valued Function-like V33([:D,D:], REAL ) Element of bool [:[:D,D:],REAL:]

MetrStruct(# D,f #) is strict MetrStruct

the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is non empty strict Reflexive discerning V96() triangle Discerning MetrStruct

( the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty strict TopSpace-like TopStruct

the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is non empty set

( the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) is Element of bool (bool the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct )

bool the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is non empty set

bool (bool the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty set

TopStruct(# the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ,( the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) #) is non empty strict TopStruct

f is non empty strict TopSpace-like TopStruct

the carrier of f is non empty set

[: the carrier of f, the carrier of f:] is non empty Relation-like set

[:[: the carrier of f, the carrier of f:],REAL:] is Relation-like set

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

the distance of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is Relation-like [: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :] -defined REAL -valued Function-like V33([: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :], REAL ) Element of bool [:[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :],REAL:]

[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :] is non empty Relation-like set

[:[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :],REAL:] is Relation-like set

bool [:[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :],REAL:] is non empty set

f is Relation-like [: the carrier of f, the carrier of f:] -defined REAL -valued Function-like V33([: the carrier of f, the carrier of f:], REAL ) Element of bool [:[: the carrier of f, the carrier of f:],REAL:]

( the carrier of f,f) is strict Reflexive discerning V96() triangle MetrStruct

(( the carrier of f,f)) is Element of bool (bool the carrier of ( the carrier of f,f))

the carrier of ( the carrier of f,f) is set

bool the carrier of ( the carrier of f,f) is non empty set

bool (bool the carrier of ( the carrier of f,f)) is non empty set

the topology of f is non empty open Element of bool (bool the carrier of f)

bool the carrier of f is non empty set

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

D is non empty set

[:D,D:] is non empty Relation-like set

[:[:D,D:],REAL:] is Relation-like set

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

f is Relation-like [:D,D:] -defined REAL -valued Function-like V33([:D,D:], REAL ) Element of bool [:[:D,D:],REAL:]

(D,f) is strict Reflexive discerning V96() triangle MetrStruct

MetrStruct(# D,f #) is strict MetrStruct