:: BORSUK_2 semantic presentation

REAL is V33() V34() V35() V39() V138() V139() V141() set

NAT is V33() V34() V35() V36() V37() V38() V39() V138() Element of bool REAL

bool REAL is non empty set

{} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V138() V141() set

the empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V138() V141() set is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V138() V141() set

1 is non empty natural V31() real V33() V34() V35() V36() V37() V38() ext-real positive V136() V138() Element of NAT

{{},1} is non empty set

omega is V33() V34() V35() V36() V37() V38() V39() V138() set

bool omega is non empty set

bool NAT is non empty set

I[01] is non empty strict TopSpace-like V130() TopStruct

the carrier of I[01] is non empty V33() V34() V35() set

[: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 natural V31() real V33() V34() V35() V36() V37() V38() ext-real positive V136() V138() 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

K300() is non empty V116() V121() V122() V123() V124() V126() V130() L7()

R^1 is non empty strict TopSpace-like V130() TopStruct

0 is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional natural V31() real V33() V34() V35() V36() V37() V38() V39() ext-real V138() V141() Element of NAT

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V130() SubSpace of R^1

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

COMPLEX is V33() V39() set

[.0,1.] is V33() V34() V35() V141() Element of bool REAL

0[01] is V31() real ext-real Element of the carrier of I[01]

1[01] is V31() real ext-real Element of the carrier of I[01]

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

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

TopSpaceMetr K300() is TopStruct

I[01] is non empty strict TopSpace-like V130() SubSpace of R^1

the carrier of I[01] is non empty V33() V34() V35() set

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

a is V31() real ext-real set

{ b

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

F

F

{ F

card { F

card F

a is Relation-like Function-like set

dom a is set

rng a is set

b is set

B is Element of F

F

a . B is set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

[#] a is non empty non proper open closed dense non boundary Element of bool the carrier of a

bool the carrier of a is non empty set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

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

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

B is non empty TopSpace-like TopStruct

the carrier of B is non empty set

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

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

[#] B is non empty non proper open closed dense non boundary Element of bool the carrier of B

bool the carrier of B is non empty set

([#] a) \/ ([#] B) is non empty set

([#] a) /\ ([#] B) is Element of bool the carrier of B

g is non empty TopSpace-like TopStruct

[#] g is non empty non proper open closed dense non boundary Element of bool the carrier of g

the carrier of g is non empty set

bool the carrier of g is non empty set

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

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

g is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]

P is non empty Relation-like the carrier of B -defined the carrier of b -valued Function-like V17( the carrier of B) V21( the carrier of B, the carrier of b) Element of bool [: the carrier of B, the carrier of b:]

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

dom P is non empty Element of bool the carrier of B

dom g is non empty Element of bool the carrier of a

dom (g +* P) is set

rng (g +* P) is set

rng g is non empty Element of bool the carrier of b

bool the carrier of b is non empty set

rng P is non empty Element of bool the carrier of b

(rng g) \/ (rng P) is non empty Element of bool the carrier of b

c

s0 is Element of bool the carrier of b

c

g " s0 is Element of bool the carrier of a

P " s0 is Element of bool the carrier of B

dom c

(dom g) \/ (dom P) is non empty set

HH is set

(c

c

P . HH is set

P . HH is set

c

HH is set

c

g . HH is set

P . HH is set

HH is set

(c

c

g . HH is set

g . HH is set

c

s1 is Element of bool the carrier of a

AI is Element of bool the carrier of g

G9 is Element of bool the carrier of B

H is Element of bool the carrier of g

(c

((c

(g " s0) \/ (P " s0) is set

a is TopStruct

id a is Relation-like the carrier of a -defined the carrier of a -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]

the carrier of a is set

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

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

id the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued Function-like one-to-one V17( the carrier of a) V21( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]

bool the carrier of a is non empty set

b is Element of bool the carrier of a

(id a) .: b is Element of bool the carrier of a

bool the carrier of a is non empty set

b is Element of bool the carrier of a

(id a) " b is Element of bool the carrier of a

a is TopStruct

the carrier of a is set

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

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

id a is Relation-like the carrier of a -defined the carrier of a -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of a) continuous open Element of bool [: the carrier of a, the carrier of a:]

id the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued Function-like one-to-one V17( the carrier of a) V21( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

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

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

B is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]

B /" is non empty Relation-like the carrier of b -defined the carrier of a -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of a) Element of bool [: the carrier of b, the carrier of a:]

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

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

rng B is non empty Element of bool the carrier of b

bool the carrier of b is non empty set

[#] b is non empty non proper open closed dense non boundary Element of bool the carrier of b

g is Element of bool the carrier of b

(B /") .: g is Element of bool the carrier of a

bool the carrier of a is non empty set

B " g is Element of bool the carrier of a

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

b is Element of the carrier of a

I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]

K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

(I[01] --> b) . 0 is set

(I[01] --> b) . 1 is set

a is TopStruct

the carrier of a is set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

g is Element of the carrier of a

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

a is TopStruct

the carrier of a is set

b is Element of the carrier of a

B is Element of the carrier of a

[: the carrier of I[01], the carrier of a:] is Relation-like set

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

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

(I[01] --> b) . 0 is set

(I[01] --> b) . 1 is set

{0[01]} is non empty trivial V33() V34() V35() connected compact Element of bool the carrier of I[01]

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

I[01] | {0[01]} is non empty strict TopSpace-like V130() SubSpace of I[01]

the carrier of (I[01] | {0[01]}) is non empty V33() V34() V35() set

[: the carrier of I[01], the carrier of (I[01] | {0[01]}):] is non empty Relation-like set

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

b is V31() real ext-real Element of the carrier of (I[01] | {0[01]})

I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | {0[01]}) -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of (I[01] | {0[01]})) continuous Element of bool [: the carrier of I[01], the carrier of (I[01] | {0[01]}):]

K324( the carrier of (I[01] | {0[01]}), the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | {0[01]}) -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of (I[01] | {0[01]})) Element of bool [: the carrier of I[01], the carrier of (I[01] | {0[01]}):]

g is V31() real ext-real Element of the carrier of (I[01] | {0[01]})

g is V31() real ext-real Element of the carrier of (I[01] | {0[01]})

B is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | {0[01]}) -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of (I[01] | {0[01]})) Element of bool [: the carrier of I[01], the carrier of (I[01] | {0[01]}):]

B . 0 is set

B . 1 is set

a is () TopStruct

the carrier of a is set

[: the carrier of I[01], the carrier of a:] is Relation-like set

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

b is Element of the carrier of a

B is Element of the carrier of a

g is Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

g . 0 is set

g . 1 is set

g is Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

g . 0 is set

g . 1 is set

a is () TopStruct

the carrier of a is set

b is Element of the carrier of a

B is Element of the carrier of a

g is Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V21( the carrier of I[01], the carrier of a) (a,b,B)

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

B is Element of the carrier of a

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

g . 0 is set

g . 1 is set

dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]

rng g is non empty Element of bool the carrier of a

bool the carrier of a is non empty set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

b is Element of the carrier of a

B is Element of the carrier of a

g is Element of the carrier of a

g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

g . 0 is set

g . 1 is set

P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

P . 0 is set

P . 1 is set

rng g is non empty Element of bool the carrier of a

bool the carrier of a is non empty set

rng P is non empty Element of bool the carrier of a

(rng g) \/ (rng P) is non empty Element of bool the carrier of a

c

c

1 / 2 is V31() real ext-real Element of REAL

{ b

Closed-Interval-TSpace (0,(1 / 2)) is non empty strict TopSpace-like V130() SubSpace of R^1

Closed-Interval-TSpace ((1 / 2),1) is non empty strict TopSpace-like V130() SubSpace of R^1

P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V17( the carrier of (Closed-Interval-TSpace ((1 / 2),1))) V21( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):]

the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty V33() V34() V35() set

[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set

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

P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V17( the carrier of (Closed-Interval-TSpace (0,(1 / 2)))) V21( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):]

the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty V33() V34() V35() set

[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set

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

c

[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:] is non empty Relation-like set

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

c

[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty set

(c

dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

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

[.0,(1 / 2).] is V33() V34() V35() V141() Element of bool REAL

dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace ((1 / 2),1))

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

[.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL

HH is TopSpace-like V130() SubSpace of I[01]

the carrier of HH is V33() V34() V35() set

[: the carrier of HH, the carrier of a:] is Relation-like set

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

HH is TopSpace-like V130() SubSpace of I[01]

the carrier of HH is V33() V34() V35() set

[: the carrier of HH, the carrier of a:] is Relation-like set

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

{ b

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

(c

2 * f is V31() real ext-real Element of REAL

(2 * f) - 1 is V31() real ext-real Element of REAL

c

t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace ((1 / 2),1))

(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

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

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

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

1 - (1 / 2) is V31() real ext-real Element of REAL

(f - f) / (1 - (1 / 2)) is V31() real ext-real Element of REAL

((f - f) / (1 - (1 / 2))) * f is V31() real ext-real Element of REAL

1 * f is V31() real ext-real Element of REAL

(1 / 2) * f is V31() real ext-real Element of REAL

(1 * f) - ((1 / 2) * f) is V31() real ext-real Element of REAL

((1 * f) - ((1 / 2) * f)) / (1 - (1 / 2)) is V31() real ext-real Element of REAL

(((f - f) / (1 - (1 / 2))) * f) + (((1 * f) - ((1 / 2) * f)) / (1 - (1 / 2))) is V31() real ext-real Element of REAL

{ b

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

(c

2 * f is V31() real ext-real Element of REAL

c

t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

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

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

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

(1 / 2) - 0 is V31() real ext-real Element of REAL

(f - f) / ((1 / 2) - 0) is V31() real ext-real Element of REAL

((f - f) / ((1 / 2) - 0)) * f is V31() real ext-real Element of REAL

(1 / 2) * f is V31() real ext-real Element of REAL

0 * f is V31() real ext-real Element of REAL

((1 / 2) * f) - (0 * f) is V31() real ext-real Element of REAL

(((1 / 2) * f) - (0 * f)) / ((1 / 2) - 0) is V31() real ext-real Element of REAL

(((f - f) / ((1 / 2) - 0)) * f) + ((((1 / 2) * f) - (0 * f)) / ((1 / 2) - 0)) is V31() real ext-real Element of REAL

ff is Relation-like the carrier of HH -defined the carrier of a -valued Function-like V17( the carrier of HH) V21( the carrier of HH, the carrier of a) Element of bool [: the carrier of HH, the carrier of a:]

ff . (1 / 2) is set

2 * (1 / 2) is V31() real ext-real Element of REAL

(2 * (1 / 2)) - 1 is V31() real ext-real Element of REAL

c

gg is Relation-like the carrier of HH -defined the carrier of a -valued Function-like V17( the carrier of HH) V21( the carrier of HH, the carrier of a) Element of bool [: the carrier of HH, the carrier of a:]

H is V31() real ext-real Element of the carrier of I[01]

gg . H is set

[#] HH is non proper V33() V34() V35() open closed dense Element of bool the carrier of HH

bool the carrier of HH is non empty set

[#] HH is non proper V33() V34() V35() open closed dense Element of bool the carrier of HH

bool the carrier of HH is non empty set

([#] HH) \/ ([#] HH) is V33() V34() V35() set

[#] I[01] is non empty non proper V33() V34() V35() open closed dense non boundary Element of bool the carrier of I[01]

([#] HH) /\ ([#] HH) is V33() V34() V35() Element of bool the carrier of HH

{H} is non empty trivial V33() V34() V35() connected compact Element of bool the carrier of I[01]

dom c

rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,1))

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

dom c

rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,1))

dom (c

{ b

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

((c

(c

2 * 0 is V31() real ext-real Element of REAL

c

dom ((c

dom (c

(dom (c

[.0,(1 / 2).] \/ [.(1 / 2),1.] is V33() V34() V35() Element of bool REAL

rng ((c

rng (c

rng (c

(rng (c

f is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

f is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]

f . 1 is set

(c

2 * 1 is V31() real ext-real Element of REAL

(2 * 1) - 1 is V31() real ext-real Element of REAL

c

f is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)

t is V31() real ext-real Element of the carrier of I[01]

f . t is Element of the carrier of a

t9 is V31() real ext-real Element of REAL

2 * t9 is V31() real ext-real Element of REAL

c

(2 * t9) - 1 is V31() real ext-real Element of REAL

c

{ b

[.0,(1 / 2).] /\ [.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL

{(1 / 2)} is non empty trivial V33() V34() V35() set

(c

(c

(c

H is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)

H . 0 is set

H . 1 is set

H is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)

H . 0 is set

H . 1 is set

rng H is non empty Element of bool the carrier of a

rng c

rng c

(rng c

dom c

HH is set

dom c

dom H is non empty V33() V34() V35() Element of bool the carrier of I[01]

HH is set

H . HH is set

HH is V31() real ext-real Element of REAL

2 * HH is V31() real ext-real Element of REAL

2 * (1 / 2) is V31() real ext-real Element of REAL

c

2 * HH is V31() real ext-real Element of REAL

2 * 1 is V31() real ext-real Element of REAL

1 + 1 is V31() real ext-real Element of REAL

(2 * HH) - 1 is V31() real ext-real Element of REAL

2 * (1 / 2) is V31() real ext-real Element of REAL

0 + 1 is V31() real ext-real Element of REAL

c

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

B is Element of the carrier of a

g is Element of the carrier of a

1 / 2 is V31() real ext-real Element of REAL

g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,B)

P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,g)

{ b

Closed-Interval-TSpace (0,(1 / 2)) is non empty strict TopSpace-like V130() SubSpace of R^1

Closed-Interval-TSpace ((1 / 2),1) is non empty strict TopSpace-like V130() SubSpace of R^1

P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V17( the carrier of (Closed-Interval-TSpace ((1 / 2),1))) V21( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):]

the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty V33() V34() V35() set

[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set

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

P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V17( the carrier of (Closed-Interval-TSpace (0,(1 / 2)))) V21( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):]

the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty V33() V34() V35() set

[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set

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

g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:]

[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:] is non empty Relation-like set

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

P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:]

[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty set

(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is Relation-like Function-like set

dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

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

[.0,(1 / 2).] is V33() V34() V35() V141() Element of bool REAL

dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace ((1 / 2),1))

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

[.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL

{ b

a is V31() real ext-real Element of REAL

(P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . a is set

2 * a is V31() real ext-real Element of REAL

(2 * a) - 1 is V31() real ext-real Element of REAL

P . ((2 * a) - 1) is set

b is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace ((1 / 2),1))

(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . b is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

HH is V31() real ext-real Element of REAL

HH is V31() real ext-real Element of REAL

HH - HH is V31() real ext-real Element of REAL

1 - (1 / 2) is V31() real ext-real Element of REAL

(HH - HH) / (1 - (1 / 2)) is V31() real ext-real Element of REAL

((HH - HH) / (1 - (1 / 2))) * a is V31() real ext-real Element of REAL

1 * HH is V31() real ext-real Element of REAL

(1 / 2) * HH is V31() real ext-real Element of REAL

(1 * HH) - ((1 / 2) * HH) is V31() real ext-real Element of REAL

((1 * HH) - ((1 / 2) * HH)) / (1 - (1 / 2)) is V31() real ext-real Element of REAL

(((HH - HH) / (1 - (1 / 2))) * a) + (((1 * HH) - ((1 / 2) * HH)) / (1 - (1 / 2))) is V31() real ext-real Element of REAL

s0 is TopSpace-like V130() SubSpace of I[01]

the carrier of s0 is V33() V34() V35() set

[: the carrier of s0, the carrier of a:] is Relation-like set

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

c

the carrier of c

[: the carrier of c

bool [: the carrier of c

rng ((g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is set

rng (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is Element of bool the carrier of a

bool the carrier of a is non empty set

rng (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is Element of bool the carrier of a

(rng (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is Element of bool the carrier of a

{ b

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

(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . b is set

2 * b is V31() real ext-real Element of REAL

g . (2 * b) is set

t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

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

a is V31() real ext-real Element of REAL

b - a is V31() real ext-real Element of REAL

(1 / 2) - 0 is V31() real ext-real Element of REAL

(b - a) / ((1 / 2) - 0) is V31() real ext-real Element of REAL

((b - a) / ((1 / 2) - 0)) * b is V31() real ext-real Element of REAL

(1 / 2) * a is V31() real ext-real Element of REAL

0 * b is V31() real ext-real Element of REAL

((1 / 2) * a) - (0 * b) is V31() real ext-real Element of REAL

(((1 / 2) * a) - (0 * b)) / (1 / 2) is V31() real ext-real Element of REAL

(((b - a) / ((1 / 2) - 0)) * b) + ((((1 / 2) * a) - (0 * b)) / (1 / 2)) is V31() real ext-real Element of REAL

HH is Relation-like the carrier of c

HH . (1 / 2) is set

2 * (1 / 2) is V31() real ext-real Element of REAL

g . (2 * (1 / 2)) is set

(2 * (1 / 2)) - 1 is V31() real ext-real Element of REAL

P . ((2 * (1 / 2)) - 1) is set

HH is Relation-like the carrier of s0 -defined the carrier of a -valued Function-like V17( the carrier of s0) V21( the carrier of s0, the carrier of a) Element of bool [: the carrier of s0, the carrier of a:]

c

HH . c

dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]

rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,1))

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

dom P is non empty V33() V34() V35() Element of bool the carrier of I[01]

rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,1))

dom (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace ((1 / 2),1))

{ b

a is V31() real ext-real Element of REAL

((g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 is set

(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 is set

2 * 0 is V31() real ext-real Element of REAL

g . (2 * 0) is set

dom ((g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is set

dom (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

(dom (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is V33() V34() V35() set

[.0,(1 / 2).] \/ [.(1 / 2),1.] is V33() V34() V35() Element of bool REAL

[#] c

bool the carrier of c

[#] s0 is non proper V33() V34() V35() open closed dense Element of bool the carrier of s0

bool the carrier of s0 is non empty set

([#] c

[#] I[01] is non empty non proper V33() V34() V35() open closed dense non boundary Element of bool the carrier of I[01]

([#] c

{c

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

a is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]

b . 1 is set

(P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 is set

2 * 1 is V31() real ext-real Element of REAL

(2 * 1) - 1 is V31() real ext-real Element of REAL

P . ((2 * 1) - 1) is set

b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)

t is V31() real ext-real Element of the carrier of I[01]

b . t is Element of the carrier of a

2 * t is V31() real ext-real Element of REAL

g . (2 * t) is set

(2 * t) - 1 is V31() real ext-real Element of REAL

P . ((2 * t) - 1) is set

{ b

[.0,(1 / 2).] /\ [.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL

{(1 / 2)} is non empty trivial V33() V34() V35() set

(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t is set

(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t is set

(P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t is set

c

c

dom c

s0 is set

c

c

{ b

G9 is V31() real ext-real Element of REAL

s1 is V31() real ext-real Element of the carrier of I[01]

c

2 * G9 is V31() real ext-real Element of REAL

g . (2 * G9) is set

c

s1 is V31() real ext-real Element of the carrier of I[01]

c

2 * G9 is V31() real ext-real Element of REAL

(2 * G9) - 1 is V31() real ext-real Element of REAL

P . ((2 * G9) - 1) is set

c

dom c

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

(I[01] --> b) . 0 is set

(I[01] --> b) . 1 is set

g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]

g is set

P is set

g . g is set

g . P is set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

dom B is non empty V33() V34() V35() Element of bool the carrier of I[01]

{ b

g is set

B . g is set

(I[01] --> b) . g is set

B . 0 is set

dom (I[01] --> b) is non empty V33() V34() V35() Element of bool the carrier of I[01]

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

(a,b,b,b,B,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

dom B is non empty V33() V34() V35() Element of bool the carrier of I[01]

g is set

B . g is set

(a,b,b,b,B,B) . g is set

{ b

P is V31() real ext-real Element of REAL

(1 / 2) * 2 is V31() real ext-real Element of REAL

P * 2 is V31() real ext-real Element of REAL

2 * P is V31() real ext-real Element of REAL

B . (2 * P) is set

g is V31() real ext-real Element of the carrier of I[01]

B . g is Element of the carrier of a

(1 / 2) * 2 is V31() real ext-real Element of REAL

P * 2 is V31() real ext-real Element of REAL

1 + 0 is V31() real ext-real Element of REAL

2 * P is V31() real ext-real Element of REAL

(2 * P) - 1 is V31() real ext-real Element of REAL

1 * 2 is V31() real ext-real Element of REAL

2 - 1 is V31() real ext-real Element of REAL

B . ((2 * P) - 1) is set

g is V31() real ext-real Element of the carrier of I[01]

B . g is Element of the carrier of a

dom (a,b,b,b,B,B) is non empty V33() V34() V35() Element of bool the carrier of I[01]

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

(a,b,b,b,B,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

B is Element of the carrier of a

g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,B)

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

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

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

[: the carrier of I[01], the carrier of a:] is non empty Relation-like set

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

g * (L[01] (((0,1) (#)),((#) (0,1)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of a:]

[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of a:] is non empty Relation-like set

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

P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]

c

P . c

1 - c

g . (1 - c

dom (L[01] (((0,1) (#)),((#) (0,1)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,1))

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

c

(L[01] (((0,1) (#)),((#) (0,1)))) . c

g . ((L[01] (((0,1) (#)),((#) (0,1)))) . c

0 - 1 is V31() real ext-real Element of REAL

(0 - 1) * c

((0 - 1) * c

g . (((0 - 1) * c

1 * c

1 - (1 * c

g . (1 - (1 * c

{ b

dom (L[01] (((0,1) (#)),((#) (0,1)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,1))

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

(L[01] (((0,1) (#)),((#) (0,1)))) . 0 is set

(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

P . 0 is set

g . 1 is set

(L[01] (((0,1) (#)),((#) (0,1)))) . 1 is set

(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

P . 1 is set

g . 0 is set

c

c

c

1 - c

g . (1 - c

g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,b)

P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,b)

c

g . c

P . c

c

g . c

1 - c

g . (1 - c

P . c

dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]

dom P is non empty V33() V34() V35() Element of bool the carrier of I[01]

a is V31() real ext-real Element of REAL

1 - a is V31() real ext-real Element of REAL

1 - 1 is V31() real ext-real Element of REAL

1 - 0 is V31() real ext-real Element of REAL

a is V31() real ext-real Element of REAL

1 - a is V31() real ext-real Element of REAL

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

(a,b,b,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

dom B is non empty V33() V34() V35() Element of bool the carrier of I[01]

g is set

B . g is set

(a,b,b,B) . g is set

g is V31() real ext-real Element of REAL

1 - g is V31() real ext-real Element of REAL

P is V31() real ext-real Element of the carrier of I[01]

B . P is Element of the carrier of a

dom (a,b,b,B) is non empty V33() V34() V35() Element of bool the carrier of I[01]

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is Element of the carrier of a

B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

(a,b,b,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

bool the carrier of b is non empty set

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

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

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

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

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

union B is Element of bool the carrier of b

g is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]

g " (union B) is Element of bool the carrier of a

bool the carrier of a is non empty set

g " B is Element of bool (bool the carrier of a)

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

union (g " B) is Element of bool the carrier of a

P is set

g . P is set

g is Element of bool the carrier of b

c

g " c

c

g is set

P is set

dom g is non empty Element of bool the carrier of a

c

c

g " c

g . g is set

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

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

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

B is non empty TopSpace-like TopStruct

the carrier of B is non empty set

g is non empty TopSpace-like TopStruct

the carrier of g is non empty set

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

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

g is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]

P is non empty Relation-like the carrier of B -defined the carrier of g -valued Function-like V17( the carrier of B) V21( the carrier of B, the carrier of g) Element of bool [: the carrier of B, the carrier of g:]

[:g,P:] is Relation-like Function-like set

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

the carrier of [:a,B:] is non empty set

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

the carrier of [:b,g:] is non empty set

[: the carrier of [:a,B:], the carrier of [:b,g:]:] is non empty Relation-like set

bool [: the carrier of [:a,B:], the carrier of [:b,g:]:] is non empty set

[:g,P:] is non empty Relation-like [: the carrier of a, the carrier of B:] -defined [: the carrier of b, the carrier of g:] -valued Function-like V17([: the carrier of a, the carrier of B:]) V21([: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]) Element of bool [:[: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]:]

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

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

[:[: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]:] is non empty Relation-like set

bool [:[: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]:] is non empty set

rng [:g,P:] is non empty Relation-like the carrier of b -defined the carrier of g -valued Element of bool [: the carrier of b, the carrier of g:]

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

dom [:g,P:] is non empty Relation-like the carrier of a -defined the carrier of B -valued Element of bool [: the carrier of a, the carrier of B:]

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

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

B is non empty TopSpace-like TopStruct

the carrier of B is non empty set

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

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

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

g is non empty TopSpace-like TopStruct

the carrier of g is non empty set

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

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

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

the carrier of [:B,g:] is non empty set

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

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

the carrier of [:a,b:] is non empty set

g is non empty Relation-like the carrier of a -defined the carrier of B -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of B) continuous Element of bool [: the carrier of a, the carrier of B:]

P is non empty Relation-like the carrier of b -defined the carrier of g -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of g) continuous Element of bool [: the carrier of b, the carrier of g:]

(a,B,b,g,g,P) is non empty Relation-like the carrier of [:a,b:] -defined the carrier of [:B,g:] -valued Function-like V17( the carrier of [:a,b:]) V21( the carrier of [:a,b:], the carrier of [:B,g:]) Element of bool [: the carrier of [:a,b:], the carrier of [:B,g:]:]

[: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty Relation-like set

bool [: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty set

c

c

Base-Appr c

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

bool the carrier of B is non empty set

bool the carrier of g is non empty set

{ [:b

(a,B,b,g,g,P) " c

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

s0 is Element of bool the carrier of B

s1 is Element of bool the carrier of g

[:s0,s1:] is Relation-like Element of bool the carrier of [:B,g:]

[#] B is non empty non proper open closed dense non boundary Element of bool the carrier of B

g " s0 is Element of bool the carrier of a

bool the carrier of a is non empty set

[#] g is non empty non proper open closed dense non boundary Element of bool the carrier of g

P " s1 is Element of bool the carrier of b

bool the carrier of b is non empty set

[:(g " s0),(P " s1):] is Relation-like Element of bool the carrier of [:a,b:]

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

B is non empty TopSpace-like TopStruct

the carrier of B is non empty set

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

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

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

g is non empty TopSpace-like TopStruct

the carrier of g is non empty set

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

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

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

the carrier of [:B,g:] is non empty set

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

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

the carrier of [:a,b:] is non empty set

g is non empty Relation-like the carrier of a -defined the carrier of B -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of B) continuous Element of bool [: the carrier of a, the carrier of B:]

P is non empty Relation-like the carrier of b -defined the carrier of g -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of g) continuous Element of bool [: the carrier of b, the carrier of g:]

(a,B,b,g,g,P) is non empty Relation-like the carrier of [:a,b:] -defined the carrier of [:B,g:] -valued Function-like V17( the carrier of [:a,b:]) V21( the carrier of [:a,b:], the carrier of [:B,g:]) Element of bool [: the carrier of [:a,b:], the carrier of [:B,g:]:]

[: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty Relation-like set

bool [: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty set

c

(a,B,b,g,g,P) " c

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

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

Base-Appr c

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

bool the carrier of B is non empty set

bool the carrier of g is non empty set

{ [:b

(a,B,b,g,g,P) " (Base-Appr c

c

s0 is Element of bool the carrier of [:a,b:]

s1 is Element of bool the carrier of [:B,g:]

(a,B,b,g,g,P) " s1 is Element of bool the carrier of [:a,b:]

union (Base-Appr c

union ((a,B,b,g,g,P) " (Base-Appr c

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

B is non empty TopSpace-like TopStruct

the carrier of B is non empty set

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

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

b is non empty TopSpace-like TopStruct

the carrier of b is non empty set

g is non empty TopSpace-like TopStruct

the carrier of g is non empty set

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

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

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

the carrier of [:a,b:] is non empty set

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

the carrier of [:B,g:] is non empty set

[: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty Relation-like set

bool [: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty set

g is non empty Relation-like the carrier of a -defined the carrier of B -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of B) continuous Element of bool [: the carrier of a, the carrier of B:]

P is non empty Relation-like the carrier of b -defined the carrier of g -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of g) continuous Element of bool [: the carrier of b, the carrier of g:]

(a,B,b,g,g,P) is non empty Relation-like the carrier of [:a,b:] -defined the carrier of [:B,g:] -valued Function-like V17( the carrier of [:a,b:]) V21( the carrier of [:a,b:], the carrier of [:B,g:]) Element of bool [: the carrier of [:a,b:], the carrier of [:B,g:]:]

[#] [:B,g:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:B,g:]

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

c

(a,B,b,g,g,P) " c

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

c

a is TopSpace-like T_0 TopStruct

b is TopSpace-like T_0 TopStruct

[:a,b:] is strict TopSpace-like TopStruct

the carrier of [:a,b:] is set

g is Element of the carrier of [:a,b:]

g is Element of the carrier of [:a,b:]

the carrier of a is set

the carrier of b is set

[: the carrier of a, the carrier of b:] is Relation-like set

P is set

c

[P,c

{P,c

{P} is non empty trivial set

{{P,c

c

s0 is set

[c

{c

{c

{{c

AI is Element of the carrier of a

H is Element of the carrier of a

bool the carrier of a is non empty set

HH is Element of bool the carrier of a

[#] b is non proper open closed dense Element of bool the carrier of b

bool the carrier of b is non empty set

[:HH,([#] b):] is Relation-like Element of bool the carrier of [:a,b:]

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

AI is Element of the carrier of a

H is Element of the carrier of a

bool the carrier of b is non empty set

s1 is Element of the carrier of b

G9 is Element of the carrier of b

HH is Element of bool the carrier of b

[#] a is non proper open closed dense Element of bool the carrier of a

bool the carrier of a is non empty set

[:([#] a),HH:] is Relation-like Element of bool the carrier of [:a,b:]

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

AI is Element of the carrier of a

H is Element of the carrier of a

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

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

a is TopSpace-like T_0 T_1 TopStruct

b is TopSpace-like T_0 T_1 TopStruct