:: BORSUK_4 semantic presentation

REAL is V143() V144() V145() V149() non bounded_below non bounded_above interval set

NAT is V143() V144() V145() V146() V147() V148() V149() bounded_below Element of bool REAL

bool REAL is non empty set

omega is V143() V144() V145() V146() V147() V148() V149() bounded_below set

bool omega is non empty set

bool NAT is non empty set

1 is non empty natural V72() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT

[:1,1:] is non empty set

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

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

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

[:[:1,1:],REAL:] is set

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

[:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

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

2 is non empty natural V72() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT

[:2,2:] is non empty set

[:[:2,2:],REAL:] is set

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

COMPLEX is V143() V149() set

RAT is V143() V144() V145() V146() V149() set

INT is V143() V144() V145() V146() V147() V149() set

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

TOP-REAL 2 is non empty non trivial TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL 2) is functional non empty non trivial set

bool the carrier of (TOP-REAL 2) is non empty set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V197() TopStruct

the carrier of I[01] is non empty V143() V144() V145() set

K199() is V85() V197() L7()

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

0 is empty trivial natural V72() real ext-real non positive non negative V80() V81() V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of NAT

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (0,1)) is non empty V143() V144() V145() set

ExtREAL is V144() interval set

[:COMPLEX,COMPLEX:] is set

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

[:COMPLEX,REAL:] is set

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

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

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

[:RAT,RAT:] is set

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

[:[:RAT,RAT:],RAT:] is set

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

[:INT,INT:] is set

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

[:[:INT,INT:],INT:] is set

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

[:NAT,NAT:] is set

[:[:NAT,NAT:],NAT:] is set

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

{} is empty trivial V143() V144() V145() V146() V147() V148() V149() bounded_below interval set

[.0,1.] is V143() V144() V145() closed interval Element of bool REAL

the carrier of R^1 is non empty V143() V144() V145() set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V197() SubSpace of R^1

the carrier of I[01] is non empty V143() V144() V145() set

bool the carrier of I[01] is non empty set

bool the carrier of R^1 is non empty set

(#) (0,1) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(0,1) (#) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

bool the carrier of I[01] is non empty set

{0,1} is non empty V143() V144() V145() V146() V147() V148() left_end bounded_below set

the carrier of I[01] \ {0,1} is V143() V144() V145() Element of bool the carrier of I[01]

R^2-unit_square is non empty closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | R^2-unit_square is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | R^2-unit_square) is non empty set

D is non empty closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)

C is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)

x is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)

D is non empty set

bool D is non empty set

C is non empty Element of bool D

D is non empty non trivial set

C is set

{C} is non empty trivial set

D \ {C} is Element of bool D

bool D is non empty set

x is set

y is Element of D

D is non empty non trivial set

bool D is non empty set

C is non empty non trivial Element of bool D

x is set

{x} is non empty trivial set

C \ {x} is Element of bool D

y9 is set

Y is Element of D

D is Relation-like Function-like set

C is Relation-like Function-like set

dom D is set

dom C is set

(dom D) /\ (dom C) is set

rng D is set

rng C is set

(rng D) /\ (rng C) is set

D +* C is Relation-like Function-like set

x is set

{x} is non empty trivial set

D . x is set

{(D . x)} is non empty trivial set

(dom D) \ (dom C) is Element of bool (dom D)

bool (dom D) is non empty set

y is set

y9 is set

C . y is set

D . y9 is set

D is Relation-like Function-like set

C is Relation-like Function-like set

dom D is set

dom C is set

(dom D) /\ (dom C) is set

rng D is set

rng C is set

(rng D) /\ (rng C) is set

D +* C is Relation-like Function-like set

(D +* C) " is Relation-like Function-like set

D " is Relation-like Function-like set

C " is Relation-like Function-like set

(D ") +* (C ") is Relation-like Function-like set

x is set

{x} is non empty trivial set

D . x is set

{(D . x)} is non empty trivial set

C . x is set

