:: RCOMP_3 semantic presentation

REAL is non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval set

NAT is ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below Element of K32(REAL)

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

K597() is TopSpace-like T_0 T_1 T_2 compact real-membered V241() SubSpace of R^1

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 real-membered TopStruct

the carrier of K597() is complex-membered ext-real-membered real-membered set

K575(K597(),K597()) is strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of K575(K597(),K597()) is set

omega is ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below set

K32(omega) is non empty non trivial non finite set

K33(NAT,REAL) is Relation-like non trivial non finite V124() V125() V126() set

K32(K33(NAT,REAL)) is non empty non trivial non finite set

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

COMPLEX is non empty non trivial non finite complex-membered V123() set

RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V123() set

INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V123() set

K33(COMPLEX,COMPLEX) is Relation-like non empty non trivial non finite V124() set

K32(K33(COMPLEX,COMPLEX)) is non empty non trivial non finite set

K33(K33(COMPLEX,COMPLEX),COMPLEX) is Relation-like non empty non trivial non finite V124() set

K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is non empty non trivial non finite set

K33(REAL,REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set

K32(K33(REAL,REAL)) is non empty non trivial non finite set

K33(K33(REAL,REAL),REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set

K32(K33(K33(REAL,REAL),REAL)) is non empty non trivial non finite set

K33(RAT,RAT) is Relation-like RAT -valued non empty non trivial non finite V124() V125() V126() set

K32(K33(RAT,RAT)) is non empty non trivial non finite set

K33(K33(RAT,RAT),RAT) is Relation-like RAT -valued non empty non trivial non finite V124() V125() V126() set

K32(K33(K33(RAT,RAT),RAT)) is non empty non trivial non finite set

K33(INT,INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V124() V125() V126() set

K32(K33(INT,INT)) is non empty non trivial non finite set

K33(K33(INT,INT),INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V124() V125() V126() set

K32(K33(K33(INT,INT),INT)) is non empty non trivial non finite set

K33(NAT,NAT) is Relation-like RAT -valued INT -valued V124() V125() V126() V127() set

K33(K33(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V124() V125() V126() V127() set

K32(K33(K33(NAT,NAT),NAT)) is non empty set

K32(NAT) is non empty non trivial non finite set

K276() is set

1 is ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

ExtREAL is non empty ext-real-membered interval set

K33(1,1) is Relation-like RAT -valued INT -valued non empty finite V124() V125() V126() V127() set

K32(K33(1,1)) is non empty finite V43() set

K33(K33(1,1),1) is Relation-like RAT -valued INT -valued non empty finite V124() V125() V126() V127() set

K32(K33(K33(1,1),1)) is non empty finite V43() set

K33(K33(1,1),REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set

K32(K33(K33(1,1),REAL)) is non empty non trivial non finite set

2 is ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

K33(2,2) is Relation-like RAT -valued INT -valued non empty finite V124() V125() V126() V127() set

K33(K33(2,2),REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set

K32(K33(K33(2,2),REAL)) is non empty non trivial non finite set

K519(2) is V216() L15()

the carrier of K519(2) is set

K590() is T_0 T_1 T_2 compact real-membered V241() TopStruct

the carrier of K590() is complex-membered ext-real-membered real-membered set

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning real-membered MetrStruct

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() SubSpace of R^1

the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set

K32( the carrier of R^1) is non empty set

K32(K32( the carrier of R^1)) is non empty set

K608(2) is non empty compact V240() V241() SubSpace of K519(2)

the carrier of K608(2) is non empty set

K33( the carrier of R^1, the carrier of K608(2)) is Relation-like non empty set

K32(K33( the carrier of R^1, the carrier of K608(2))) is non empty set

K612() is Relation-like Function-like V27( the carrier of R^1, the carrier of K608(2)) V27( the carrier of R^1, the carrier of K608(2)) V28( the carrier of K608(2)) continuous Element of K32(K33( the carrier of R^1, the carrier of K608(2)))

K609() is Element of the carrier of K608(2)

K611(K609()) is non empty strict SubSpace of K608(2)

the carrier of K611(K609()) is non empty set

0 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() V67() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of NAT

{} is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set

the Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set

].0,1.[ is non empty complex-membered ext-real-membered real-membered open non left_end non right_end interval Element of K32(REAL)

R^1 ].0,1.[ is non empty open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

R^1 | (R^1 ].0,1.[) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (R^1 | (R^1 ].0,1.[)) is non empty complex-membered ext-real-membered real-membered set

K33( the carrier of K611(K609()), the carrier of (R^1 | (R^1 ].0,1.[))) is Relation-like non empty V124() V125() V126() set

K32(K33( the carrier of K611(K609()), the carrier of (R^1 | (R^1 ].0,1.[)))) is non empty set

K610() is Element of the carrier of K608(2)

K611(K610()) is non empty strict SubSpace of K608(2)

the carrier of K611(K610()) is non empty set

1 / 2 is ext-real non negative real V65() Element of REAL

3 is ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

3 / 2 is ext-real non negative real V65() Element of REAL

].(1 / 2),(3 / 2).[ is non empty complex-membered ext-real-membered real-membered open non left_end non right_end interval Element of K32(REAL)

R^1 ].(1 / 2),(3 / 2).[ is non empty open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

R^1 | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)) is non empty complex-membered ext-real-membered real-membered set

K33( the carrier of K611(K610()), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[))) is Relation-like non empty V124() V125() V126() set

K32(K33( the carrier of K611(K610()), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)))) is non empty set

{{},1} is non empty finite V43() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

K33( the carrier of K597(), the carrier of K597()) is Relation-like V124() V125() V126() set

K32(K33( the carrier of K597(), the carrier of K597())) is non empty set

K32( the carrier of K575(K597(),K597())) is non empty set

K33(COMPLEX,REAL) is Relation-like non empty non trivial non finite V124() V125() V126() set

K32(K33(COMPLEX,REAL)) is non empty non trivial non finite set

the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set

dom {} is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set

rng {} is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval set

union {} is finite set

K32( the carrier of R^1) is non empty set

Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(NAT)

{1} is non empty trivial finite V43() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of K32(NAT)

{1,2} is non empty finite V43() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

+infty is non empty ext-real positive non negative non real set

-infty is non empty ext-real non positive negative non real set

r is non empty set

[#] r is non empty non proper Element of K32(r)

K32(r) is non empty set

r is Reflexive discerning symmetric triangle SubSpace of RealSpace

the carrier of r is set

the carrier of RealSpace is non empty complex-membered ext-real-membered real-membered set

K32( the carrier of RealSpace) is non empty set

r is non empty complex-membered ext-real-membered real-membered bounded_below set

lower_bound r is ext-real real V65() set

inf r is ext-real real V65() set

s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

n is non empty complex-membered ext-real-membered real-membered bounded_below Element of K32(REAL)

lower_bound n is ext-real real V65() Element of REAL

inf n is ext-real real V65() set

Cl n is non empty complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)

lower_bound (Cl n) is ext-real real V65() Element of REAL

inf (Cl n) is ext-real real V65() set

r is non empty complex-membered ext-real-membered real-membered bounded_above set

upper_bound r is ext-real real V65() set

sup r is ext-real real V65() set

s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

n is non empty complex-membered ext-real-membered real-membered bounded_above Element of K32(REAL)

upper_bound n is ext-real real V65() Element of REAL

sup n is ext-real real V65() set

Cl n is non empty complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)

upper_bound (Cl n) is ext-real real V65() Element of REAL

sup (Cl n) is ext-real real V65() set

r is complex-membered ext-real-membered real-membered Element of K32(REAL)

s is complex-membered ext-real-membered real-membered Element of K32(REAL)

r \/ s is complex-membered ext-real-membered real-membered Element of K32(REAL)

Cl (r \/ s) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

Cl r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

Cl s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

(Cl r) \/ (Cl s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

F is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

n \/ F is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl (n \/ F) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl F is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl n) \/ (Cl F) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl r) \/ (Cl F) is complex-membered ext-real-membered real-membered set

r is ext-real real V65() set

s is ext-real set

[.r,s.[ is complex-membered ext-real-membered real-membered non right_end interval Element of K32(REAL)

n is ext-real set

].s,r.] is complex-membered ext-real-membered real-membered non left_end interval Element of K32(REAL)

n is ext-real set

r is ext-real real V65() set

s is ext-real real V65() set

[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval Element of K32(REAL)

n is ext-real set

].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval Element of K32(REAL)

n is ext-real set

].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end interval Element of K32(REAL)

