:: SPRECT_1 semantic presentation

REAL is non empty V32() V199() V200() V201() V205() non bounded_below non bounded_above V245() set

NAT is V199() V200() V201() V202() V203() V204() V205() bounded_below Element of bool REAL

bool REAL is non empty set

COMPLEX is non empty V32() V199() V205() set

omega is V199() V200() V201() V202() V203() V204() V205() bounded_below set

bool omega is non empty set

bool NAT is non empty set

1 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

2 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

[:1,1:] is non empty V23( RAT ) V23( INT ) V189() V190() V191() V192() set

RAT is non empty V32() V199() V200() V201() V202() V205() set

INT is non empty V32() V199() V200() V201() V202() V203() V205() set

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

[:[:1,1:],1:] is non empty V23( RAT ) V23( INT ) V189() V190() V191() V192() set

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

[:[:1,1:],REAL:] is non empty V189() V190() V191() set

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

[:REAL,REAL:] is non empty V189() V190() V191() set

[:[:REAL,REAL:],REAL:] is non empty V189() V190() V191() set

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

[:2,2:] is non empty V23( RAT ) V23( INT ) V189() V190() V191() V192() set

[:[:2,2:],REAL:] is non empty V189() V190() V191() set

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

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

TOP-REAL 2 is non empty TopSpace-like V114() V145() V146() V147() V148() V149() V150() V151() strict RLTopStruct

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

K257( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M15( the carrier of (TOP-REAL 2))

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

[: the carrier of (TOP-REAL 2),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of (TOP-REAL 2),REAL:] is non empty set

[:COMPLEX,COMPLEX:] is non empty V189() set

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

[:COMPLEX,REAL:] is non empty V189() V190() V191() set

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

ExtREAL is non empty V200() V245() set

{} is empty trivial Function-like functional FinSequence-membered V199() V200() V201() V202() V203() V204() V205() bounded_below V245() set

the empty trivial Function-like functional FinSequence-membered V199() V200() V201() V202() V203() V204() V205() bounded_below V245() set is empty trivial Function-like functional FinSequence-membered V199() V200() V201() V202() V203() V204() V205() bounded_below V245() set

3 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

Seg 1 is non empty V32() 1 -element V199() V200() V201() V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

{1} is non empty trivial V199() V200() V201() V202() V203() V204() left_end bounded_below set

Seg 2 is non empty V32() 2 -element V199() V200() V201() V202() V203() V204() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

{1,2} is non empty V199() V200() V201() V202() V203() V204() left_end bounded_below set

proj1 is V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) Function-like V44( the carrier of (TOP-REAL 2), REAL ) V189() V190() V191() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj2 is V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) Function-like V44( the carrier of (TOP-REAL 2), REAL ) V189() V190() V191() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

[:(Seg 2),(Seg 2):] is non empty V23( RAT ) V23( INT ) V189() V190() V191() V192() set

[1,1] is non empty set

{1,1} is non empty V199() V200() V201() V202() V203() V204() left_end bounded_below set

{{1,1},{1}} is non empty set

[1,2] is non empty set

{{1,2},{1}} is non empty set

[2,1] is non empty set

{2,1} is non empty V199() V200() V201() V202() V203() V204() left_end bounded_below set

{2} is non empty trivial V199() V200() V201() V202() V203() V204() left_end bounded_below set

{{2,1},{2}} is non empty set

[2,2] is non empty set

{2,2} is non empty V199() V200() V201() V202() V203() V204() left_end bounded_below set

{{2,2},{2}} is non empty set

0 is empty trivial ordinal natural V11() real ext-real non positive non negative Function-like functional FinSequence-membered V97() V188() V199() V200() V201() V202() V203() V204() V205() bounded_below V245() Element of NAT

4 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

5 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

<*0*> is non empty trivial V19() V22( NAT ) V23( REAL ) Function-like one-to-one constant V32() 1 -element FinSequence-like FinSubsequence-like V189() V190() V191() increasing V194() V195() V196() M16( REAL ,K258(1,REAL))

K258(1,REAL) is functional FinSequence-membered M15( REAL )

