:: PSCOMP_1 semantic presentation

REAL is non empty non trivial V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() non with_non-empty_elements non empty-membered set

NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below non with_non-empty_elements Element of K32(REAL)

K32(REAL) is non empty set

COMPLEX is non empty non trivial V47() V53() V54() non empty-membered set

RAT is non empty non trivial V47() V48() V49() V50() V53() V54() non empty-membered set

INT is non empty non trivial V47() V48() V49() V50() V51() V53() V54() non empty-membered set

omega is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below non with_non-empty_elements set

K32(omega) is non empty set

K32(NAT) is non empty set

K33(COMPLEX,COMPLEX) is non empty Relation-like complex-valued set

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

K33(COMPLEX,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

ExtREAL is non empty V48() V68() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below Element of NAT

K33(1,1) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

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

K33(K33(1,1),1) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

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

K33(K33(1,1),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

K33(REAL,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

K33(K33(REAL,REAL),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below Element of NAT

K33(2,2) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K33(K33(2,2),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

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

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V164() V189() V190() V191() V192() V193() V194() V195() strict RLTopStruct

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

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

K33(K33(COMPLEX,COMPLEX),COMPLEX) is non empty Relation-like complex-valued set

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

K33(RAT,RAT) is non empty Relation-like RAT -valued complex-valued ext-real-valued real-valued set

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

K33(K33(RAT,RAT),RAT) is non empty Relation-like RAT -valued complex-valued ext-real-valued real-valued set

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

K33(INT,INT) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

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

K33(K33(INT,INT),INT) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

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

K33(NAT,NAT) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K33(K33(NAT,NAT),NAT) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

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

{} is empty Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() set

the empty Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() set is empty Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() set

0 is empty Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() Element of NAT

K33(NAT,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

0 " is empty Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() set

K32(K32(REAL)) is non empty set

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

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

r is V47() V48() V49() Element of K32(REAL)

-- r is V47() V48() V49() Element of K32(REAL)

s is V24() real ext-real set

- s is V24() real ext-real set

p is ext-real set

{ (- b

p is V24() Element of COMPLEX

- p is V24() Element of COMPLEX

p is V24() real ext-real Element of REAL

r is non empty set

K33(r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

K32(K33(r,REAL)) is non empty set

s is non empty Relation-like r -defined REAL -valued Function-like V29(r) V30(r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(r,REAL))

- s is non empty Relation-like r -defined REAL -valued Function-like V29(r) V30(r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(r,REAL))

- 1 is V24() real ext-real non positive V45() set

(- 1) * s is Relation-like r -defined Function-like V29(r) complex-valued ext-real-valued real-valued set

s .: r is non empty V47() V48() V49() Element of K32(REAL)

lower_bound (s .: r) is V24() real ext-real Element of REAL

-- (s .: r) is V47() V48() V49() Element of K32(REAL)

(- s) .: r is non empty V47() V48() V49() Element of K32(REAL)

upper_bound ((- s) .: r) is V24() real ext-real set

upper_bound ((- s) .: r) is V24() real ext-real Element of REAL

-- (-- (s .: r)) is V47() V48() V49() Element of K32(REAL)

lower_bound (-- (-- (s .: r))) is V24() real ext-real Element of REAL

- (lower_bound (-- (-- (s .: r)))) is V24() real ext-real Element of REAL

- (lower_bound (s .: r)) is V24() real ext-real Element of REAL

r is non empty 1-sorted

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

the carrier of r --> 0 is non empty Relation-like the carrier of r -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like constant V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued natural-valued Element of K32(K33( the carrier of r,REAL))

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

dom p is non empty Element of K32( the carrier of r)

K32( the carrier of r) is non empty set

rng p is non empty V47() V48() V49() Element of K32(REAL)

{0} is non empty V47() V48() V49() V50() V51() V52() V54() V58() left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)

p .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

r is 1-sorted

the carrier of r is set

K33( the carrier of r,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

s .: the carrier of r is V47() V48() V49() Element of K32(REAL)

lower_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

upper_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued bounded_below Element of K32(K33( the carrier of r,REAL))

(r,s) is V24() real ext-real Element of REAL

s .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

lower_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

p is Element of the carrier of r

s . p is V24() real ext-real Element of REAL

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued bounded_below Element of K32(K33( the carrier of r,REAL))

(r,s) is V24() real ext-real Element of REAL

s .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

lower_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

p is V24() real ext-real Element of REAL

p is V24() real ext-real set

p is set

s . p is V24() real ext-real Element of REAL

r is V24() real ext-real set

s is non empty TopSpace-like TopStruct

the carrier of s is non empty set

K33( the carrier of s,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

p is non empty Relation-like the carrier of s -defined REAL -valued Function-like V29( the carrier of s) V30( the carrier of s, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of s,REAL))

(s,p) is V24() real ext-real Element of REAL

p .: the carrier of s is non empty V47() V48() V49() Element of K32(REAL)

lower_bound (p .: the carrier of s) is V24() real ext-real Element of REAL

p is V24() real ext-real set

p is Element of the carrier of s

p . p is V24() real ext-real Element of REAL

p is V24() real ext-real set

p is set

p . p is V24() real ext-real Element of REAL

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued bounded_above Element of K32(K33( the carrier of r,REAL))

(r,s) is V24() real ext-real Element of REAL

s .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

upper_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

p is Element of the carrier of r

s . p is V24() real ext-real Element of REAL

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued bounded_above Element of K32(K33( the carrier of r,REAL))

(r,s) is V24() real ext-real Element of REAL

s .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

upper_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

p is V24() real ext-real set

p is V24() real ext-real set

p is set

s . p is V24() real ext-real Element of REAL

r is V24() real ext-real set

s is non empty TopSpace-like TopStruct

the carrier of s is non empty set

K33( the carrier of s,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

p is non empty Relation-like the carrier of s -defined REAL -valued Function-like V29( the carrier of s) V30( the carrier of s, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of s,REAL))

(s,p) is V24() real ext-real Element of REAL

p .: the carrier of s is non empty V47() V48() V49() Element of K32(REAL)

upper_bound (p .: the carrier of s) is V24() real ext-real Element of REAL

p is V24() real ext-real set

p is Element of the carrier of s

p . p is V24() real ext-real Element of REAL

p is V24() real ext-real set

p is set

p . p is V24() real ext-real Element of REAL

r is non empty 1-sorted

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of K32(K33( the carrier of r,REAL))

(r,s) is V24() real ext-real Element of REAL

s .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

lower_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

(r,s) is V24() real ext-real Element of REAL

upper_bound (s .: the carrier of r) is V24() real ext-real Element of REAL

r is TopStruct

the carrier of r is set

K33( the carrier of r,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

the carrier of r --> 0 is non empty Relation-like the carrier of r -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like constant V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued natural-valued Element of K32(K33( the carrier of r,REAL))

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

dom p is non empty Element of K32( the carrier of r)

K32( the carrier of r) is non empty set

p is V47() V48() V49() Element of K32(REAL)

p " p is Element of K32( the carrier of r)

rng p is non empty V47() V48() V49() Element of K32(REAL)

{0} is non empty V47() V48() V49() V50() V51() V52() V54() V58() left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)

(rng p) /\ p is V47() V48() V49() Element of K32(REAL)

p " ((rng p) /\ p) is Element of K32( the carrier of r)

p " (rng p) is Element of K32( the carrier of r)

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

(rng p) /\ p is V47() V48() V49() Element of K32(REAL)

p " ((rng p) /\ p) is Element of K32( the carrier of r)

p " {} is empty proper Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() closed compact Element of K32( the carrier of r)

{} r is empty proper Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() closed compact Element of K32( the carrier of r)

r is non empty TopSpace-like TopStruct

s is non empty TopSpace-like SubSpace of r

the carrier of s is non empty set

K33( the carrier of s,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

the carrier of s --> 0 is non empty Relation-like the carrier of s -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like constant V29( the carrier of s) V30( the carrier of s, REAL ) complex-valued ext-real-valued real-valued natural-valued Element of K32(K33( the carrier of s,REAL))

p is non empty Relation-like the carrier of s -defined REAL -valued Function-like V29( the carrier of s) V30( the carrier of s, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of s,REAL))

dom p is non empty Element of K32( the carrier of s)

K32( the carrier of s) is non empty set

p is V47() V48() V49() Element of K32(REAL)

p " p is Element of K32( the carrier of s)

rng p is non empty V47() V48() V49() Element of K32(REAL)

{0} is non empty V47() V48() V49() V50() V51() V52() V54() V58() left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)

(rng p) /\ p is V47() V48() V49() Element of K32(REAL)

p " ((rng p) /\ p) is Element of K32( the carrier of s)

p " (rng p) is Element of K32( the carrier of s)

[#] s is non empty non proper closed Element of K32( the carrier of s)

(rng p) /\ p is V47() V48() V49() Element of K32(REAL)

p " ((rng p) /\ p) is Element of K32( the carrier of s)

p " {} is empty proper Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() closed compact Element of K32( the carrier of s)

{} s is empty proper Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V47() V48() V49() V50() V51() V52() V53() V54() V55() V58() bounded_below bounded_above real-bounded V68() closed compact Element of K32( the carrier of s)

r is TopStruct

the carrier of r is set

K33( the carrier of r,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

p is V47() V48() V49() Element of K32(REAL)

p ` is V47() V48() V49() Element of K32(REAL)

REAL \ p is V47() V48() V49() set

s " (p `) is Element of K32( the carrier of r)

K32( the carrier of r) is non empty set

s " REAL is Element of K32( the carrier of r)

s " p is Element of K32( the carrier of r)

(s " REAL) \ (s " p) is Element of K32( the carrier of r)

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

([#] r) \ (s " p) is Element of K32( the carrier of r)

([#] r) \ (([#] r) \ (s " p)) is Element of K32( the carrier of r)

p is V47() V48() V49() Element of K32(REAL)

s " p is Element of K32( the carrier of r)

p ` is V47() V48() V49() Element of K32(REAL)

REAL \ p is V47() V48() V49() set

(p `) ` is V47() V48() V49() Element of K32(REAL)

REAL \ (p `) is V47() V48() V49() set

s " (p `) is Element of K32( the carrier of r)

(s " REAL) \ (s " p) is Element of K32( the carrier of r)

([#] r) \ (s " p) is Element of K32( the carrier of r)

r is TopStruct

the carrier of r is set

K33( the carrier of r,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

- s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

- 1 is V24() real ext-real non positive V45() set

(- 1) * s is Relation-like the carrier of r -defined Function-like V29( the carrier of r) complex-valued ext-real-valued real-valued set

p is V47() V48() V49() Element of K32(REAL)

(- s) " p is Element of K32( the carrier of r)

K32( the carrier of r) is non empty set

-- p is V47() V48() V49() Element of K32(REAL)

s " (-- p) is Element of K32( the carrier of r)

r is V24() real ext-real Element of REAL

s is TopStruct

the carrier of s is set

K33( the carrier of s,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

p is Relation-like the carrier of s -defined REAL -valued Function-like V29( the carrier of s) V30( the carrier of s, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of s,REAL))

r + p is Relation-like the carrier of s -defined REAL -valued Function-like V29( the carrier of s) V30( the carrier of s, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of s,REAL))

p is V47() V48() V49() Element of K32(REAL)

(r + p) " p is Element of K32( the carrier of s)

K32( the carrier of s) is non empty set

- r is V24() real ext-real Element of REAL

(- r) ++ p is V47() V48() V49() Element of K32(REAL)

p " ((- r) ++ p) is Element of K32( the carrier of s)

r is TopStruct

the carrier of r is set

K33( the carrier of r,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

rng s is V47() V48() V49() Element of K32(REAL)

Inv s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

p is V47() V48() V49() Element of K32(REAL)

(Inv s) " p is Element of K32( the carrier of r)

K32( the carrier of r) is non empty set

{0} is non empty V47() V48() V49() V50() V51() V52() V54() V58() left_end right_end bounded_below bounded_above real-bounded Element of K32(REAL)

p \ {0} is V47() V48() V49() Element of K32(REAL)

p is V47() V48() V49() with_non-empty_elements Element of K32(REAL)

Inv p is V47() V48() V49() with_non-empty_elements Element of K32(REAL)

{ (1 / b

(Inv p) /\ (rng s) is V47() V48() V49() Element of K32(REAL)

Cl ((Inv p) /\ (rng s)) is V47() V48() V49() closed Element of K32(REAL)

{ b

meet { b

p is set

(Cl ((Inv p) /\ (rng s))) /\ (rng s) is V47() V48() V49() Element of K32(REAL)

Q is V24() real ext-real Element of REAL

Q is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(NAT,REAL))

rng Q is non empty V47() V48() V49() Element of K32(REAL)

lim Q is V24() real ext-real Element of REAL

Q " is non empty Relation-like NAT -defined REAL -valued Function-like V29( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(NAT,REAL))

rng (Q ") is non empty V47() V48() V49() Element of K32(REAL)

r29 is set

dom (Q ") is non empty V47() V48() V49() V50() V51() V52() left_end bounded_below Element of K32(NAT)

fx9 is set

(Q ") . fx9 is V24() real ext-real Element of REAL

fx9 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT

Q . fx9 is V24() real ext-real Element of REAL

1 / (Q . fx9) is V24() real ext-real Element of REAL

(Q . fx9) " is V24() real ext-real set

1 * ((Q . fx9) ") is V24() real ext-real set

1 / (1 / (Q . fx9)) is V24() real ext-real Element of REAL

(1 / (Q . fx9)) " is V24() real ext-real set

1 * ((1 / (Q . fx9)) ") is V24() real ext-real set

(Q ") . fx9 is V24() real ext-real Element of REAL

(Q . fx9) " is V24() real ext-real Element of REAL

r29 is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT

Q . r29 is V24() real ext-real Element of REAL

lim (Q ") is V24() real ext-real Element of REAL

(lim Q) " is V24() real ext-real Element of REAL

1 / (lim (Q ")) is V24() real ext-real Element of REAL

(lim (Q ")) " is V24() real ext-real set

1 * ((lim (Q ")) ") is V24() real ext-real set

s " (Cl ((Inv p) /\ (rng s))) is Element of K32( the carrier of r)

s " ((Inv p) /\ (rng s)) is Element of K32( the carrier of r)

p is set

(Inv s) . p is V24() real ext-real Element of REAL

s . p is V24() real ext-real Element of REAL

(s . p) " is V24() real ext-real Element of REAL

(Inv s) " p is Element of K32( the carrier of r)

s " (Inv p) is Element of K32( the carrier of r)

bool REAL is non empty Element of K32(K32(REAL))

r is TopStruct

the carrier of r is set

K33( the carrier of r,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

bool the carrier of r is non empty Element of K32(K32( the carrier of r))

K32( the carrier of r) is non empty set

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

s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

" s is non empty Relation-like bool REAL -defined bool the carrier of r -valued Function-like V29( bool REAL) V30( bool REAL, bool the carrier of r) Element of K32(K33((bool REAL),(bool the carrier of r)))

K33((bool REAL),(bool the carrier of r)) is non empty Relation-like set

K32(K33((bool REAL),(bool the carrier of r))) is non empty set

p is Element of K32(K32(REAL))

(" s) .: p is Element of K32((bool the carrier of r))

K32((bool the carrier of r)) is non empty set

p is Element of K32( the carrier of r)

p is set

(" s) . p is set

s " p is Element of K32( the carrier of r)

p is V47() V48() V49() Element of K32(REAL)

r is TopStruct

the carrier of r is set

K33( the carrier of r,REAL) is Relation-like complex-valued ext-real-valued real-valued set

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

bool the carrier of r is non empty Element of K32(K32( the carrier of r))

K32( the carrier of r) is non empty set

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

s is Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

" s is non empty Relation-like bool REAL -defined bool the carrier of r -valued Function-like V29( bool REAL) V30( bool REAL, bool the carrier of r) Element of K32(K33((bool REAL),(bool the carrier of r)))

K33((bool REAL),(bool the carrier of r)) is non empty Relation-like set

K32(K33((bool REAL),(bool the carrier of r))) is non empty set

p is Element of K32(K32(REAL))

(" s) .: p is Element of K32((bool the carrier of r))

K32((bool the carrier of r)) is non empty set

p is Element of K32( the carrier of r)

p is set

(" s) . p is set

s " p is Element of K32( the carrier of r)

p is V47() V48() V49() Element of K32(REAL)

r is non empty TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

K32( the carrier of r) is non empty set

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

p is Element of K32( the carrier of r)

s | p is Relation-like p -defined the carrier of r -defined REAL -valued complex-valued ext-real-valued real-valued set

r | p is strict SubSpace of r

the carrier of (r | p) is set

K33( the carrier of (r | p),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of (r | p),REAL)) is non empty set

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

K32( the carrier of r) is non empty set

p is Element of K32( the carrier of r)

r | p is strict TopSpace-like SubSpace of r

the carrier of (r | p) is set

K33( the carrier of (r | p),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of (r | p),REAL)) is non empty set

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued (r) Element of K32(K33( the carrier of r,REAL))

(r,s,p) is Relation-like p -defined the carrier of r -defined the carrier of (r | p) -defined REAL -valued Function-like V29( the carrier of (r | p)) V30( the carrier of (r | p), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (r | p),REAL))

p is V47() V48() V49() Element of K32(REAL)

s " p is Element of K32( the carrier of r)

(r,s,p) " p is Element of K32( the carrier of (r | p))

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

p /\ (s " p) is Element of K32( the carrier of r)

p is Relation-like the carrier of (r | p) -defined REAL -valued Function-like V29( the carrier of (r | p)) V30( the carrier of (r | p), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (r | p),REAL))

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K32( the carrier of r) is non empty set

s is non empty compact Element of K32( the carrier of r)

r | s is non empty strict TopSpace-like SubSpace of r

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

- s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

- 1 is V24() real ext-real non positive V45() set

(- 1) * s is Relation-like the carrier of r -defined Function-like V29( the carrier of r) complex-valued ext-real-valued real-valued set

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

- s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

(- 1) * s is Relation-like the carrier of r -defined Function-like V29( the carrier of r) complex-valued ext-real-valued real-valued set

- (- s) is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

(- 1) * (- s) is Relation-like the carrier of r -defined Function-like V29( the carrier of r) complex-valued ext-real-valued real-valued set

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

p .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

upper_bound (p .: the carrier of r) is V24() real ext-real Element of REAL

- p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

- 1 is V24() real ext-real non positive V45() set

(- 1) * p is Relation-like the carrier of r -defined Function-like V29( the carrier of r) complex-valued ext-real-valued real-valued set

(upper_bound (p .: the carrier of r)) + (- p) is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

Inv ((upper_bound (p .: the carrier of r)) + (- p)) is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

(Inv ((upper_bound (p .: the carrier of r)) + (- p))) .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

rng ((upper_bound (p .: the carrier of r)) + (- p)) is non empty V47() V48() V49() Element of K32(REAL)

dom ((upper_bound (p .: the carrier of r)) + (- p)) is non empty Element of K32( the carrier of r)

K32( the carrier of r) is non empty set

fx9 is set

((upper_bound (p .: the carrier of r)) + (- p)) . fx9 is V24() real ext-real Element of REAL

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

fx9 is Element of the carrier of r

p . fx9 is V24() real ext-real Element of REAL

Q is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

- Q is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

(- 1) * Q is Relation-like the carrier of r -defined Function-like V29( the carrier of r) complex-valued ext-real-valued real-valued set

(- Q) . fx9 is V24() real ext-real Element of REAL

(upper_bound (p .: the carrier of r)) + ((- Q) . fx9) is V24() real ext-real Element of REAL

p . fx9 is V24() real ext-real Element of REAL

- (p . fx9) is V24() real ext-real Element of REAL

(upper_bound (p .: the carrier of r)) + (- (p . fx9)) is V24() real ext-real Element of REAL

(upper_bound (p .: the carrier of r)) - (p . fx9) is V24() real ext-real Element of REAL

- (p . fx9) is V24() real ext-real set

(upper_bound (p .: the carrier of r)) + (- (p . fx9)) is V24() real ext-real set

fx9 is V24() real ext-real set

fx9 is V24() real ext-real set

fx9 is V24() real ext-real set

x is V24() real ext-real set

x is V24() real ext-real set

fx9 is V24() real ext-real set

x is V24() real ext-real set

fx9 is V24() real ext-real set

fx9 is V24() real ext-real set

1 / fx9 is V24() real ext-real Element of REAL

fx9 " is V24() real ext-real set

1 * (fx9 ") is V24() real ext-real set

(upper_bound (p .: the carrier of r)) - (1 / fx9) is V24() real ext-real Element of REAL

- (1 / fx9) is V24() real ext-real set

(upper_bound (p .: the carrier of r)) + (- (1 / fx9)) is V24() real ext-real set

fx9 is V24() real ext-real set

x is set

p . x is V24() real ext-real Element of REAL

x is Element of the carrier of r

p . x is V24() real ext-real Element of REAL

(p . x) + 0 is V24() real ext-real Element of REAL

(upper_bound (p .: the carrier of r)) - (p . x) is V24() real ext-real Element of REAL

- (p . x) is V24() real ext-real set

(upper_bound (p .: the carrier of r)) + (- (p . x)) is V24() real ext-real set

(Inv ((upper_bound (p .: the carrier of r)) + (- p))) . x is V24() real ext-real Element of REAL

p . x is V24() real ext-real Element of REAL

(p . x) " is V24() real ext-real Element of REAL

(- Q) . x is V24() real ext-real Element of REAL

(upper_bound (p .: the carrier of r)) + ((- Q) . x) is V24() real ext-real Element of REAL

((upper_bound (p .: the carrier of r)) + ((- Q) . x)) " is V24() real ext-real Element of REAL

1 / ((upper_bound (p .: the carrier of r)) + ((- Q) . x)) is V24() real ext-real Element of REAL

((upper_bound (p .: the carrier of r)) + ((- Q) . x)) " is V24() real ext-real set

1 * (((upper_bound (p .: the carrier of r)) + ((- Q) . x)) ") is V24() real ext-real set

- (p . x) is V24() real ext-real Element of REAL

(upper_bound (p .: the carrier of r)) + (- (p . x)) is V24() real ext-real Element of REAL

1 / ((upper_bound (p .: the carrier of r)) + (- (p . x))) is V24() real ext-real Element of REAL

((upper_bound (p .: the carrier of r)) + (- (p . x))) " is V24() real ext-real set

1 * (((upper_bound (p .: the carrier of r)) + (- (p . x))) ") is V24() real ext-real set

1 / ((upper_bound (p .: the carrier of r)) - (p . x)) is V24() real ext-real Element of REAL

((upper_bound (p .: the carrier of r)) - (p . x)) " is V24() real ext-real set

1 * (((upper_bound (p .: the carrier of r)) - (p . x)) ") is V24() real ext-real set

fx9 * ((upper_bound (p .: the carrier of r)) - (p . x)) is V24() real ext-real Element of REAL

(p . x) + (1 / fx9) is V24() real ext-real Element of REAL

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

p .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

the Element of the carrier of r is Element of the carrier of r

s . the Element of the carrier of r is V24() real ext-real Element of REAL

{ (right_closed_halfline b

right_closed_halfline (s . the Element of the carrier of r) is V47() V48() V49() closed Element of K32(REAL)

K310((s . the Element of the carrier of r),+infty) is non right_end V68() set

{ b

K32( the carrier of r) is non empty set

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

bool the carrier of r is non empty Element of K32(K32( the carrier of r))

" s is non empty Relation-like bool REAL -defined bool the carrier of r -valued Function-like V29( bool REAL) V30( bool REAL, bool the carrier of r) Element of K32(K33((bool REAL),(bool the carrier of r)))

K33((bool REAL),(bool the carrier of r)) is non empty Relation-like set

K32(K33((bool REAL),(bool the carrier of r))) is non empty set

p is non empty Element of K32(K32(REAL))

(" s) .: p is Element of K32((bool the carrier of r))

K32((bool the carrier of r)) is non empty set

p is Element of K32(K32( the carrier of r))

p is set

Q is set

Q is set

(" s) . Q is set

s " Q is Element of K32( the carrier of r)

r29 is V24() real ext-real Element of REAL

right_closed_halfline r29 is V47() V48() V49() closed Element of K32(REAL)

K310(r29,+infty) is non right_end V68() set

{ b

fx9 is set

(" s) . fx9 is set

s " fx9 is Element of K32( the carrier of r)

fx9 is V24() real ext-real Element of REAL

right_closed_halfline fx9 is V47() V48() V49() closed Element of K32(REAL)

K310(fx9,+infty) is non right_end V68() set

{ b

s .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

p is set

(" s) . p is set

Q is V24() real ext-real Element of REAL

right_closed_halfline Q is V47() V48() V49() closed Element of K32(REAL)

K310(Q,+infty) is non right_end V68() set

{ b

Q is ext-real set

{ b

s " p is Element of K32( the carrier of r)

r29 is set

s . r29 is V24() real ext-real Element of REAL

p is V47() V48() V49() Element of K32(REAL)

Q is V24() real ext-real Element of REAL

right_closed_halfline Q is V47() V48() V49() closed Element of K32(REAL)

K310(Q,+infty) is non right_end V68() set

{ b

(" s) . (right_closed_halfline (s . the Element of the carrier of r)) is Element of bool the carrier of r

meet p is Element of K32( the carrier of r)

p is set

the Element of p is Element of p

Q is V24() real ext-real Element of REAL

right_closed_halfline Q is V47() V48() V49() closed Element of K32(REAL)

K310(Q,+infty) is non right_end V68() set

{ b

r29 is Element of the carrier of r

s . r29 is V24() real ext-real Element of REAL

meet p is V47() V48() V49() Element of K32(REAL)

fx9 is V24() real ext-real set

{ b

x is V24() real ext-real Element of REAL

fx9 is V24() real ext-real Element of REAL

right_closed_halfline fx9 is V47() V48() V49() closed Element of K32(REAL)

K310(fx9,+infty) is non right_end V68() set

{ b

{ b

x is V24() real ext-real Element of REAL

the Element of the carrier of r is Element of the carrier of r

s . the Element of the carrier of r is V24() real ext-real Element of REAL

{ (left_closed_halfline b

left_closed_halfline (s . the Element of the carrier of r) is V47() V48() V49() closed Element of K32(REAL)

K311(-infty,(s . the Element of the carrier of r)) is non left_end V68() set

{ b

K32( the carrier of r) is non empty set

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

bool the carrier of r is non empty Element of K32(K32( the carrier of r))

" s is non empty Relation-like bool REAL -defined bool the carrier of r -valued Function-like V29( bool REAL) V30( bool REAL, bool the carrier of r) Element of K32(K33((bool REAL),(bool the carrier of r)))

K33((bool REAL),(bool the carrier of r)) is non empty Relation-like set

K32(K33((bool REAL),(bool the carrier of r))) is non empty set

p is non empty Element of K32(K32(REAL))

(" s) .: p is Element of K32((bool the carrier of r))

K32((bool the carrier of r)) is non empty set

p is V47() V48() V49() Element of K32(REAL)

Q is V24() real ext-real Element of REAL

left_closed_halfline Q is V47() V48() V49() closed Element of K32(REAL)

K311(-infty,Q) is non left_end V68() set

{ b

p is Element of K32(K32( the carrier of r))

p is set

Q is set

Q is set

(" s) . Q is set

s " Q is Element of K32( the carrier of r)

r29 is V24() real ext-real Element of REAL

left_closed_halfline r29 is V47() V48() V49() closed Element of K32(REAL)

K311(-infty,r29) is non left_end V68() set

{ b

fx9 is set

(" s) . fx9 is set

s " fx9 is Element of K32( the carrier of r)

fx9 is V24() real ext-real Element of REAL

left_closed_halfline fx9 is V47() V48() V49() closed Element of K32(REAL)

K311(-infty,fx9) is non left_end V68() set

{ b

s .: the carrier of r is non empty V47() V48() V49() Element of K32(REAL)

p is set

(" s) . p is set

Q is V24() real ext-real Element of REAL

left_closed_halfline Q is V47() V48() V49() closed Element of K32(REAL)

K311(-infty,Q) is non left_end V68() set

{ b

Q is ext-real set

{ b

s " p is Element of K32( the carrier of r)

r29 is set

s . r29 is V24() real ext-real Element of REAL

(" s) . (left_closed_halfline (s . the Element of the carrier of r)) is Element of bool the carrier of r

meet p is Element of K32( the carrier of r)

p is set

the Element of p is Element of p

Q is V24() real ext-real Element of REAL

left_closed_halfline Q is V47() V48() V49() closed Element of K32(REAL)

K311(-infty,Q) is non left_end V68() set

{ b

r29 is Element of the carrier of r

s . r29 is V24() real ext-real Element of REAL

meet p is V47() V48() V49() Element of K32(REAL)

fx9 is V24() real ext-real set

{ b

x is V24() real ext-real Element of REAL

fx9 is V24() real ext-real Element of REAL

left_closed_halfline fx9 is V47() V48() V49() closed Element of K32(REAL)

K311(-infty,fx9) is non left_end V68() set

{ b

{ b

x is V24() real ext-real Element of REAL

the non empty TopSpace-like compact () TopStruct is non empty TopSpace-like compact () TopStruct

r is non empty TopSpace-like () TopStruct

the carrier of r is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of r,REAL))

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K32( the carrier of r) is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Element of K32( the carrier of r)

r | s is non empty strict TopSpace-like SubSpace of r

p is compact Element of K32( the carrier of r)

r | p is strict TopSpace-like SubSpace of r

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued (r) Element of K32(K33( the carrier of r,REAL))

(r,p,p) is Relation-like p -defined the carrier of r -defined the carrier of (r | p) -defined REAL -valued Function-like V29( the carrier of (r | p)) V30( the carrier of (r | p), REAL ) complex-valued ext-real-valued real-valued (r | p) Element of K32(K33( the carrier of (r | p),REAL))

the carrier of (r | p) is set

K33( the carrier of (r | p),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of (r | p),REAL)) is non empty set

((r | p),(r,p,p)) is V24() real ext-real Element of REAL

(r,p,p) .: the carrier of (r | p) is V47() V48() V49() Element of K32(REAL)

lower_bound ((r,p,p) .: the carrier of (r | p)) is V24() real ext-real Element of REAL

(r,p,s) is non empty Relation-like s -defined the carrier of r -defined the carrier of (r | s) -defined REAL -valued Function-like V29( the carrier of (r | s)) V30( the carrier of (r | s), REAL ) complex-valued ext-real-valued real-valued (r | s) Element of K32(K33( the carrier of (r | s),REAL))

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

K33( the carrier of (r | s),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

((r | s),(r,p,s)) is V24() real ext-real Element of REAL

(r,p,s) .: the carrier of (r | s) is non empty V47() V48() V49() Element of K32(REAL)

lower_bound ((r,p,s) .: the carrier of (r | s)) is V24() real ext-real Element of REAL

(r,p,p) .: p is V47() V48() V49() Element of K32(REAL)

p .: p is V47() V48() V49() Element of K32(REAL)

(r,p,s) .: s is V47() V48() V49() Element of K32(REAL)

p .: s is V47() V48() V49() Element of K32(REAL)

p is non empty compact Element of K32( the carrier of r)

r | p is non empty strict TopSpace-like compact () SubSpace of r

the carrier of (r | p) is non empty set

(r,p,p) is non empty Relation-like p -defined the carrier of r -defined the carrier of (r | p) -defined REAL -valued Function-like V29( the carrier of (r | p)) V30( the carrier of (r | p), REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below with_max with_min bounded (r | p) Element of K32(K33( the carrier of (r | p),REAL))

K33( the carrier of (r | p),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of (r | p),REAL)) is non empty set

(r,p,p) .: the carrier of (r | p) is non empty V47() V48() V49() Element of K32(REAL)

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K32( the carrier of r) is non empty set

K33( the carrier of r,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

s is non empty Element of K32( the carrier of r)

r | s is non empty strict TopSpace-like SubSpace of r

p is compact Element of K32( the carrier of r)

r | p is strict TopSpace-like SubSpace of r

p is non empty Relation-like the carrier of r -defined REAL -valued Function-like V29( the carrier of r) V30( the carrier of r, REAL ) complex-valued ext-real-valued real-valued (r) Element of K32(K33( the carrier of r,REAL))

(r,p,s) is non empty Relation-like s -defined the carrier of r -defined the carrier of (r | s) -defined REAL -valued Function-like V29( the carrier of (r | s)) V30( the carrier of (r | s), REAL ) complex-valued ext-real-valued real-valued (r | s) Element of K32(K33( the carrier of (r | s),REAL))

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

K33( the carrier of (r | s),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

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

((r | s),(r,p,s)) is V24() real ext-real Element of REAL

(r,p,s) .: the carrier of (r | s) is non empty V47() V48() V49() Element of K32(REAL)

upper_bound ((r,p,s) .: the carrier of (r | s)) is V24() real ext-real Element of REAL

(r,p,p) is Relation-like p -defined the carrier of r -defined the carrier of (r | p) -defined REAL -valued Function-like V29( the carrier of (r | p)) V30( the carrier of (r | p), REAL ) complex-valued ext-real-valued real-valued (r | p) Element of K32(K33( the carrier of (r | p),REAL))

the carrier of (r | p) is set

K33( the carrier of (r | p),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of (r | p),REAL)) is non empty set

((r | p),(r,p,p)) is V24() real ext-real Element of REAL

(r,p,p) .: the carrier of (r | p) is V47() V48() V49() Element of K32(REAL)

upper_bound ((r,p,p) .: the carrier of (r | p)) is V24() real ext-real Element of REAL

(r,p,p) .: p is V47() V48() V49() Element of K32(REAL)

p .: p is V47() V48() V49() Element of K32(REAL)

(r,p,s) .: s is V47() V48() V49() Element of K32(REAL)

p .: s is V47() V48() V49() Element of K32(REAL)

p is non empty compact Element of K32( the carrier of r)

r | p is non empty strict TopSpace-like compact () SubSpace of r

the carrier of (r | p) is non empty set

(r,p,p) is non empty Relation-like p -defined the carrier of r -defined the carrier of (r | p) -defined REAL -valued Function-like V29( the carrier of (r | p)) V30( the carrier of (r | p), REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below with_max with_min bounded (r | p) Element of K32(K33( the carrier of (r | p),REAL))

K33( the carrier of (r | p),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of (r | p),REAL)) is non empty set

(r,p,p) .: the carrier of (r | p) is non empty V47() V48() V49() Element of K32(REAL)

r is epsilon-transitive epsilon-connected ordinal natural V24() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT

TOP-REAL r is non empty TopSpace-like T_0 T_1 T_2 V164() V189() V190() V191() V192() V193() V194() V195() strict RLTopStruct

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

K32( the carrier of (TOP-REAL r)) is non empty set

s is closed compact Element of K32( the carrier of (TOP-REAL r))

p is closed compact Element of K32( the carrier of (TOP-REAL r))

s /\ p is Element of K32( the carrier of (TOP-REAL r))

p is Element of K32( the carrier of (TOP-REAL r))

K33( the carrier of (TOP-REAL 2),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of (TOP-REAL 2),REAL)) is non empty set

r is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V29( the carrier of (TOP-REAL 2)) V30( the carrier of (TOP-REAL 2), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (TOP-REAL 2),REAL))

s is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V29( the carrier of (TOP-REAL 2)) V30( the carrier of (TOP-REAL 2), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (TOP-REAL 2),REAL))

p is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

r . p is V24() real ext-real Element of REAL

p `1 is V24() real ext-real Element of REAL

s . p is V24() real ext-real Element of REAL

r is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V29( the carrier of (TOP-REAL 2)) V30( the carrier of (TOP-REAL 2), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (TOP-REAL 2),REAL))

s is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V29( the carrier of (TOP-REAL 2)) V30( the carrier of (TOP-REAL 2), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (TOP-REAL 2),REAL))

p is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

r . p is V24() real ext-real Element of REAL

p `2 is V24() real ext-real Element of REAL

s . p is V24() real ext-real Element of REAL

() is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V29( the carrier of (TOP-REAL 2)) V30( the carrier of (TOP-REAL 2), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (TOP-REAL 2),REAL))

() is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V29( the carrier of (TOP-REAL 2)) V30( the carrier of (TOP-REAL 2), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33( the carrier of (TOP-REAL 2),REAL))

r is V24() real ext-real set

s is V24() real ext-real set

].r,s.[ is V47() V48() V49() non left_end non right_end V68() open Element of K32(REAL)

{ b

() " ].r,s.[ is Element of K32( the carrier of (TOP-REAL 2))

{ |[b

p is set

p is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

() . p is V24() real ext-real Element of REAL

p `1 is V24() real ext-real Element of REAL

p `2 is V24() real ext-real Element of REAL

|[(p `1),(p `2)]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

p is V24() real ext-real Element of REAL

p is V24() real ext-real Element of REAL

p is V24() real ext-real Element of REAL

|[p,p]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

() . |[p,p]| is V24() real ext-real Element of REAL

|[p,p]| `1 is V24() real ext-real Element of REAL

r is Element of K32( the carrier of (TOP-REAL 2))

s is V24() real ext-real Element of REAL

p is V24() real ext-real Element of REAL

{ |[b

{ H

{ H

{ |[b

{ |[b

p is set

p is Element of K32( the carrier of (TOP-REAL 2))

p is Element of K32( the carrier of (TOP-REAL 2))

p is V24() real ext-real Element of REAL

Q is V24() real ext-real Element of REAL

|[p,Q]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

p /\ p is Element of K32( the carrier of (TOP-REAL 2))

p is V24() real ext-real Element of REAL

Q is V24() real ext-real Element of REAL

|[p,Q]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

Q is V24() real ext-real Element of REAL

r29 is V24() real ext-real Element of REAL

|[Q,r29]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

|[p,Q]| `1 is V24() real ext-real Element of REAL

|[Q,r29]| `1 is V24() real ext-real Element of REAL

r is V24() real ext-real set

s is V24() real ext-real set

].r,s.[ is V47() V48() V49() non left_end non right_end V68() open Element of K32(REAL)

{ b

() " ].r,s.[ is Element of K32( the carrier of (TOP-REAL 2))

{ |[b

p is set

p is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

() . p is V24() real ext-real Element of REAL

p `2 is V24() real ext-real Element of REAL

p `1 is V24() real ext-real Element of REAL

|[(p `1),(p `2)]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

p is V24() real ext-real Element of REAL

p is V24() real ext-real Element of REAL

p is V24() real ext-real Element of REAL

|[p,p]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

() . |[p,p]| is V24() real ext-real Element of REAL

|[p,p]| `2 is V24() real ext-real Element of REAL

r is Element of K32( the carrier of (TOP-REAL 2))

s is V24() real ext-real Element of REAL

p is V24() real ext-real Element of REAL

{ |[b

{ H

{ H

{ |[b

{ |[b

p is set

p is Element of K32( the carrier of (TOP-REAL 2))

p is Element of K32( the carrier of (TOP-REAL 2))

p is V24() real ext-real Element of REAL

Q is V24() real ext-real Element of REAL

|[p,Q]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

p /\ p is Element of K32( the carrier of (TOP-REAL 2))

p is V24() real ext-real Element of REAL

Q is V24() real ext-real Element of REAL

|[p,Q]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

Q is V24() real ext-real Element of REAL

r29 is V24() real ext-real Element of REAL

|[Q,r29]| is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

|[p,Q]| `2 is V24() real ext-real Element of REAL

|[Q,r29]| `2 is V24() real ext-real Element of REAL

r is V47() V48() V49() Element of K32(REAL)

() " r is Element of K32( the carrier of (TOP-REAL 2))

p is set

p is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

() . p is V24() real ext-real Element of REAL

p is V24() real ext-real set

(() . p) - p is V24() real ext-real Element of REAL

- p is V24() real ext-real set

(() . p) + (- p) is V24() real ext-real set

(() . p) + p is V24() real ext-real Element of REAL

].((() . p) - p),((() . p) + p).[ is V47() V48() V49() non left_end non right_end V68() open Element of K32(REAL)

{ b

p is V24() real ext-real Element of REAL

(() . p) - p is V24() real ext-real Element of REAL

- p is V24() real ext-real set

(() . p) + (- p) is V24() real ext-real set

(() . p) + p is V24() real ext-real Element of REAL

].((() . p) - p),((() . p) + p).[ is V47() V48() V49() non left_end non right_end V68() open Element of K32(REAL)

{ b

() " ].((() . p) - p),((() . p) + p).[ is Element of K32( the carrier of (TOP-REAL 2))

Q is Element of K32( the carrier of (TOP-REAL 2))

Q is Element of K32( the carrier of (TOP-REAL 2))

{ |[b

p is Element of K32( the carrier of (TOP-REAL 2))

r is V47() V48() V49() Element of K32(REAL)

() " r is Element of K32( the carrier of (TOP-REAL 2))

p is set

p is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

() . p is V24() real ext-real Element of REAL

p is V24() real ext-real set

(() . p) - p is V24() real ext-real Element of REAL

- p is V24() real ext-real set

(() . p) + (- p) is V24() real ext-real set

(() . p) + p is V24() real ext-real Element of REAL

].((() . p) - p),((() . p) + p).[ is V47() V48() V49() non left_end non right_end V68() open Element of K32(REAL)

{ b

p is V24() real ext-real Element of REAL

(() . p) - p is V24() real ext-real Element of REAL

- p is V24() real ext-real set

(() . p) + (- p) is V24() real ext-real set

(() . p) + p is V24() real ext-real Element of REAL

].((() . p) - p),((() . p) + p).[ is V47() V48() V49() non left_end non right_end V68() open Element of K32(REAL)

{ b

() " ].((() . p) - p),((() . p) + p).[ is Element of K32( the carrier of (TOP-REAL 2))

Q is Element of K32( the carrier of (TOP-REAL 2))

Q is Element of K32( the carrier of (TOP-REAL 2))

{ |[b

p is Element of K32( the carrier of (TOP-REAL 2))

r is Element of K32( the carrier of (TOP-REAL 2))

((TOP-REAL 2),(),r) is Relation-like r -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | r) -defined REAL -valued Function-like V29( the carrier of ((TOP-REAL 2) | r)) V30( the carrier of ((TOP-REAL 2) | r), REAL ) complex-valued ext-real-valued real-valued ((TOP-REAL 2) | r) Element of K32(K33( the carrier of ((TOP-REAL 2) | r),REAL))

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

the carrier of ((TOP-REAL 2) | r) is set

K33( the carrier of ((TOP-REAL 2) | r),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of ((TOP-REAL 2) | r),REAL)) is non empty set

s is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

((TOP-REAL 2),(),r) . s is V24() real ext-real Element of REAL

s `1 is V24() real ext-real Element of REAL

() . s is V24() real ext-real Element of REAL

r is Element of K32( the carrier of (TOP-REAL 2))

((TOP-REAL 2),(),r) is Relation-like r -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | r) -defined REAL -valued Function-like V29( the carrier of ((TOP-REAL 2) | r)) V30( the carrier of ((TOP-REAL 2) | r), REAL ) complex-valued ext-real-valued real-valued ((TOP-REAL 2) | r) Element of K32(K33( the carrier of ((TOP-REAL 2) | r),REAL))

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

the carrier of ((TOP-REAL 2) | r) is set

K33( the carrier of ((TOP-REAL 2) | r),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K32(K33( the carrier of ((TOP-REAL 2) | r),REAL)) is non empty set

s is real-valued V71(2) V72() Element of the carrier of (TOP-REAL 2)

((TOP-REAL 2),(),r) . s is V24() real ext-real Element of REAL

s `2 is V24() real ext-real Element of REAL

() . s is V24() real ext-real Element of REAL

r is Element of K32( the carrier of (TOP-REAL 2))

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

((TOP-REAL 2),(),r) is Relation-like r -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | r) -defined REAL -valued Function-like V29( the carrier of ((TOP-REAL 2) | r)) V30( the carrier of ((TOP-REAL 2) | r), REAL ) complex-valued ext-real-valued real-valued ((