n is ext-real set

n is ext-real set

r is ext-real real V65() set

s is ext-real real V65() set

[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound [.r,s.[ is ext-real real V65() Element of REAL

F is ext-real real V65() set

r + s is ext-real real V65() set

(r + s) / 2 is ext-real real V65() Element of REAL

F is ext-real real V65() set

r + F is ext-real real V65() set

r + (r + F) is ext-real real V65() set

(r + (r + F)) / 2 is ext-real real V65() Element of REAL

r is ext-real real V65() set

s is ext-real real V65() set

[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

upper_bound [.r,s.[ is ext-real real V65() Element of REAL

F is ext-real real V65() set

r + s is ext-real real V65() set

(r + s) / 2 is ext-real real V65() Element of REAL

F is ext-real real V65() set

s - F is ext-real real V65() set

s - 0 is ext-real real V65() Element of REAL

s + (s - F) is ext-real real V65() set

(s + (s - F)) / 2 is ext-real real V65() Element of REAL

r is ext-real real V65() set

s is ext-real real V65() set

].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound ].r,s.] is ext-real real V65() Element of REAL

F is ext-real real V65() set

r + s is ext-real real V65() set

(r + s) / 2 is ext-real real V65() Element of REAL

F is ext-real real V65() set

r + F is ext-real real V65() set

r + (r + F) is ext-real real V65() set

(r + (r + F)) / 2 is ext-real real V65() Element of REAL

r is ext-real real V65() set

s is ext-real real V65() set

].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

upper_bound ].r,s.] is ext-real real V65() Element of REAL