dom (C ") is set

dom (D ") is set

(dom (D ")) /\ (dom (C ")) is set

y is set

(D ") . y is set

(C ") . y is set

Y is set

D . Y is set

C . Y is set

dom ((D ") +* (C ")) is set

(dom (D ")) \/ (dom (C ")) is set

(rng D) \/ (dom (C ")) is set

(rng D) \/ (rng C) is set

rng (D +* C) is set

dom (D +* C) is set

(dom D) \/ (dom C) is set

Y is set

Cy is set

((D ") +* (C ")) . Y is set

(D +* C) . Cy is set

(D ") . Y is set

D . Cy is set

(C ") . Y is set

C . Cy is set

D . Cy is set

(D ") . Y is set

C . Cy is set

(C ") . Y is set

D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL D) is functional non empty set

bool the carrier of (TOP-REAL D) is non empty set

C is Element of bool the carrier of (TOP-REAL D)

x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL D)

C \ {x} is Element of bool the carrier of (TOP-REAL D)

{x,y} is non empty Element of bool the carrier of (TOP-REAL D)

C \ {x,y} is Element of bool the carrier of (TOP-REAL D)

D is V72() real ext-real set

C is V72() real ext-real set

x is V72() real ext-real set

y is V72() real ext-real set

1 - y is V72() real ext-real set

(1 - y) * C is V72() real ext-real set

y * x is V72() real ext-real set

((1 - y) * C) + (y * x) is V72() real ext-real set

(1 - y) * D is V72() real ext-real set

y * D is V72() real ext-real set

((1 - y) * D) + (y * D) is V72() real ext-real set

1 * D is V72() real ext-real set

D is V143() V144() V145() Element of bool the carrier of I[01]

x is V72() real ext-real set

C is V72() real ext-real set

].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

D is V143() V144() V145() Element of bool the carrier of I[01]

x is V72() real ext-real set

C is V72() real ext-real set

].C,x.] is V143() V144() V145() non left_end interval Element of bool REAL

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

D is V143() V144() V145() Element of bool the carrier of I[01]

x is V72() real ext-real set

C is V72() real ext-real set

[.C,x.[ is V143() V144() V145() non right_end interval Element of bool REAL

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

D is V72() real ext-real set

C is V72() real ext-real set

].D,C.] is V143() V144() V145() non left_end interval Element of bool REAL

Cl ].D,C.] is V143() V144() V145() Element of bool REAL

[.D,C.] is V143() V144() V145() closed interval Element of bool REAL

].D,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

Cl ].D,C.[ is V143() V144() V145() Element of bool REAL

D is V72() real ext-real set

C is V72() real ext-real set

[.D,C.[ is V143() V144() V145() non right_end interval Element of bool REAL

Cl [.D,C.[ is V143() V144() V145() Element of bool REAL

[.D,C.] is V143() V144() V145() closed interval Element of bool REAL

].D,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

Cl ].D,C.[ is V143() V144() V145() Element of bool REAL

D is V143() V144() V145() Element of bool the carrier of I[01]

Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]

x is V72() real ext-real set

C is V72() real ext-real set

].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

Cl ].C,x.[ is V143() V144() V145() Element of bool REAL

y is V143() V144() V145() Element of bool the carrier of R^1

Cl y is closed V143() V144() V145() Element of bool the carrier of R^1

[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]

(Cl y) /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]

[.C,x.] /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]

D is V143() V144() V145() Element of bool the carrier of I[01]

Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]

x is V72() real ext-real set

C is V72() real ext-real set

].C,x.] is V143() V144() V145() non left_end interval Element of bool REAL

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

Cl ].C,x.] is V143() V144() V145() Element of bool REAL

y is V143() V144() V145() Element of bool the carrier of R^1

Cl y is closed V143() V144() V145() Element of bool the carrier of R^1

[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]

(Cl y) /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]

[.C,x.] /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]

D is V143() V144() V145() Element of bool the carrier of I[01]

Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]

x is V72() real ext-real set

C is V72() real ext-real set

[.C,x.[ is V143() V144() V145() non right_end interval Element of bool REAL

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

Cl [.C,x.[ is V143() V144() V145() Element of bool REAL

y is V143() V144() V145() Element of bool the carrier of R^1

Cl y is closed V143() V144() V145() Element of bool the carrier of R^1

[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]

(Cl y) /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]

[.C,x.] /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]

D is V143() V144() V145() Element of bool the carrier of I[01]

C is V72() real ext-real set

x is V72() real ext-real set

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

D is V143() V144() V145() Element of bool the carrier of I[01]

C is V143() V144() V145() Element of bool the carrier of I[01]

y is V72() real ext-real set

x is V72() real ext-real set

y9 is V72() real ext-real set

[.x,y.[ is V143() V144() V145() non right_end interval Element of bool REAL

].y,y9.] is V143() V144() V145() non left_end interval Element of bool REAL

Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]

[.x,y.] is V143() V144() V145() closed interval Element of bool REAL

Cl C is closed V143() V144() V145() Element of bool the carrier of I[01]

[.y,y9.] is V143() V144() V145() closed interval Element of bool REAL

D is V72() real ext-real Element of the carrier of I[01]

C is V72() real ext-real Element of the carrier of I[01]

[.D,C.] is V143() V144() V145() closed interval Element of bool REAL

D is V72() real ext-real Element of the carrier of I[01]

C is V72() real ext-real Element of the carrier of I[01]

].D,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

[.D,C.] is V143() V144() V145() closed interval Element of bool REAL

D is V72() real ext-real set

{D} is non empty trivial V143() V144() V145() Element of bool REAL

[.D,D.] is V143() V144() V145() closed interval Element of bool REAL

D is non empty connected V143() V144() V145() Element of bool the carrier of I[01]

C is V72() real ext-real Element of the carrier of I[01]

x is V72() real ext-real Element of the carrier of I[01]

y is V72() real ext-real Element of the carrier of I[01]

].x,1.] is V143() V144() V145() non left_end interval Element of bool REAL

[.x,1.] is V143() V144() V145() closed interval Element of bool REAL

