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
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 (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*>,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 (TOP-REAL 2)
{ (((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 (TOP-REAL 2)
{ (((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 (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*>,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 (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*>,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 (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,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 (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,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 (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,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 (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,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 (TOP-REAL 2)
{ (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
{} (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 - 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 (TOP-REAL 2)
L~ <*a2*> is Element of bool the carrier of (TOP-REAL 2)
{ (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 (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,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
{} (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 - b1) * |[0,0]|) + (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 (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 - b1) * |[0,1]|) + (b1 * |[1,1]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - 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]|,|[0,0]|) is non empty compact V258( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * |[1,0]|) + (b1 * |[0,0]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (NW-corner f)) + (b1 * (NE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner f)) + (b1 * (SE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner f)) + (b1 * (NW-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner f)) + (b1 * (NE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner f)) + (b1 * (NE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner f)) + (b1 * (NW-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (NW-corner f)) + (b1 * (NE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner f)) + (b1 * (SE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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