:: 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
is non empty V189() V190() V191() set
is non empty V189() V190() V191() set
bool 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 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 () is non empty set
K257( the carrier of ()) is non empty functional FinSequence-membered M15( the carrier of ())
bool the carrier of () is non empty set
[: the carrier of (),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (),REAL:] is non empty set
is non empty V189() set
bool is non empty set
is non empty V189() V190() V191() set
bool is non empty set
ExtREAL is non empty V200() 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 ()) V23( REAL ) Function-like V44( the carrier of (), REAL ) V189() V190() V191() continuous Element of bool [: the carrier of (),REAL:]
proj2 is V19() V22( the carrier of ()) V23( REAL ) Function-like V44( the carrier of (), REAL ) V189() V190() V191() continuous Element of bool [: the carrier of (),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

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

rng f is 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

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 <*A1*>) is set
{A1} is non empty trivial set
() \/ {A1} is non empty set
{f} is non empty trivial set
{f} \/ {A1} is non empty set
{f,A1} is non empty 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

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

(<*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 (<*f*> ^ <*A1*>)) \/ (rng <*A2*>) is set
{A2} is non empty trivial set
(rng (<*f*> ^ <*A1*>)) \/ {A2} is non empty set

() \/ (rng <*A1*>) is set
(() \/ (rng <*A1*>)) \/ {A2} is non empty set
{A1} is non empty trivial set
() \/ {A1} is non empty set
(() \/ {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

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
c6 is Element of bool the carrier of f
A2 \/ a1 is Element of bool the carrier of f
a2 \/ c6 is Element of bool the carrier of f
{A2,a1} is non empty set
{a2,c6} is non empty set
A2 is set
f is 2 -element FinSequence-like V191() Element of the carrier of ()
A1 is 2 -element FinSequence-like V191() Element of the carrier of ()
A2 is 2 -element FinSequence-like V191() Element of the carrier of ()
<*f,A1,A2*> is non empty non trivial V19() V22( NAT ) V23( the carrier of ()) Function-like V32() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
L~ <*f,A1,A2*> is Element of bool the carrier of ()
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*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*f,A1,A2*> ) } is set
union { (LSeg (<*f,A1,A2*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*f,A1,A2*> ) } is set
LSeg (f,A1) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * f) + (b1 * A1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (A1,A2) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * A1) + (b1 * A2)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg (f,A1)) \/ (LSeg (A1,A2)) is non empty Element of bool the carrier of ()
<*f,A1*> is non empty non trivial V19() V22( NAT ) V23( the carrier of ()) Function-like V32() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
<*f,A1*> /. 2 is 2 -element FinSequence-like V191() Element of the carrier of ()
<*A2*> is non empty trivial V19() V22( NAT ) V23( the carrier of ()) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like special M16( the carrier of (),K258(1, the carrier of ()))
K258(1, the carrier of ()) is functional FinSequence-membered M15( the carrier of ())
<*A2*> /. 1 is 2 -element FinSequence-like V191() Element of the carrier of ()
<*f,A1*> ^ <*A2*> is non empty V19() V22( NAT ) V23( the carrier of ()) Function-like V32() 2 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
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 ()
{ (LSeg (<*f,A1*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*f,A1*> ) } is set
union { (LSeg (<*f,A1*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*f,A1*> ) } is set
(L~ <*f,A1*>) \/ (LSeg (A1,A2)) is non empty Element of bool the carrier of ()
L~ <*A2*> is Element of bool the carrier of ()
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*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*A2*> ) } is set
union { (LSeg (<*A2*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*A2*> ) } is set
((L~ <*f,A1*>) \/ (LSeg (A1,A2))) \/ (L~ <*A2*>) is non empty Element of bool the carrier of ()
((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 () is non empty set
A1 is non empty non trivial V19() V22( NAT ) V23( the carrier of ()) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
L~ A1 is Element of bool the carrier of ()
bool the carrier of () 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,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len A1 ) } is set
union { (LSeg (A1,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len A1 ) } is set
f is V19() V22( NAT ) V23( the carrier of ()) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
L~ f is Element of bool the carrier of ()
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,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len f ) } is set
union { (LSeg (f,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len f ) } is set
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 ()) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
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 ()
{ (LSeg (A2,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len A2 ) } is set
union { (LSeg (A2,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len A2 ) } is set
a1 is V19() V22( NAT ) V23( the carrier of ()) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
a2 is 2 -element FinSequence-like V191() Element of the carrier of ()
<*a2*> is non empty trivial V19() V22( NAT ) V23( the carrier of ()) Function-like constant V32() 1 -element FinSequence-like FinSubsequence-like special M16( the carrier of (),K258(1, the carrier of ()))
K258(1, the carrier of ()) is functional FinSequence-membered M15( the carrier of ())
a1 ^ <*a2*> is non empty V19() V22( NAT ) V23( the carrier of ()) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
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 ()
{ (LSeg (a1,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len a1 ) } is set
union { (LSeg (a1,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len a1 ) } is set
L~ <*a2*> is Element of bool the carrier of ()
{ (LSeg (<*a2*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*a2*> ) } is set
union { (LSeg (<*a2*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*a2*> ) } is set

a1 /. (len a1) is 2 -element FinSequence-like V191() Element of the carrier of ()
<*a2*> /. 1 is 2 -element FinSequence-like V191() Element of the carrier of ()
LSeg ((a1 /. (len a1)),(<*a2*> /. 1)) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * (a1 /. (len a1))) + (b1 * (<*a2*> /. 1))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(L~ a1) \/ (LSeg ((a1 /. (len a1)),(<*a2*> /. 1))) is non empty Element of bool the carrier of ()
L~ <*a2*> is Element of bool the carrier of ()
{ (LSeg (<*a2*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*a2*> ) } is set
union { (LSeg (<*a2*>,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*a2*> ) } is set
((L~ a1) \/ (LSeg ((a1 /. (len a1)),(<*a2*> /. 1)))) \/ (L~ <*a2*>) is non empty Element of bool the carrier of ()
((L~ a1) \/ (LSeg ((a1 /. (len a1)),(<*a2*> /. 1)))) \/ {} is non empty set
A1 is V19() V22( NAT ) V23( the carrier of ()) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
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 ()
{ (LSeg (A1,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len A1 ) } is set
union { (LSeg (A1,b1)) where b1 is ordinal natural V11() real ext-real non negative V97() V188() V199() V200() V201() V202() V203() V204() bounded_below Element of NAT : ( 1 <= b1 & b1 + 1 <= len A1 ) } is set

f is Element of bool the carrier of ()
A1 is Element of bool the carrier of ()
A2 is 2 -element FinSequence-like V191() Element of the carrier of ()
A2 `2 is V11() real ext-real Element of REAL
a1 is 2 -element FinSequence-like V191() Element of the carrier of ()
a1 `2 is V11() real ext-real Element of REAL
f is Element of bool the carrier of ()
A1 is Element of bool the carrier of ()
A2 is 2 -element FinSequence-like V191() Element of the carrier of ()
A2 `1 is V11() real ext-real Element of REAL
a1 is 2 -element FinSequence-like V191() Element of the carrier of ()
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 ()
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 ()
|[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 ()
LSeg (,|[0,1]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ) + (b1 * |[0,1]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[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 ()
LSeg (|[0,1]|,|[1,1]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * |[0,1]|) + (b1 * |[1,1]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg (,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is non empty Element of bool the carrier of ()
|[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 ()
LSeg (|[1,1]|,|[1,0]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * |[1,1]|) + (b1 * |[1,0]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (|[1,0]|,) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * |[1,0]|) + (b1 * )) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,)) is non empty Element of bool the carrier of ()
((LSeg (,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,))) is non empty Element of bool the carrier of ()

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

f is non empty compact Element of bool the carrier of ()
N-min f is 2 -element FinSequence-like V191() Element of the carrier of ()
N-most f is non empty compact Element of bool the carrier of ()
NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
upper_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj1 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj1 | ()) is V11() real ext-real Element of REAL
(proj1 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj1 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(lower_bound (proj1 | ())),()]| 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 ()
N-max f is 2 -element FinSequence-like V191() Element of the carrier of ()
upper_bound (proj1 | ()) is V11() real ext-real Element of REAL
upper_bound ((proj1 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(upper_bound (proj1 | ())),()]| 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 ()
f is non empty compact Element of bool the carrier of ()
S-min f is 2 -element FinSequence-like V191() Element of the carrier of ()
S-most f is non empty compact Element of bool the carrier of ()
SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj1 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj1 | ()) is V11() real ext-real Element of REAL
(proj1 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj1 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(lower_bound (proj1 | ())),()]| 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 ()
S-max f is 2 -element FinSequence-like V191() Element of the carrier of ()
upper_bound (proj1 | ()) is V11() real ext-real Element of REAL
upper_bound ((proj1 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(upper_bound (proj1 | ())),()]| 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 ()
f is non empty compact Element of bool the carrier of ()
W-min f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
W-most f is non empty compact Element of bool the carrier of ()
SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj2 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(lower_bound (proj2 | ()))]| 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 ()
W-max f is 2 -element FinSequence-like V191() Element of the carrier of ()
upper_bound (proj2 | ()) is V11() real ext-real Element of REAL
upper_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(upper_bound (proj2 | ()))]| 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 ()
f is non empty compact Element of bool the carrier of ()
E-min f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
upper_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
E-most f is non empty compact Element of bool the carrier of ()
SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj2 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(lower_bound (proj2 | ()))]| 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 ()
E-max f is 2 -element FinSequence-like V191() Element of the carrier of ()
upper_bound (proj2 | ()) is V11() real ext-real Element of REAL
upper_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(upper_bound (proj2 | ()))]| 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 ()
f is non empty compact Element of bool the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
E-min f is 2 -element FinSequence-like V191() Element of the carrier of ()
E-most f is non empty compact Element of bool the carrier of ()
SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj2 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(lower_bound (proj2 | ()))]| 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 ()
W-min f is 2 -element FinSequence-like V191() Element of the carrier of ()
W-most f is non empty compact Element of bool the carrier of ()
SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()
|[(),()]| 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 ()
NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj2 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(lower_bound (proj2 | ()))]| 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 ()
() `1 is V11() real ext-real Element of REAL
() `1 is V11() real ext-real Element of REAL
A1 is 2 -element FinSequence-like V191() Element of the carrier of ()
A1 `1 is V11() real ext-real Element of REAL
A2 is 2 -element FinSequence-like V191() Element of the carrier of ()
A2 `1 is V11() real ext-real Element of REAL
f is non empty compact Element of bool the carrier of ()

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
N-min f is 2 -element FinSequence-like V191() Element of the carrier of ()
N-most f is non empty compact Element of bool the carrier of ()
NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj1 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj1 | ()) is V11() real ext-real Element of REAL
(proj1 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj1 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(lower_bound (proj1 | ())),()]| 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 ()
S-min f is 2 -element FinSequence-like V191() Element of the carrier of ()
S-most f is non empty compact Element of bool the carrier of ()
SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()
|[(),()]| 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 ()
SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()
|[(),()]| 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 ()
LSeg ((),()) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of ()
{ (((1 - b1) * ()) + (b1 * ())) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((),())) /\ f is compact Element of bool the carrier of ()
() | () is non empty strict TopSpace-like compact pseudocompact SubSpace of TOP-REAL 2
proj1 | () is V19() V22( the carrier of (() | ())) V23( REAL ) Function-like V44( the carrier of (() | ()), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | ())) V267( the carrier of (() | ())) V268() Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj1 | ()) is V11() real ext-real Element of REAL
(proj1 | ()) .: the carrier of (() | ()) is V199() V200() V201() Element of bool REAL
lower_bound ((proj1 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(lower_bound (proj1 | ())),()]| 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 ()
() `2 is V11() real ext-real Element of REAL
() `2 is V11() real ext-real Element of REAL
A1 is 2 -element FinSequence-like V191() Element of the carrier of ()
A1 `2 is V11() real ext-real Element of REAL
A2 is 2 -element FinSequence-like V191() Element of the carrier of ()
A2 `2 is V11() real ext-real Element of REAL
f is non empty compact Element of bool the carrier of ()
NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
upper_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
NE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
f is non empty compact Element of bool the carrier of ()
SW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

proj1 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
the carrier of (() | f) is non empty set
[: the carrier of (() | f),REAL:] is non empty V189() V190() V191() set
bool [: the carrier of (() | f),REAL:] is non empty set
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL

proj2 | f is V19() V22( the carrier of (() | f)) V23( REAL ) Function-like V44( the carrier of (() | f), REAL ) V189() V190() V191() continuous V260() V261() V266( the carrier of (() | f)) V267( the carrier of (() | f)) V268() Element of bool [: the carrier of (() | f),REAL:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | f) is V199() V200() V201() Element of bool REAL
lower_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
SE-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | f)) is V11() real ext-real Element of REAL
|[(),()]| 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 ()
f is non empty compact Element of bool the carrier of ()
NW-corner f is 2 -element FinSequence-like V191() Element of the carrier of ()