[.0,x.[ is V143() V144() V145() non right_end interval Element of bool REAL

[.0,x.] is V143() V144() V145() closed interval Element of bool REAL

{x} is non empty trivial V143() V144() V145() Element of bool REAL

[.0,1.] \ {x} is V143() V144() V145() Element of bool REAL

[.0,x.[ \/ ].x,1.] is V143() V144() V145() Element of bool REAL

y9 is non empty V143() V144() V145() Element of bool the carrier of I[01]

Y is non empty V143() V144() V145() Element of bool the carrier of I[01]

y9 is non empty V143() V144() V145() Element of bool the carrier of I[01]

Y is non empty V143() V144() V145() Element of bool the carrier of I[01]

D is non empty connected V143() V144() V145() Element of bool the carrier of I[01]

C is V72() real ext-real set

x is V72() real ext-real set

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

y is set

{ b

y9 is V72() real ext-real Element of REAL

Y is V72() real ext-real Element of the carrier of I[01]

D is V72() real ext-real set

C is V72() real ext-real set

[.D,C.] is V143() V144() V145() closed interval Element of bool REAL

x is V143() V144() V145() Element of bool the carrier of I[01]

Closed-Interval-TSpace (D,C) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1

bool the carrier of (Closed-Interval-TSpace (0,1)) is non empty set

the carrier of (Closed-Interval-TSpace (D,C)) is non empty V143() V144() V145() set

y is V143() V144() V145() Element of bool the carrier of (Closed-Interval-TSpace (0,1))

{} I[01] is empty trivial proper open closed connected compact V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of bool the carrier of I[01]

D is V72() real ext-real Element of the carrier of I[01]

C is V72() real ext-real Element of the carrier of I[01]

[.D,C.] is V143() V144() V145() closed interval Element of bool REAL

Closed-Interval-TSpace (D,C) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1

y is V143() V144() V145() Element of bool the carrier of I[01]

I[01] | y is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

D is V143() V144() V145() Element of bool the carrier of I[01]

C is V143() V144() V145() Element of bool REAL

x is ext-real set

x is ext-real set

D is V143() V144() V145() Element of bool the carrier of I[01]

C is V143() V144() V145() Element of bool REAL

lower_bound C is V72() real ext-real Element of REAL

upper_bound C is V72() real ext-real Element of REAL

x is V72() real ext-real set

C is V143() V144() V145() Element of bool REAL

x is V143() V144() V145() Element of bool the carrier of I[01]

y is V143() V144() V145() Element of bool the carrier of R^1

[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]

y /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]

D is V143() V144() V145() Element of bool the carrier of R^1

D is non empty V143() V144() V145() closed_interval interval Element of bool REAL

lower_bound D is V72() real ext-real Element of REAL

upper_bound D is V72() real ext-real Element of REAL

the V72() real ext-real Element of D is V72() real ext-real Element of D

D is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]

C is V143() V144() V145() Element of bool REAL

lower_bound C is V72() real ext-real Element of REAL

upper_bound C is V72() real ext-real Element of REAL

[.(lower_bound C),(upper_bound C).] is V143() V144() V145() closed interval Element of bool REAL

x is set

y is V72() real ext-real set

D is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]

C is V143() V144() V145() Element of bool REAL

lower_bound C is V72() real ext-real Element of REAL

upper_bound C is V72() real ext-real Element of REAL

[.(lower_bound C),(upper_bound C).] is V143() V144() V145() closed interval Element of bool REAL

D is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]

C is non empty V143() V144() V145() closed_interval interval Element of bool REAL

lower_bound C is V72() real ext-real Element of REAL

upper_bound C is V72() real ext-real Element of REAL

[.(lower_bound C),(upper_bound C).] is V143() V144() V145() closed interval Element of bool REAL

x is V72() real ext-real Element of the carrier of I[01]

y is V72() real ext-real Element of the carrier of I[01]

[.x,y.] is V143() V144() V145() closed interval Element of bool REAL

].0,1.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

D is V143() V144() V145() Element of bool the carrier of I[01]

I[01] | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of (I[01] | D) is V143() V144() V145() set

D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of D is V143() V144() V145() set

C is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of C is V143() V144() V145() set

() is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of () is V143() V144() V145() set

the carrier of () is non empty V143() V144() V145() set

D is V143() V144() V145() Element of bool the carrier of I[01]

I[01] | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of I[01] \ {0,1} is V143() V144() V145() Element of bool the carrier of I[01]

].0,1.[ \/ {0,1} is non empty V143() V144() V145() set

D is V72() real ext-real set

bool the carrier of () is non empty set

C is V72() real ext-real Element of the carrier of I[01]

D is V72() real ext-real Element of the carrier of I[01]

].D,C.] is V143() V144() V145() non left_end interval Element of bool REAL

x is set

{ b

y is V72() real ext-real Element of REAL

C is V72() real ext-real Element of the carrier of I[01]

D is V72() real ext-real Element of the carrier of I[01]

[.D,C.[ is V143() V144() V145() non right_end interval Element of bool REAL

x is set

{ b

y is V72() real ext-real Element of REAL

D is non empty non trivial closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | D is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | D) is non empty set

[: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | D):] is non empty set

bool [: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | D):] is non empty set

C is Relation-like the carrier of ((TOP-REAL 2) | R^2-unit_square) -defined the carrier of ((TOP-REAL 2) | D) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | D):]

C is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL C) is functional non empty set

bool the carrier of (TOP-REAL C) is non empty set

x is non empty Element of bool the carrier of (TOP-REAL C)

y is V35(C) V77() V135() Element of the carrier of (TOP-REAL C)

y9 is V35(C) V77() V135() Element of the carrier of (TOP-REAL C)

{y,y9} is non empty Element of bool the carrier of (TOP-REAL C)

x \ {y,y9} is Element of bool the carrier of (TOP-REAL C)

(TOP-REAL C) | (x \ {y,y9}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C

(TOP-REAL C) | x is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C

the carrier of ((TOP-REAL C) | x) is non empty set

[: the carrier of I[01], the carrier of ((TOP-REAL C) | x):] is non empty set

bool [: the carrier of I[01], the carrier of ((TOP-REAL C) | x):] is non empty set

Y is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL C) | x) -valued Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL C) | x):]

Y . 0 is set

Y . 1 is set

rng Y is Element of bool the carrier of ((TOP-REAL C) | x)

bool the carrier of ((TOP-REAL C) | x) is non empty set