f is V19() V22( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

A1 is V19() V22( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

f ^ A1 is V19() V22( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

rng f is set

A2 is V19() V22( NAT ) Function-like constant V32() FinSequence-like FinSubsequence-like set

rng A2 is trivial set

rng A1 is set

f is set

A1 is set

<*f,A1*> is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like set

rng <*f,A1*> is set

<*f*> is non empty trivial V19() V22( NAT ) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like set

<*A1*> is non empty trivial V19() V22( NAT ) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like set

<*f*> ^ <*A1*> is non empty V19() V22( NAT ) Function-like V32() 1 + 1 -element FinSequence-like FinSubsequence-like set

1 + 1 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

rng (<*f*> ^ <*A1*>) is set

rng <*f*> is trivial set

rng <*A1*> is trivial set

(rng <*f*>) \/ (rng <*A1*>) is set

{A1} is non empty trivial set

(rng <*f*>) \/ {A1} is non empty set

{f} is non empty trivial set

{f} \/ {A1} is non empty set

{f,A1} is non empty set

A2 is V19() Function-like constant set

rng A2 is trivial set

f is set

A1 is set

A2 is set

<*f,A1,A2*> is non empty non trivial V19() V22( NAT ) Function-like V32() 3 -element FinSequence-like FinSubsequence-like set

rng <*f,A1,A2*> is set

<*f*> is non empty trivial V19() V22( NAT ) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like set

<*A1*> is non empty trivial V19() V22( NAT ) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like set

<*f*> ^ <*A1*> is non empty V19() V22( NAT ) Function-like V32() 1 + 1 -element FinSequence-like FinSubsequence-like set

1 + 1 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

<*A2*> is non empty trivial V19() V22( NAT ) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like set

(<*f*> ^ <*A1*>) ^ <*A2*> is non empty V19() V22( NAT ) Function-like V32() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set

(1 + 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

rng ((<*f*> ^ <*A1*>) ^ <*A2*>) is set

rng (<*f*> ^ <*A1*>) is set

rng <*A2*> is trivial set

(rng (<*f*> ^ <*A1*>)) \/ (rng <*A2*>) is set

{A2} is non empty trivial set

(rng (<*f*> ^ <*A1*>)) \/ {A2} is non empty set

rng <*f*> is trivial set

rng <*A1*> is trivial set

(rng <*f*>) \/ (rng <*A1*>) is set

((rng <*f*>) \/ (rng <*A1*>)) \/ {A2} is non empty set

{A1} is non empty trivial set

(rng <*f*>) \/ {A1} is non empty set

((rng <*f*>) \/ {A1}) \/ {A2} is non empty set

{f} is non empty trivial set

{f} \/ {A1} is non empty set

({f} \/ {A1}) \/ {A2} is non empty set

{f,A1} is non empty set

{f,A1} \/ {A2} is non empty set

{f,A1,A2} is non empty set

a1 is V19() Function-like constant set

rng a1 is trivial set

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

bool the carrier of f is non empty set

A1 is Element of bool the carrier of f

A2 is non empty Element of bool the carrier of f

f | A2 is non empty strict TopSpace-like SubSpace of f

the carrier of (f | A2) is non empty set

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

a1 is Element of bool the carrier of (f | A2)

{} (f | A2) is empty trivial proper Function-like functional FinSequence-membered closed compact V199() V200() V201() V202() V203() V204() V205() bounded_below V245() Element of bool the carrier of (f | A2)

f is TopStruct

the carrier of f is set

bool the carrier of f is non empty set

A2 is Element of bool the carrier of f

A1 is Element of bool the carrier of f

f | A2 is strict SubSpace of f

the carrier of (f | A2) is set

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

a1 is Element of bool the carrier of (f | A2)

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

bool the carrier of f is non empty set

A1 is non empty Element of bool the carrier of f

A2 is Element of bool the carrier of f

a1 is Element of bool the carrier of f

a2 is Element of bool the carrier of f

A2 \/ a1 is Element of bool the carrier of f

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

bool the carrier of f is non empty set

A1 is non empty Element of bool the carrier of f

A2 is Element of bool the carrier of f

a1 is Element of bool the carrier of f

a2 is Element of bool the carrier of f

c

A2 \/ a1 is Element of bool the carrier of f

a2 \/ c

{A2,a1} is non empty set

{a2,c

A2 is set

f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A1 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A2 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

<*f,A1,A2*> is non empty non trivial V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

L~ <*f,A1,A2*> is Element of bool the carrier of (TOP-REAL 2)

len <*f,A1,A2*> is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

{ (LSeg (<*f,A1,A2*>,b

union { (LSeg (<*f,A1,A2*>,b

LSeg (f,A1) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

LSeg (A1,A2) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg (f,A1)) \/ (LSeg (A1,A2)) is non empty Element of bool the carrier of (TOP-REAL 2)

<*f,A1*> is non empty non trivial V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

<*f,A1*> /. 2 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

<*A2*> is non empty trivial V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like special M16( the carrier of (TOP-REAL 2),K258(1, the carrier of (TOP-REAL 2)))

K258(1, the carrier of (TOP-REAL 2)) is functional FinSequence-membered M15( the carrier of (TOP-REAL 2))

<*A2*> /. 1 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

<*f,A1*> ^ <*A2*> is non empty V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() 2 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

2 + 1 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

len <*f,A1*> is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

L~ <*f,A1*> is Element of bool the carrier of (TOP-REAL 2)

{ (LSeg (<*f,A1*>,b

union { (LSeg (<*f,A1*>,b

(L~ <*f,A1*>) \/ (LSeg (A1,A2)) is non empty Element of bool the carrier of (TOP-REAL 2)

L~ <*A2*> is Element of bool the carrier of (TOP-REAL 2)

len <*A2*> is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

{ (LSeg (<*A2*>,b

union { (LSeg (<*A2*>,b

((L~ <*f,A1*>) \/ (LSeg (A1,A2))) \/ (L~ <*A2*>) is non empty Element of bool the carrier of (TOP-REAL 2)

((L~ <*f,A1*>) \/ (LSeg (A1,A2))) \/ {} is non empty set

f is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

TOP-REAL f is non empty TopSpace-like V114() V145() V146() V147() V148() V149() V150() V151() strict RLTopStruct

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

A1 is non empty non trivial V19() V22( NAT ) V23( the carrier of (TOP-REAL f)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL f)

L~ A1 is Element of bool the carrier of (TOP-REAL f)

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

len A1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

{ (LSeg (A1,b

union { (LSeg (A1,b

f is V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

L~ f is Element of bool the carrier of (TOP-REAL 2)

len f is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

{ (LSeg (f,b

union { (LSeg (f,b

A1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

A1 + 1 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

A2 is V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len A2 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

L~ A2 is Element of bool the carrier of (TOP-REAL 2)

{ (LSeg (A2,b

union { (LSeg (A2,b

a1 is V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

a2 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

<*a2*> is non empty trivial V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like special M16( the carrier of (TOP-REAL 2),K258(1, the carrier of (TOP-REAL 2)))

K258(1, the carrier of (TOP-REAL 2)) is functional FinSequence-membered M15( the carrier of (TOP-REAL 2))

a1 ^ <*a2*> is non empty V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len a1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

len <*a2*> is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

(len a1) + (len <*a2*>) is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

(len a1) + 1 is non empty ordinal natural V11() real ext-real positive non negative V97() V188() V199() V200() V201() V202() V203() V204() left_end bounded_below Element of NAT

L~ a1 is Element of bool the carrier of (TOP-REAL 2)

{ (LSeg (a1,b

union { (LSeg (a1,b

L~ <*a2*> is Element of bool the carrier of (TOP-REAL 2)

{ (LSeg (<*a2*>,b

union { (LSeg (<*a2*>,b

{} (TOP-REAL 2) is empty trivial proper Function-like functional FinSequence-membered closed compact V199() V200() V201() V202() V203() V204() V205() V211( TOP-REAL 2) circled bounded_below V245() Element of bool the carrier of (TOP-REAL 2)

a1 /. (len a1) is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

<*a2*> /. 1 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

LSeg ((a1 /. (len a1)),(<*a2*> /. 1)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(L~ a1) \/ (LSeg ((a1 /. (len a1)),(<*a2*> /. 1))) is non empty Element of bool the carrier of (TOP-REAL 2)

L~ <*a2*> is Element of bool the carrier of (TOP-REAL 2)

{ (LSeg (<*a2*>,b

union { (LSeg (<*a2*>,b

((L~ a1) \/ (LSeg ((a1 /. (len a1)),(<*a2*> /. 1)))) \/ (L~ <*a2*>) is non empty Element of bool the carrier of (TOP-REAL 2)

((L~ a1) \/ (LSeg ((a1 /. (len a1)),(<*a2*> /. 1)))) \/ {} is non empty set

A1 is V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len A1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT

L~ A1 is Element of bool the carrier of (TOP-REAL 2)

{ (LSeg (A1,b

union { (LSeg (A1,b

{} (TOP-REAL 2) is empty trivial proper Function-like functional FinSequence-membered closed compact V199() V200() V201() V202() V203() V204() V205() V211( TOP-REAL 2) circled bounded_below V245() Element of bool the carrier of (TOP-REAL 2)

f is Element of bool the carrier of (TOP-REAL 2)

A1 is Element of bool the carrier of (TOP-REAL 2)

A2 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A2 `2 is V11() real ext-real Element of REAL

a1 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

a1 `2 is V11() real ext-real Element of REAL

f is Element of bool the carrier of (TOP-REAL 2)

A1 is Element of bool the carrier of (TOP-REAL 2)

A2 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A2 `1 is V11() real ext-real Element of REAL

a1 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

a1 `1 is V11() real ext-real Element of REAL

R^2-unit_square is non empty non trivial compact special_polygonal Element of bool the carrier of (TOP-REAL 2)

|[0,0]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

|[0,1]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg (|[0,0]|,|[0,1]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

|[1,1]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg (|[0,1]|,|[1,1]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is non empty Element of bool the carrier of (TOP-REAL 2)

|[1,0]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg (|[1,1]|,|[1,0]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

LSeg (|[1,0]|,|[0,0]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)) is non empty Element of bool the carrier of (TOP-REAL 2)

((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is non empty Element of bool the carrier of (TOP-REAL 2)

|[0,1]| `2 is V11() real ext-real Element of REAL

|[0,0]| `2 is V11() real ext-real Element of REAL

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

|[0,1]| `1 is V11() real ext-real Element of REAL

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

N-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

N-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

lower_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

N-bound f is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

upper_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(W-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

E-bound f is V11() real ext-real Element of REAL

upper_bound (proj1 | f) is V11() real ext-real Element of REAL

upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((NW-corner f),(NE-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((NW-corner f),(NE-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (N-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | (N-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (N-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (N-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (N-most f))) V267( the carrier of ((TOP-REAL 2) | (N-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (N-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (N-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (N-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (N-most f)),REAL:] is non empty set

lower_bound (proj1 | (N-most f)) is V11() real ext-real Element of REAL

(proj1 | (N-most f)) .: the carrier of ((TOP-REAL 2) | (N-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | (N-most f)) .: the carrier of ((TOP-REAL 2) | (N-most f))) is V11() real ext-real Element of REAL

|[(lower_bound (proj1 | (N-most f))),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

N-max f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

upper_bound (proj1 | (N-most f)) is V11() real ext-real Element of REAL

upper_bound ((proj1 | (N-most f)) .: the carrier of ((TOP-REAL 2) | (N-most f))) is V11() real ext-real Element of REAL

|[(upper_bound (proj1 | (N-most f))),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

S-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

S-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

lower_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

S-bound f is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

lower_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(W-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

E-bound f is V11() real ext-real Element of REAL

upper_bound (proj1 | f) is V11() real ext-real Element of REAL

upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner f),(SE-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((SW-corner f),(SE-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (S-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | (S-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (S-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (S-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (S-most f))) V267( the carrier of ((TOP-REAL 2) | (S-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (S-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (S-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (S-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (S-most f)),REAL:] is non empty set

lower_bound (proj1 | (S-most f)) is V11() real ext-real Element of REAL

(proj1 | (S-most f)) .: the carrier of ((TOP-REAL 2) | (S-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | (S-most f)) .: the carrier of ((TOP-REAL 2) | (S-most f))) is V11() real ext-real Element of REAL

|[(lower_bound (proj1 | (S-most f))),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

S-max f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

upper_bound (proj1 | (S-most f)) is V11() real ext-real Element of REAL

upper_bound ((proj1 | (S-most f)) .: the carrier of ((TOP-REAL 2) | (S-most f))) is V11() real ext-real Element of REAL

|[(upper_bound (proj1 | (S-most f))),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

W-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

lower_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

W-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

S-bound f is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

lower_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(W-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

N-bound f is V11() real ext-real Element of REAL

upper_bound (proj2 | f) is V11() real ext-real Element of REAL

upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(W-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner f),(NW-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((SW-corner f),(NW-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (W-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (W-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (W-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (W-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (W-most f))) V267( the carrier of ((TOP-REAL 2) | (W-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (W-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (W-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (W-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (W-most f)),REAL:] is non empty set

lower_bound (proj2 | (W-most f)) is V11() real ext-real Element of REAL

(proj2 | (W-most f)) .: the carrier of ((TOP-REAL 2) | (W-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | (W-most f)) .: the carrier of ((TOP-REAL 2) | (W-most f))) is V11() real ext-real Element of REAL

|[(W-bound f),(lower_bound (proj2 | (W-most f)))]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

W-max f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

upper_bound (proj2 | (W-most f)) is V11() real ext-real Element of REAL

upper_bound ((proj2 | (W-most f)) .: the carrier of ((TOP-REAL 2) | (W-most f))) is V11() real ext-real Element of REAL

|[(W-bound f),(upper_bound (proj2 | (W-most f)))]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

E-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

E-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

upper_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

E-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

S-bound f is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

lower_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

N-bound f is V11() real ext-real Element of REAL

upper_bound (proj2 | f) is V11() real ext-real Element of REAL

upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner f),(NE-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((SE-corner f),(NE-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (E-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (E-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (E-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (E-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (E-most f))) V267( the carrier of ((TOP-REAL 2) | (E-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (E-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (E-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (E-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (E-most f)),REAL:] is non empty set

lower_bound (proj2 | (E-most f)) is V11() real ext-real Element of REAL

(proj2 | (E-most f)) .: the carrier of ((TOP-REAL 2) | (E-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | (E-most f)) .: the carrier of ((TOP-REAL 2) | (E-most f))) is V11() real ext-real Element of REAL

|[(E-bound f),(lower_bound (proj2 | (E-most f)))]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

E-max f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

upper_bound (proj2 | (E-most f)) is V11() real ext-real Element of REAL

upper_bound ((proj2 | (E-most f)) .: the carrier of ((TOP-REAL 2) | (E-most f))) is V11() real ext-real Element of REAL

|[(E-bound f),(upper_bound (proj2 | (E-most f)))]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

lower_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

E-bound f is V11() real ext-real Element of REAL

upper_bound (proj1 | f) is V11() real ext-real Element of REAL

upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

E-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

E-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

S-bound f is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

lower_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

N-bound f is V11() real ext-real Element of REAL

upper_bound (proj2 | f) is V11() real ext-real Element of REAL

upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner f),(NE-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((SE-corner f),(NE-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (E-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (E-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (E-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (E-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (E-most f))) V267( the carrier of ((TOP-REAL 2) | (E-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (E-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (E-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (E-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (E-most f)),REAL:] is non empty set

lower_bound (proj2 | (E-most f)) is V11() real ext-real Element of REAL

(proj2 | (E-most f)) .: the carrier of ((TOP-REAL 2) | (E-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | (E-most f)) .: the carrier of ((TOP-REAL 2) | (E-most f))) is V11() real ext-real Element of REAL

|[(E-bound f),(lower_bound (proj2 | (E-most f)))]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

W-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

|[(W-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

|[(W-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner f),(NW-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((SW-corner f),(NW-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (W-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (W-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (W-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (W-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (W-most f))) V267( the carrier of ((TOP-REAL 2) | (W-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (W-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (W-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (W-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (W-most f)),REAL:] is non empty set

lower_bound (proj2 | (W-most f)) is V11() real ext-real Element of REAL

(proj2 | (W-most f)) .: the carrier of ((TOP-REAL 2) | (W-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | (W-most f)) .: the carrier of ((TOP-REAL 2) | (W-most f))) is V11() real ext-real Element of REAL

|[(W-bound f),(lower_bound (proj2 | (W-most f)))]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

(W-min f) `1 is V11() real ext-real Element of REAL

(E-min f) `1 is V11() real ext-real Element of REAL

A1 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A1 `1 is V11() real ext-real Element of REAL

A2 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A2 `1 is V11() real ext-real Element of REAL

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

S-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

lower_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

N-bound f is V11() real ext-real Element of REAL

upper_bound (proj2 | f) is V11() real ext-real Element of REAL

upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

N-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

N-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

lower_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(W-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

E-bound f is V11() real ext-real Element of REAL

upper_bound (proj1 | f) is V11() real ext-real Element of REAL

upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((NW-corner f),(NE-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((NW-corner f),(NE-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (N-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | (N-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (N-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (N-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (N-most f))) V267( the carrier of ((TOP-REAL 2) | (N-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (N-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (N-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (N-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (N-most f)),REAL:] is non empty set

lower_bound (proj1 | (N-most f)) is V11() real ext-real Element of REAL

(proj1 | (N-most f)) .: the carrier of ((TOP-REAL 2) | (N-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | (N-most f)) .: the carrier of ((TOP-REAL 2) | (N-most f))) is V11() real ext-real Element of REAL

|[(lower_bound (proj1 | (N-most f))),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

S-min f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

S-most f is non empty compact Element of bool the carrier of (TOP-REAL 2)

SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

|[(W-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

|[(E-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner f),(SE-corner f)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

(LSeg ((SW-corner f),(SE-corner f))) /\ f is compact Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (S-most f) is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | (S-most f) is V19() V22( the carrier of ((TOP-REAL 2) | (S-most f))) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | (S-most f)), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | (S-most f))) V267( the carrier of ((TOP-REAL 2) | (S-most f))) V268() Element of bool [: the carrier of ((TOP-REAL 2) | (S-most f)),REAL:]

the carrier of ((TOP-REAL 2) | (S-most f)) is non empty set

[: the carrier of ((TOP-REAL 2) | (S-most f)),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | (S-most f)),REAL:] is non empty set

lower_bound (proj1 | (S-most f)) is V11() real ext-real Element of REAL

(proj1 | (S-most f)) .: the carrier of ((TOP-REAL 2) | (S-most f)) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | (S-most f)) .: the carrier of ((TOP-REAL 2) | (S-most f))) is V11() real ext-real Element of REAL

|[(lower_bound (proj1 | (S-most f))),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

(S-min f) `2 is V11() real ext-real Element of REAL

(N-min f) `2 is V11() real ext-real Element of REAL

A1 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A1 `2 is V11() real ext-real Element of REAL

A2 is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

A2 `2 is V11() real ext-real Element of REAL

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

lower_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

N-bound f is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

upper_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

upper_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(W-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

E-bound f is V11() real ext-real Element of REAL

upper_bound (proj1 | f) is V11() real ext-real Element of REAL

upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2

proj1 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

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

[: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty V189() V190() V191() set

bool [: the carrier of ((TOP-REAL 2) | f),REAL:] is non empty set

lower_bound (proj1 | f) is V11() real ext-real Element of REAL

(proj1 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

S-bound f is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of ((TOP-REAL 2) | f)) V23( REAL ) Function-like V44( the carrier of ((TOP-REAL 2) | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of ((TOP-REAL 2) | f)) V267( the carrier of ((TOP-REAL 2) | f)) V268() Element of bool [: the carrier of ((TOP-REAL 2) | f),REAL:]

lower_bound (proj2 | f) is V11() real ext-real Element of REAL

(proj2 | f) .: the carrier of ((TOP-REAL 2) | f) is V199() V200() V201() Element of bool REAL

lower_bound ((proj2 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(W-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

E-bound f is V11() real ext-real Element of REAL

upper_bound (proj1 | f) is V11() real ext-real Element of REAL

upper_bound ((proj1 | f) .: the carrier of ((TOP-REAL 2) | f)) is V11() real ext-real Element of REAL

|[(E-bound f),(S-bound f)]| is non empty non trivial V19() V22( NAT ) Function-like V32() 2 -element FinSequence-like FinSubsequence-like V189() V190() V191() Element of the carrier of (TOP-REAL 2)

f is non empty compact Element of bool the carrier of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of (TOP-REAL 2)

W-bound f is V11() real ext-real Element of REAL

(TOP-REAL 2) | f is non empty strict TopSpace-like compact pseudocompact SubSpace of