F is ext-real real V65() set

r + s is ext-real real V65() set

(r + s) / 2 is ext-real real V65() Element of REAL

F is ext-real real V65() set

s - F is ext-real real V65() set

s - 0 is ext-real real V65() Element of REAL

s + (s - F) is ext-real real V65() set

(s + (s - F)) / 2 is ext-real real V65() Element of REAL

r is ext-real real V65() set

left_closed_halfline r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

s is ext-real real V65() set

[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

right_closed_halfline s is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

C is set

G is ext-real real V65() Element of REAL

C is set

r is ext-real real V65() set

left_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)

].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

s is ext-real real V65() set

n is ext-real real V65() set

r - 0 is ext-real real V65() Element of REAL

r - 1 is ext-real real V65() Element of REAL

(r - 1) - 0 is ext-real real V65() Element of REAL

s - 1 is ext-real real V65() Element of REAL

s - 0 is ext-real real V65() Element of REAL

r is ext-real real V65() set

right_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)

].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

s is ext-real real V65() set

r + 1 is ext-real real V65() Element of REAL

r + 0 is ext-real real V65() Element of REAL

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

s + 1 is ext-real real V65() Element of REAL

s + 0 is ext-real real V65() Element of REAL

r is ext-real real V65() set

left_closed_halfline r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

left_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)

].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real set

F is ext-real set

[.n,F.] is ext-real-membered interval set

L is set

C is ext-real real V65() Element of REAL

G is ext-real real V65() Element of REAL

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

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

left_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)

].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real set

n is ext-real set

F is ext-real set

[.n,F.] is ext-real-membered interval set

L is set

C is ext-real real V65() Element of REAL

G is ext-real real V65() Element of REAL

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

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

right_closed_halfline r is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

[.r,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

right_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)

].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real set

F is ext-real set

[.n,F.] is ext-real-membered interval set

L is set

C is ext-real real V65() Element of REAL

G is ext-real real V65() Element of REAL

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

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

right_open_halfline r is complex-membered ext-real-membered real-membered open Element of K32(REAL)

].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real set

n is ext-real set

F is ext-real set

[.n,F.] is ext-real-membered interval set

L is set

C is ext-real real V65() Element of REAL

G is ext-real real V65() Element of REAL

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

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

r is ext-real real V65() set

left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

upper_bound (left_closed_halfline r) is ext-real real V65() Element of REAL

n is ext-real real V65() set

r - n is ext-real real V65() set

r - 0 is ext-real real V65() Element of REAL

n is ext-real real V65() set

r is ext-real real V65() set

left_open_halfline r is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

upper_bound (left_open_halfline r) is ext-real real V65() Element of REAL

n is ext-real real V65() set

r - n is ext-real real V65() set

r - 0 is ext-real real V65() Element of REAL