[#] ((TOP-REAL C) | x) is non empty non proper open closed Element of bool the carrier of ((TOP-REAL C) | x)

dom Y is V143() V144() V145() Element of bool the carrier of I[01]

Y .: the carrier of () is Element of bool the carrier of ((TOP-REAL C) | x)

Y .: the carrier of I[01] is Element of bool the carrier of ((TOP-REAL C) | x)

Y .: {0,1} is Element of bool the carrier of ((TOP-REAL C) | x)

(Y .: the carrier of I[01]) \ (Y .: {0,1}) is Element of bool the carrier of ((TOP-REAL C) | x)

x \ (Y .: {0,1}) is Element of bool the carrier of (TOP-REAL C)

p1 is non empty Element of bool the carrier of (TOP-REAL C)

(TOP-REAL C) | p1 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C

Cy is Element of bool the carrier of ((TOP-REAL C) | x)

((TOP-REAL C) | x) | Cy is strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL C) | x

Y /" is Relation-like the carrier of ((TOP-REAL C) | x) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:]

[: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:] is non empty set

bool [: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:] is non empty set

(Y /") | p1 is Relation-like the carrier of ((TOP-REAL C) | x) -defined the carrier of I[01] -valued Function-like Element of bool [: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:]

the carrier of ((TOP-REAL C) | p1) is non empty set

[: the carrier of ((TOP-REAL C) | p1), the carrier of I[01]:] is non empty set

bool [: the carrier of ((TOP-REAL C) | p1), the carrier of I[01]:] is non empty set

B is Relation-like the carrier of ((TOP-REAL C) | p1) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL C) | p1), the carrier of I[01]:]

Y | the carrier of () is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL C) | x) -valued Function-like Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL C) | x):]

D is V143() V144() V145() Element of bool the carrier of I[01]

I[01] | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of (I[01] | D) is V143() V144() V145() set

[: the carrier of (I[01] | D), the carrier of ((TOP-REAL C) | x):] is set

bool [: the carrier of (I[01] | D), the carrier of ((TOP-REAL C) | x):] is non empty set

dom (Y | the carrier of ()) is V143() V144() V145() Element of bool the carrier of I[01]

Y " is Relation-like Function-like set

rng (Y | the carrier of ()) is Element of bool the carrier of ((TOP-REAL C) | x)

the carrier of ((TOP-REAL C) | (x \ {y,y9})) is set

[: the carrier of (), the carrier of ((TOP-REAL C) | (x \ {y,y9})):] is set

bool [: the carrier of (), the carrier of ((TOP-REAL C) | (x \ {y,y9})):] is non empty set

fC9 is Relation-like the carrier of () -defined the carrier of ((TOP-REAL C) | (x \ {y,y9})) -valued Function-like quasi_total Element of bool [: the carrier of (), the carrier of ((TOP-REAL C) | (x \ {y,y9})):]

dom fC9 is V143() V144() V145() Element of bool the carrier of ()

[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()

fC9 /" is Relation-like the carrier of ((TOP-REAL C) | (x \ {y,y9})) -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL C) | (x \ {y,y9})), the carrier of ():]

[: the carrier of ((TOP-REAL C) | (x \ {y,y9})), the carrier of ():] is set

bool [: the carrier of ((TOP-REAL C) | (x \ {y,y9})), the carrier of ():] is non empty set

fC9 " is Relation-like Function-like set

fC9 is Relation-like the carrier of (I[01] | D) -defined the carrier of ((TOP-REAL C) | x) -valued Function-like total quasi_total Element of bool [: the carrier of (I[01] | D), the carrier of ((TOP-REAL C) | x):]

rng fC9 is Element of bool the carrier of ((TOP-REAL C) | (x \ {y,y9}))

bool the carrier of ((TOP-REAL C) | (x \ {y,y9})) is non empty set

[#] ((TOP-REAL C) | (x \ {y,y9})) is non proper open closed Element of bool the carrier of ((TOP-REAL C) | (x \ {y,y9}))

D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL D) is functional non empty set

bool the carrier of (TOP-REAL D) is non empty set

C is Element of bool the carrier of (TOP-REAL D)

(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

the carrier of ((TOP-REAL D) | C) is set

[: the carrier of I[01], the carrier of ((TOP-REAL D) | C):] is set

bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | C):] is non empty set

y9 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL D) | C) -valued Function-like quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | C):]

y9 . 0 is set

y9 . 1 is set

D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL D) is functional non empty set

C is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

LSeg (C,x) is Element of bool the carrier of (TOP-REAL D)

bool the carrier of (TOP-REAL D) is non empty set

(TOP-REAL D) | (LSeg (C,x)) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

D is V143() V144() V145() Element of bool the carrier of ()

() | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()

x is V72() real ext-real Element of the carrier of I[01]

C is V72() real ext-real Element of the carrier of I[01]

[.C,x.] is V143() V144() V145() closed interval Element of bool REAL

Closed-Interval-TSpace (C,x) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1

y is TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of y is V143() V144() V145() set

y9 is TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

(#) (C,x) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (C,x))

the carrier of (Closed-Interval-TSpace (C,x)) is non empty V143() V144() V145() set

(C,x) (#) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (C,x))

L[01] (((#) (C,x)),((C,x) (#))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (C,x)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (C,x)):]

[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (C,x)):] is non empty set

bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (C,x)):] is non empty set

D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL D) is functional non empty set

bool the carrier of (TOP-REAL D) is non empty set

C is Element of bool the carrier of (TOP-REAL D)

(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | C) is set

x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

Y is V72() real ext-real Element of the carrier of I[01]

y9 is V72() real ext-real Element of the carrier of I[01]

[.y9,Y.] is V143() V144() V145() closed interval Element of bool REAL

Cy is non empty V143() V144() V145() Element of bool the carrier of I[01]

I[01] | Cy is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

Closed-Interval-TSpace (y9,Y) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1

the carrier of (I[01] | Cy) is non empty V143() V144() V145() set

[: the carrier of (I[01] | Cy), the carrier of I[01]:] is non empty set

bool [: the carrier of (I[01] | Cy), the carrier of I[01]:] is non empty set

P[01] (y9,Y,((#) (0,1)),((0,1) (#))) is Relation-like the carrier of (Closed-Interval-TSpace (y9,Y)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of (Closed-Interval-TSpace (0,1)):]

the carrier of (Closed-Interval-TSpace (y9,Y)) is non empty V143() V144() V145() set

[: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty set

bool [: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty set

[: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | C):] is set

bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | C):] is non empty set

(#) (y9,Y) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (y9,Y))

p2 is non empty Element of bool the carrier of (TOP-REAL D)

(TOP-REAL D) | p2 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | p2) is non empty set

[: the carrier of I[01], the carrier of ((TOP-REAL D) | p2):] is non empty set

bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | p2):] is non empty set

B is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL D) | p2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | p2):]

B . 0 is set

B . 1 is set

p1 is Relation-like the carrier of (I[01] | Cy) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of I[01]:]

B * p1 is Relation-like the carrier of (I[01] | Cy) -defined the carrier of ((TOP-REAL D) | p2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | p2):]

[: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | p2):] is non empty set

bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | p2):] is non empty set

fC9 is Relation-like the carrier of (I[01] | Cy) -defined the carrier of ((TOP-REAL D) | C) -valued Function-like quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | C):]

fC9 . y9 is set

fC9 . Y is set

p1 . y9 is set

B . (p1 . y9) is set

(y9,Y) (#) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (y9,Y))

p1 . Y is set

B . (p1 . Y) is set

D is TopSpace-like TopStruct

the carrier of D is set

bool the carrier of D is non empty set

C is non empty TopSpace-like TopStruct

the carrier of C is non empty set

[: the carrier of D, the carrier of C:] is set

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

x is Relation-like the carrier of D -defined the carrier of C -valued Function-like total quasi_total Element of bool [: the carrier of D, the carrier of C:]

y is TopSpace-like TopStruct

the carrier of y is set

y9 is Element of bool the carrier of D

D | y9 is strict TopSpace-like SubSpace of D

the carrier of (D | y9) is set

[: the carrier of (D | y9), the carrier of y:] is set

bool [: the carrier of (D | y9), the carrier of y:] is non empty set

x | y9 is Relation-like the carrier of D -defined the carrier of C -valued Function-like Element of bool [: the carrier of D, the carrier of C:]

[: the carrier of (D | y9), the carrier of C:] is set

bool [: the carrier of (D | y9), the carrier of C:] is non empty set

Cy is Relation-like the carrier of (D | y9) -defined the carrier of y -valued Function-like quasi_total Element of bool [: the carrier of (D | y9), the carrier of y:]

Y is Relation-like the carrier of (D | y9) -defined the carrier of C -valued Function-like total quasi_total Element of bool [: the carrier of (D | y9), the carrier of C:]

D is V143() V144() V145() Element of bool the carrier of I[01]

C is V72() real ext-real Element of the carrier of I[01]

x is V72() real ext-real Element of the carrier of I[01]

].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

[.x,1.] is V143() V144() V145() closed interval Element of bool REAL

[.0,C.] is V143() V144() V145() closed interval Element of bool REAL

y is V143() V144() V145() Element of bool the carrier of I[01]

y9 is V143() V144() V145() Element of bool the carrier of I[01]

y9 \/ y is V143() V144() V145() Element of bool the carrier of I[01]