(r - n) + r is ext-real real V65() set

((r - n) + r) / 2 is ext-real real V65() Element of REAL

n is ext-real real V65() set

r is ext-real real V65() set

right_closed_halfline r is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.r,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

lower_bound (right_closed_halfline r) is ext-real real V65() Element of REAL

n is ext-real real V65() set

r + n is ext-real real V65() set

r + 0 is ext-real real V65() Element of REAL

n is ext-real real V65() set

r is ext-real real V65() set

right_open_halfline r is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].r,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

lower_bound (right_open_halfline r) is ext-real real V65() Element of REAL

n is ext-real real V65() set

r + n is ext-real real V65() set

r + 0 is ext-real real V65() Element of REAL

r + r is ext-real real V65() set

(r + r) + n is ext-real real V65() set

((r + r) + n) / 2 is ext-real real V65() Element of REAL

r + (r + n) is ext-real real V65() set

(r + (r + n)) / 2 is ext-real real V65() Element of REAL

n is ext-real real V65() set

[#] REAL is non empty non proper complex-membered ext-real-membered real-membered closed open Element of K32(REAL)

r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

upper_bound r is ext-real real V65() Element of REAL

[.(lower_bound r),(upper_bound r).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound s is ext-real real V65() Element of REAL

inf s is ext-real real V65() set

upper_bound s is ext-real real V65() Element of REAL

sup s is ext-real real V65() set

[.(lower_bound s),(upper_bound s).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

upper_bound r is ext-real real V65() Element of REAL

].(lower_bound r),(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is set

n is ext-real real V65() Element of REAL

r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

upper_bound r is ext-real real V65() Element of REAL

].(lower_bound r),(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is set

n is ext-real real V65() Element of REAL

n - (lower_bound r) is ext-real real V65() Element of REAL

(lower_bound r) - (lower_bound r) is ext-real real V65() Element of REAL

(lower_bound r) + (n - (lower_bound r)) is ext-real real V65() Element of REAL

F is ext-real real V65() set

[.F,(upper_bound r).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of K32(REAL)

upper_bound r is ext-real real V65() Element of REAL

lower_bound r is ext-real real V65() Element of REAL

[.(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is set

n is ext-real real V65() Element of REAL

r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

upper_bound r is ext-real real V65() Element of REAL

[.(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is set

n is ext-real real V65() Element of REAL

(upper_bound r) - n is ext-real real V65() Element of REAL

n - n is ext-real real V65() Element of REAL

(upper_bound r) - ((upper_bound r) - n) is ext-real real V65() Element of REAL

F is ext-real real V65() set

[.(lower_bound r),F.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

upper_bound r is ext-real real V65() Element of REAL

].(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is set

n is ext-real real V65() Element of REAL

r is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

inf r is ext-real real V65() set

upper_bound r is ext-real real V65() Element of REAL

sup r is ext-real real V65() set

].(lower_bound r),(upper_bound r).[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is set

n is ext-real real V65() Element of REAL

n - (lower_bound r) is ext-real real V65() Element of REAL

(lower_bound r) - (lower_bound r) is ext-real real V65() Element of REAL

(lower_bound r) + (n - (lower_bound r)) is ext-real real V65() Element of REAL

F is ext-real real V65() set

(upper_bound r) - n is ext-real real V65() Element of REAL

n - n is ext-real real V65() Element of REAL

(upper_bound r) - ((upper_bound r) - n) is ext-real real V65() Element of REAL

C is ext-real real V65() set

[.F,C.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered Element of K32(REAL)

upper_bound r is ext-real real V65() Element of REAL

left_closed_halfline (upper_bound r) is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

s is set

n is ext-real real V65() Element of REAL

r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

upper_bound r is ext-real real V65() Element of REAL

left_closed_halfline (upper_bound r) is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,(upper_bound r).] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

s is set

n is ext-real real V65() Element of REAL

F is ext-real set

C is ext-real real V65() set

[.C,(upper_bound r).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered Element of K32(REAL)

upper_bound r is ext-real real V65() Element of REAL

left_open_halfline (upper_bound r) is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,(upper_bound r).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

s is set

n is ext-real real V65() Element of REAL

r is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)

upper_bound r is ext-real real V65() Element of REAL

left_open_halfline (upper_bound r) is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,(upper_bound r).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

s is set

n is ext-real real V65() Element of REAL

F is ext-real set

(upper_bound r) - n is ext-real real V65() Element of REAL

n - n is ext-real real V65() Element of REAL

(upper_bound r) - ((upper_bound r) - n) is ext-real real V65() Element of REAL

G is ext-real real V65() set

C is ext-real real V65() set

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

right_closed_halfline (lower_bound r) is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

s is set

n is ext-real real V65() Element of REAL

r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

right_closed_halfline (lower_bound r) is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

s is set

n is ext-real real V65() Element of REAL

F is ext-real set

C is ext-real real V65() set

[.(lower_bound r),C.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

right_open_halfline (lower_bound r) is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

s is set

n is ext-real real V65() Element of REAL

r is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

right_open_halfline (lower_bound r) is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].(lower_bound r),+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

s is set

n is ext-real real V65() Element of REAL

F is ext-real set

n - (lower_bound r) is ext-real real V65() Element of REAL

(lower_bound r) - (lower_bound r) is ext-real real V65() Element of REAL

(lower_bound r) + (n - (lower_bound r)) is ext-real real V65() Element of REAL

C is ext-real real V65() set

G is ext-real real V65() set

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

s is set

n is ext-real real V65() Element of REAL

F is ext-real set

G is ext-real set

L is ext-real real V65() set

C is ext-real real V65() set

[.L,C.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)

n is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is set

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

C is ext-real real V65() Element of REAL

[.C,C.] is non empty complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

n is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

upper_bound n is ext-real real V65() Element of REAL

sup n is ext-real real V65() set

lower_bound n is ext-real real V65() Element of REAL

inf n is ext-real real V65() set

F is set

C is set

[.(lower_bound n),(upper_bound n).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

].(lower_bound n),(upper_bound n).] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

[.(lower_bound n),(upper_bound n).[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

].(lower_bound n),(upper_bound n).[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

n is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)

upper_bound s is ext-real real V65() Element of REAL

left_closed_halfline (upper_bound s) is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,(upper_bound s).] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

upper_bound s is ext-real real V65() Element of REAL

left_open_halfline (upper_bound s) is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,(upper_bound s).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

upper_bound s is ext-real real V65() Element of REAL

lower_bound s is ext-real real V65() Element of REAL

right_closed_halfline (lower_bound s) is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.(lower_bound s),+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

lower_bound s is ext-real real V65() Element of REAL

right_open_halfline (lower_bound s) is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].(lower_bound s),+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

lower_bound s is ext-real real V65() Element of REAL

s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)

r is ext-real real V65() set

s is non empty complex-membered ext-real-membered real-membered interval Element of K32(REAL)

lower_bound s is ext-real real V65() Element of REAL

upper_bound s is ext-real real V65() Element of REAL

n is ext-real real V65() set

left_closed_halfline n is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,n.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

n is ext-real real V65() set

left_closed_halfline n is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,n.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

n is ext-real real V65() set

left_open_halfline n is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,n.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real real V65() set

left_open_halfline n is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,n.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real real V65() set

right_closed_halfline n is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.n,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

n is ext-real real V65() set

right_closed_halfline n is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.n,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

n is ext-real real V65() set

right_open_halfline n is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].n,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real real V65() set

right_open_halfline n is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].n,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

n is ext-real real V65() set

F is ext-real real V65() set

[.n,F.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

n is ext-real real V65() set

F is ext-real real V65() set

[.n,F.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is ext-real real V65() set

n is ext-real real V65() set

[.n,F.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is ext-real real V65() set

n is ext-real real V65() set

[.n,F.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is ext-real real V65() set

n is ext-real real V65() set

].n,F.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is ext-real real V65() set

n is ext-real real V65() set

].n,F.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is ext-real real V65() set

n is ext-real real V65() set

].n,F.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is ext-real real V65() set

n is ext-real real V65() set

].n,F.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound r is ext-real real V65() Element of REAL

inf r is ext-real real V65() set

s is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval Element of K32(REAL)

lower_bound s is ext-real real V65() Element of REAL

inf s is ext-real real V65() set

upper_bound s is ext-real real V65() Element of REAL

sup s is ext-real real V65() set

upper_bound r is ext-real real V65() Element of REAL

sup r is ext-real real V65() set

n is set

[.(lower_bound s),(upper_bound s).] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

F is ext-real real V65() Element of REAL

C is ext-real real V65() set

left_closed_halfline C is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,C.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

G is ext-real real V65() set

left_open_halfline G is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,G.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

L is ext-real real V65() set

right_closed_halfline L is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.L,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

k is ext-real real V65() set

right_open_halfline k is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].k,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

C is ext-real real V65() set

G is ext-real real V65() set

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

C is ext-real real V65() set

G is ext-real real V65() set

[.C,G.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

G is ext-real real V65() set

C is ext-real real V65() set

[.C,G.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

G is ext-real real V65() set

C is ext-real real V65() set

[.C,G.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

L is ext-real real V65() set

left_closed_halfline L is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,L.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

k is ext-real real V65() set

left_open_halfline k is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,k.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

z is ext-real real V65() set

right_closed_halfline z is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.z,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

x is ext-real real V65() set

right_open_halfline x is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].x,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

L is ext-real real V65() set

k is ext-real real V65() set

[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

L is ext-real real V65() set

k is ext-real real V65() set

[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

G is ext-real real V65() set

C is ext-real real V65() set

].C,G.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

G is ext-real real V65() set

C is ext-real real V65() set

].C,G.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

L is ext-real real V65() set

left_closed_halfline L is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,L.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

k is ext-real real V65() set

left_open_halfline k is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,k.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

z is ext-real real V65() set

right_closed_halfline z is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.z,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

x is ext-real real V65() set

right_open_halfline x is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].x,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

L is ext-real real V65() set

k is ext-real real V65() set

[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

L is ext-real real V65() set

k is ext-real real V65() set

[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

G is ext-real real V65() set

C is ext-real real V65() set

].C,G.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

G is ext-real real V65() set

C is ext-real real V65() set

].C,G.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

L is ext-real real V65() set

left_closed_halfline L is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,L.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

k is ext-real real V65() set

left_open_halfline k is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,k.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

z is ext-real real V65() set

right_closed_halfline z is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.z,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

x is ext-real real V65() set

right_open_halfline x is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].x,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

L is ext-real real V65() set

k is ext-real real V65() set

[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

L is ext-real real V65() set

k is ext-real real V65() set

[.L,k.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

[.L,k.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

k is ext-real real V65() set

L is ext-real real V65() set

].L,k.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

r is ext-real real V65() set

s is ext-real real V65() set

[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl [.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded Element of K32(REAL)

left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

left_open_halfline r is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

R^1 (left_open_halfline r) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

R^1 (right_closed_halfline s) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

right_open_halfline s is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].s,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

R^1 (right_open_halfline s) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

[.r,s.] ` is complex-membered ext-real-membered real-membered Element of K32(REAL)

REAL \ [.r,s.] is complex-membered ext-real-membered real-membered set

(R^1 (left_open_halfline r)) \/ (R^1 (right_open_halfline s)) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set

Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl ([.r,s.] `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

Cl (left_open_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)

Cl (right_open_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)

(Cl (left_open_halfline r)) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

Cl (R^1 (left_open_halfline r)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl (R^1 (left_open_halfline r))) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered set

Cl (R^1 (right_open_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl (R^1 (left_open_halfline r))) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(R^1 (left_closed_halfline r)) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(R^1 (left_closed_halfline r)) \/ (R^1 (right_closed_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is ext-real real V65() set

s is ext-real real V65() set

].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl ].r,s.[ is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded Element of K32(REAL)

[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

R^1 (right_closed_halfline s) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

].r,s.[ ` is complex-membered ext-real-membered real-membered Element of K32(REAL)

REAL \ ].r,s.[ is complex-membered ext-real-membered real-membered set

(R^1 (left_closed_halfline r)) \/ (R^1 (right_closed_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set

Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl (].r,s.[ `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

Cl (left_closed_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)

Cl (right_closed_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)

(Cl (left_closed_halfline r)) \/ (Cl (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

(Cl (left_closed_halfline r)) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

r is ext-real real V65() set

s is ext-real real V65() set

[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

left_open_halfline r is complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

R^1 (left_open_halfline r) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

R^1 (right_closed_halfline s) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

[.r,s.[ ` is complex-membered ext-real-membered real-membered Element of K32(REAL)

REAL \ [.r,s.[ is complex-membered ext-real-membered real-membered set

(R^1 (left_open_halfline r)) \/ (R^1 (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set

Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl ([.r,s.[ `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

Cl (left_open_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)

Cl (right_closed_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)

(Cl (left_open_halfline r)) \/ (Cl (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

Cl (R^1 (left_open_halfline r)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl (R^1 (left_open_halfline r))) \/ (Cl (right_closed_halfline s)) is complex-membered ext-real-membered real-membered set

Cl (R^1 (right_closed_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl (R^1 (left_open_halfline r))) \/ (Cl (R^1 (right_closed_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(R^1 (left_closed_halfline r)) \/ (Cl (R^1 (right_closed_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is ext-real real V65() set

s is ext-real real V65() set

].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

left_closed_halfline r is complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval Element of K32(REAL)

].-infty,r.] is complex-membered ext-real-membered real-membered non left_end bounded_above interval set

right_closed_halfline s is complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval Element of K32(REAL)

[.s,+infty.[ is complex-membered ext-real-membered real-membered non right_end bounded_below interval set

(left_closed_halfline r) \/ (right_closed_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

[.r,s.] /\ ((left_closed_halfline r) \/ (right_closed_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

].r,s.] ` is complex-membered ext-real-membered real-membered Element of K32(REAL)

REAL \ ].r,s.] is complex-membered ext-real-membered real-membered set

right_open_halfline s is complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval Element of K32(REAL)

].s,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

(left_closed_halfline r) \/ (right_open_halfline s) is complex-membered ext-real-membered real-membered Element of K32(REAL)

R^1 (right_open_halfline s) is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

R^1 (left_closed_halfline r) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

n ` is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

the carrier of R^1 \ n is complex-membered ext-real-membered real-membered set

Cl (n `) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Cl (].r,s.] `) is complex-membered ext-real-membered real-membered closed Element of K32(REAL)

Cl (left_closed_halfline r) is complex-membered ext-real-membered real-membered closed bounded_above Element of K32(REAL)

Cl (right_open_halfline s) is complex-membered ext-real-membered real-membered closed bounded_below Element of K32(REAL)

(Cl (left_closed_halfline r)) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered Element of K32(REAL)

Cl (R^1 (left_closed_halfline r)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl (R^1 (left_closed_halfline r))) \/ (Cl (right_open_halfline s)) is complex-membered ext-real-membered real-membered set

Cl (R^1 (right_open_halfline s)) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(Cl (R^1 (left_closed_halfline r))) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

(R^1 (left_closed_halfline r)) \/ (Cl (R^1 (right_open_halfline s))) is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is ext-real real V65() set

s is ext-real real V65() set

[.r,s.] is complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval Element of K32(REAL)

].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

F is set

{} R^1 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of R^1)

Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

C is ext-real real V65() Element of the carrier of R^1

F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is ext-real real V65() set

s is ext-real real V65() set

].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Int F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is ext-real real V65() set

s is ext-real real V65() set

[.r,s.[ is complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

F is set

{} R^1 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of R^1)

Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

C is ext-real real V65() Element of the carrier of R^1

F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is ext-real real V65() set

s is ext-real real V65() set

].r,s.] is complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

].r,s.[ is complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

n is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

Int n is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

F is set

{} R^1 is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126() V127() bounded_below bounded_above real-bounded interval Element of K32( the carrier of R^1)

Fr n is closed complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

{r,s} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

C is ext-real real V65() Element of the carrier of R^1

F is open complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is real-membered TopStruct

the carrier of r is complex-membered ext-real-membered real-membered set

K32( the carrier of r) is non empty set

s is complex-membered ext-real-membered real-membered interval Element of K32( the carrier of r)

r | s is strict real-membered SubSpace of r

[#] (r | s) is non proper dense complex-membered ext-real-membered real-membered Element of K32( the carrier of (r | s))

the carrier of (r | s) is complex-membered ext-real-membered real-membered set

K32( the carrier of (r | s)) is non empty set

r is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

R^1 r is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

r is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

s is ext-real set

n is ext-real set

[.s,n.] is ext-real-membered interval set

r is complex-membered ext-real-membered real-membered Element of K32( the carrier of R^1)

s is Relation-like non-empty empty-yielding RAT -valued functional ordinal natural empty proper ext-real non positive non negative finite finite-yielding V43() cardinal {} -element real V65() V66() FinSequence-like FinSequence-membered open closed boundary nowhere_dense connected complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() V124() V125() V126()