(y9 \/ y) ` is V143() V144() V145() Element of bool the carrier of I[01]

the carrier of I[01] \ (y9 \/ y) is V143() V144() V145() set

D is V143() V144() V145() Element of bool the carrier of ()

C is V72() real ext-real Element of the carrier of I[01]

x is V72() real ext-real Element of the carrier of I[01]

].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

y is V143() V144() V145() Element of bool the carrier of I[01]

D is V143() V144() V145() Element of bool the carrier of ()

C is V72() real ext-real Element of the carrier of I[01]

].0,C.] is V143() V144() V145() non left_end interval Element of bool REAL

[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()

([#] ()) \ D is V143() V144() V145() Element of bool the carrier of ()

].C,1.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

{} () is empty trivial proper open closed connected compact V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of bool the carrier of ()

D is V143() V144() V145() Element of bool the carrier of ()

C is V72() real ext-real Element of the carrier of I[01]

[.C,1.[ is V143() V144() V145() non right_end interval Element of bool REAL

[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()

([#] ()) \ D is V143() V144() V145() Element of bool the carrier of ()

].0,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL

D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL D) is functional non empty set

bool the carrier of (TOP-REAL D) is non empty set

C is Element of bool the carrier of (TOP-REAL D)

x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL D)

C \ {x} is Element of bool the carrier of (TOP-REAL D)

(TOP-REAL D) | (C \ {x}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | (C \ {x})) is set

Y is V72() real ext-real Element of the carrier of I[01]

y9 is V72() real ext-real Element of the carrier of I[01]

].y9,Y.] is V143() V144() V145() non left_end interval Element of bool REAL

Cy is non empty Element of bool the carrier of (TOP-REAL D)

(TOP-REAL D) | Cy is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | Cy) is non empty set

[.y9,Y.] is V143() V144() V145() closed interval Element of bool REAL

p1 is non empty V143() V144() V145() Element of bool the carrier of I[01]

I[01] | p1 is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of (I[01] | p1) is non empty V143() V144() V145() set

[: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):] is non empty set

bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):] is non empty set

p2 is Relation-like the carrier of (I[01] | p1) -defined the carrier of ((TOP-REAL D) | Cy) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):]

p2 . y9 is set

p2 . Y is set

dom p2 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)

bool the carrier of (I[01] | p1) is non empty set

[#] (I[01] | p1) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (I[01] | p1)

B is non empty V143() V144() V145() Element of bool the carrier of ()

() | B is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()

p2 | B is Relation-like the carrier of (I[01] | p1) -defined the carrier of ((TOP-REAL D) | Cy) -valued Function-like Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):]

p2 /" is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]

[: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set

bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set

(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | C) is set

bool the carrier of ((TOP-REAL D) | C) is non empty set

p1 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)

(I[01] | p1) | p1 is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01] | p1

the carrier of (() | B) is non empty V143() V144() V145() set

fC9 is Element of bool the carrier of ((TOP-REAL D) | C)

((TOP-REAL D) | C) | fC9 is strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL D) | C

dom (p2 | B) is V143() V144() V145() Element of bool the carrier of (I[01] | p1)

[#] (() | B) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (() | B)

bool the carrier of (() | B) is non empty set

rng p2 is Element of bool the carrier of ((TOP-REAL D) | Cy)

bool the carrier of ((TOP-REAL D) | Cy) is non empty set

[#] ((TOP-REAL D) | C) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | C)

{y9} is non empty trivial V143() V144() V145() Element of bool REAL

p1 \ {y9} is V143() V144() V145() Element of bool the carrier of I[01]

p2 .: B is Element of bool the carrier of ((TOP-REAL D) | Cy)

p2 .: p1 is Element of bool the carrier of ((TOP-REAL D) | Cy)

Im (p2,y9) is set

{y9} is non empty trivial V143() V144() V145() set

p2 .: {y9} is set

(p2 .: p1) \ (Im (p2,y9)) is Element of bool the carrier of ((TOP-REAL D) | Cy)

{(p2 . y9)} is non empty trivial set

(p2 .: p1) \ {(p2 . y9)} is Element of bool the carrier of ((TOP-REAL D) | Cy)

(rng p2) \ {x} is Element of bool the carrier of ((TOP-REAL D) | Cy)

[#] ((TOP-REAL D) | (C \ {x})) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | (C \ {x}))

bool the carrier of ((TOP-REAL D) | (C \ {x})) is non empty set

rng (p2 | B) is Element of bool the carrier of ((TOP-REAL D) | Cy)

[: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {x})):] is set

bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {x})):] is non empty set

p2 is Relation-like the carrier of (() | B) -defined the carrier of ((TOP-REAL D) | (C \ {x})) -valued Function-like quasi_total Element of bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {x})):]

p2 . Y is set

p2 /" is Relation-like the carrier of ((TOP-REAL D) | (C \ {x})) -defined the carrier of (() | B) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | (C \ {x})), the carrier of (() | B):]

[: the carrier of ((TOP-REAL D) | (C \ {x})), the carrier of (() | B):] is set

bool [: the carrier of ((TOP-REAL D) | (C \ {x})), the carrier of (() | B):] is non empty set

p2 " is Relation-like Function-like set

p2 " is Relation-like Function-like set

(p2 ") | (p2 .: B) is Relation-like set

(p2 /") | ([#] ((TOP-REAL D) | (C \ {x}))) is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]

(p2 /") | fC9 is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]

D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL D) is functional non empty set

bool the carrier of (TOP-REAL D) is non empty set

C is Element of bool the carrier of (TOP-REAL D)

x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)

{y} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL D)

C \ {y} is Element of bool the carrier of (TOP-REAL D)

(TOP-REAL D) | (C \ {y}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | (C \ {y})) is set

Y is V72() real ext-real Element of the carrier of I[01]

y9 is V72() real ext-real Element of the carrier of I[01]

[.y9,Y.[ is V143() V144() V145() non right_end interval Element of bool REAL

Cy is non empty Element of bool the carrier of (TOP-REAL D)

(TOP-REAL D) | Cy is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | Cy) is non empty set

[.y9,Y.] is V143() V144() V145() closed interval Element of bool REAL

p1 is non empty V143() V144() V145() Element of bool the carrier of I[01]

I[01] | p1 is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]

the carrier of (I[01] | p1) is non empty V143() V144() V145() set

[: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):] is non empty set

bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):] is non empty set

p2 is Relation-like the carrier of (I[01] | p1) -defined the carrier of ((TOP-REAL D) | Cy) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):]

p2 . y9 is set

p2 . Y is set

dom p2 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)

bool the carrier of (I[01] | p1) is non empty set

[#] (I[01] | p1) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (I[01] | p1)

B is non empty V143() V144() V145() Element of bool the carrier of ()

() | B is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()

p2 | B is Relation-like the carrier of (I[01] | p1) -defined the carrier of ((TOP-REAL D) | Cy) -valued Function-like Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):]

p2 /" is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]

[: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set

bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set

(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D

the carrier of ((TOP-REAL D) | C) is set

bool the carrier of ((TOP-REAL D) | C) is non empty set

p1 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)

(I[01] | p1) | p1 is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01] | p1

the carrier of (() | B) is non empty V143() V144() V145() set

fC9 is Element of bool the carrier of ((TOP-REAL D) | C)

((TOP-REAL D) | C) | fC9 is strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL D) | C

dom (p2 | B) is V143() V144() V145() Element of bool the carrier of (I[01] | p1)

[#] (() | B) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (() | B)

bool the carrier of (() | B) is non empty set

rng p2 is Element of bool the carrier of ((TOP-REAL D) | Cy)

bool the carrier of ((TOP-REAL D) | Cy) is non empty set

[#] ((TOP-REAL D) | C) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | C)

{Y} is non empty trivial V143() V144() V145() Element of bool REAL

p1 \ {Y} is V143() V144() V145() Element of bool the carrier of I[01]

p2 .: B is Element of bool the carrier of ((TOP-REAL D) | Cy)

p2 .: p1 is Element of bool the carrier of ((TOP-REAL D) | Cy)

Im (p2,Y) is set

{Y} is non empty trivial V143() V144() V145() set

p2 .: {Y} is set

(p2 .: p1) \ (Im (p2,Y)) is Element of bool the carrier of ((TOP-REAL D) | Cy)

{(p2 . Y)} is non empty trivial set

(p2 .: p1) \ {(p2 . Y)} is Element of bool the carrier of ((TOP-REAL D) | Cy)

(rng p2) \ {y} is Element of bool the carrier of ((TOP-REAL D) | Cy)

[#] ((TOP-REAL D) | (C \ {y})) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | (C \ {y}))

bool the carrier of ((TOP-REAL D) | (C \ {y})) is non empty set

rng (p2 | B) is Element of bool the carrier of ((TOP-REAL D) | Cy)

[: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {y})):] is set

bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {y})):] is non empty set

p2 is Relation-like the carrier of (() | B) -defined the carrier of ((TOP-REAL D) | (C \ {y})) -valued Function-like quasi_total Element of bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {y})):]

p2 . y9 is set

p2 /" is Relation-like the carrier of ((TOP-REAL D) | (C \ {y})) -defined the carrier of (() | B) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | (C \ {y})), the carrier of (() | B):]

[: the carrier of ((TOP-REAL D) | (C \ {y})), the carrier of (() | B):] is set

bool [: the carrier of ((TOP-REAL D) | (C \ {y})), the carrier of (() | B):] is non empty set

p2 " is Relation-like Function-like set

p2 " is Relation-like Function-like set

(p2 ") | (p2 .: B) is Relation-like set

(p2 /") | ([#] ((TOP-REAL D) | (C \ {y}))) is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]

(p2 /") | fC9 is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]

1 / 2 is V72() real ext-real non negative set

y is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

TOP-REAL y is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL y) is functional non empty set

bool the carrier of (TOP-REAL y) is non empty set

y9 is Element of bool the carrier of (TOP-REAL y)

Y is Element of bool the carrier of (TOP-REAL y)

y9 /\ Y is Element of bool the carrier of (TOP-REAL y)

Cy is V35(y) V77() V135() Element of the carrier of (TOP-REAL y)

p1 is V35(y) V77() V135() Element of the carrier of (TOP-REAL y)

{Cy,p1} is non empty Element of bool the carrier of (TOP-REAL y)

{Cy} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL y)

y9 \ {Cy} is Element of bool the carrier of (TOP-REAL y)

Y \ {Cy} is Element of bool the carrier of (TOP-REAL y)

(y9 \ {Cy}) \/ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)

(TOP-REAL y) | ((y9 \ {Cy}) \/ (Y \ {Cy})) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y

(TOP-REAL y) | (Y \ {Cy}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y

the carrier of ((TOP-REAL y) | (Y \ {Cy})) is set

C is V72() real ext-real Element of the carrier of I[01]

x is V72() real ext-real Element of the carrier of I[01]

[.C,x.[ is V143() V144() V145() non right_end interval Element of bool REAL

p2 is non empty V143() V144() V145() Element of bool the carrier of ()

() | p2 is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()

the carrier of (() | p2) is non empty V143() V144() V145() set

[: the carrier of (() | p2), the carrier of ((TOP-REAL y) | (Y \ {Cy})):] is set

bool [: the carrier of (() | p2), the carrier of ((TOP-REAL y) | (Y \ {Cy})):] is non empty set

B is Relation-like the carrier of (() | p2) -defined the carrier of ((TOP-REAL y) | (Y \ {Cy})) -valued Function-like quasi_total Element of bool [: the carrier of (() | p2), the carrier of ((TOP-REAL y) | (Y \ {Cy})):]

B . C is set

(TOP-REAL y) | (y9 \ {Cy}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y

the carrier of ((TOP-REAL y) | (y9 \ {Cy})) is set

D is V72() real ext-real Element of the carrier of I[01]

].D,C.] is V143() V144() V145() non left_end interval Element of bool REAL

c

() | c

the carrier of (() | c

[: the carrier of (() | c

bool [: the carrier of (() | c

fC9 is Relation-like the carrier of (() | c

fC9 . C is set

s2 is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y

the carrier of s2 is non empty set

U2 is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y

the carrier of U2 is non empty set

[: the carrier of (() | p2), the carrier of s2:] is non empty set

bool [: the carrier of (() | p2), the carrier of s2:] is non empty set

ty9 is Relation-like the carrier of (() | p2) -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of (() | p2), the carrier of s2:]

[#] (() | c

bool the carrier of (() | c

[#] (() | p2) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (() | p2)

bool the carrier of (() | p2) is non empty set

F2 is non empty V143() V144() V145() Element of bool the carrier of ()

[.(1 / 2),1.[ is V143() V144() V145() non right_end interval Element of bool REAL

c

the carrier of c

[: the carrier of (() | c

bool [: the carrier of (() | c

rng B is Element of bool the carrier of ((TOP-REAL y) | (Y \ {Cy}))

bool the carrier of ((TOP-REAL y) | (Y \ {Cy})) is non empty set

[#] ((TOP-REAL y) | (Y \ {Cy})) is non proper open closed Element of bool the carrier of ((TOP-REAL y) | (Y \ {Cy}))

rng fC9 is Element of bool the carrier of ((TOP-REAL y) | (y9 \ {Cy}))

bool the carrier of ((TOP-REAL y) | (y9 \ {Cy})) is non empty set

[#] ((TOP-REAL y) | (y9 \ {Cy})) is non proper open closed Element of bool the carrier of ((TOP-REAL y) | (y9 \ {Cy}))

sx9 is Relation-like the carrier of (() | c

rng sx9 is Element of bool the carrier of s2

bool the carrier of s2 is non empty set

rng ty9 is Element of bool the carrier of s2

(rng sx9) /\ (rng ty9) is Element of bool the carrier of s2

(y9 \ {Cy}) /\ Y is Element of bool the carrier of (TOP-REAL y)

((y9 \ {Cy}) /\ Y) \ {Cy} is Element of bool the carrier of (TOP-REAL y)

(y9 /\ Y) \ {Cy} is Element of bool the carrier of (TOP-REAL y)

((y9 /\ Y) \ {Cy}) \ {Cy} is Element of bool the carrier of (TOP-REAL y)

{Cy} \/ {Cy} is non empty closed Element of bool the carrier of (TOP-REAL y)

(y9 /\ Y) \ ({Cy} \/ {Cy}) is Element of bool the carrier of (TOP-REAL y)

sx9 . C is set

{(sx9 . C)} is non empty trivial set

F1 is non empty V143() V144() V145() Element of bool the carrier of ()

].0,(1 / 2).] is V143() V144() V145() non left_end interval Element of bool REAL

([#] (() | c

[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()

([#] (() | c

{(1 / 2)} is non empty trivial V143() V144() V145() Element of bool REAL

F is set

fC9 . F is set

B . F is set

[: the carrier of (), the carrier of s2:] is non empty set

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

sx9 +* B is Relation-like Function-like set

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

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

bool the carrier of U2 is non empty set

[: the carrier of U2, the carrier of ():] is non empty set

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

B /" is Relation-like the carrier of ((TOP-REAL y) | (Y \ {Cy})) -defined the carrier of (() | p2) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL y) | (Y \ {Cy})), the carrier of (() | p2):]

[: the carrier of ((TOP-REAL y) | (Y \ {Cy})), the carrier of (() | p2):] is set

bool [: the carrier of ((TOP-REAL y) | (Y \ {Cy})), the carrier of (() | p2):] is non empty set

[: the carrier of c

bool [: the carrier of c

fC9 /" is Relation-like the carrier of ((TOP-REAL y) | (y9 \ {Cy})) -defined the carrier of (() | c

[: the carrier of ((TOP-REAL y) | (y9 \ {Cy})), the carrier of (() | c

bool [: the carrier of ((TOP-REAL y) | (y9 \ {Cy})), the carrier of (() | c

dom ty9 is V143() V144() V145() Element of bool the carrier of (() | p2)

[#] c

bool the carrier of c

dom F is V143() V144() V145() Element of bool the carrier of ()

V2 is Element of bool the carrier of s2

r is Element of bool the carrier of (TOP-REAL y)

{p1} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL y)

Y /\ (y9 \ {Cy}) is Element of bool the carrier of (TOP-REAL y)

Y /\ y9 is Element of bool the carrier of (TOP-REAL y)

(Y /\ y9) \ {Cy} is Element of bool the carrier of (TOP-REAL y)

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

r /\ ([#] s2) is Element of bool the carrier of s2

r /\ ((y9 \ {Cy}) \/ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)

Y /\ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)

(Y /\ (y9 \ {Cy})) \/ (Y /\ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)

(Y /\ (y9 \ {Cy})) \/ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)

V1 is Element of bool the carrier of s2

r is Element of bool the carrier of (TOP-REAL y)

{p1} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL y)

y9 /\ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)

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

r /\ ([#] s2) is Element of bool the carrier of s2

r /\ ((y9 \ {Cy}) \/ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)

y9 /\ (y9 \ {Cy}) is Element of bool the carrier of (TOP-REAL y)

(y9 /\ (y9 \ {Cy})) \/ (y9 /\ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)

(y9 \ {Cy}) \/ (y9 /\ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)

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

f is Relation-like the carrier of c

B " is Relation-like Function-like set

dom sx9 is V143() V144() V145() Element of bool the carrier of (() | c

(dom sx9) /\ (dom ty9) is V143() V144() V145() Element of bool the carrier of (() | p2)

{C} is non empty trivial V143() V144() V145() Element of bool REAL

r is set

dom sx9 is set

dom ty9 is set

(dom sx9) /\ (dom ty9) is set

sx9 . r is set

ty9 . r is set

rng F is Element of bool the carrier of s2

(rng sx9) \/ (rng ty9) is Element of bool the carrier of s2

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

fC9 " is Relation-like Function-like set

([#] c

r is set

f . r is set

g . r is set

dom B is V143() V144() V145() Element of bool the carrier of (() | p2)

dom fC9 is V143() V144() V145() Element of bool the carrier of (() | c

f . p1 is set

([#] c

[: the carrier of s2, the carrier of ():] is non empty set

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

f +* g is Relation-like Function-like set

F /" is Relation-like the carrier of s2 -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of s2, the carrier of ():]

F " is Relation-like Function-like set

(fC9 /") +* (B /") is Relation-like Function-like set

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

D is non empty non trivial closed