:: JORDAN1G semantic presentation

REAL is V200() V201() V202() V206() set
NAT is non empty non trivial V6() V26() cardinal limit_cardinal V200() V201() V202() V203() V204() V205() V206() Element of bool REAL
bool REAL is set
NAT is non empty non trivial V6() V26() cardinal limit_cardinal V200() V201() V202() V203() V204() V205() V206() set
bool NAT is non empty non trivial V26() set
bool NAT is non empty non trivial V26() set
COMPLEX is V200() V206() set
1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
2 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
K356() is TopStruct
the U1 of K356() is set
[:1,1:] is V13() V26() set
bool [:1,1:] is V26() V30() set
[:[:1,1:],1:] is V13() V26() set
bool [:[:1,1:],1:] is V26() V30() set
[:[:1,1:],REAL:] is V13() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is V13() set
[:[:REAL,REAL:],REAL:] is V13() set
bool [:[:REAL,REAL:],REAL:] is set
[:2,2:] is V13() V26() set
[:[:2,2:],REAL:] is V13() set
bool [:[:2,2:],REAL:] is set
K384() is V171() L15()
K394() is TopSpace-like T_0 T_1 T_2 TopStruct
RAT is V200() V201() V202() V203() V206() set
INT is V200() V201() V202() V203() V204() V206() set
bool [:REAL,REAL:] is set
TOP-REAL 2 is non empty non trivial TopSpace-like V104() V135() V136() V137() V138() V139() V140() V141() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty non trivial set
[: the U1 of (TOP-REAL 2),REAL:] is V13() set
bool [: the U1 of (TOP-REAL 2),REAL:] is set
bool the U1 of (TOP-REAL 2) is set
K238( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the U1 of (TOP-REAL 2))
{} is empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V200() V201() V202() V203() V204() V205() V206() set
the empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V200() V201() V202() V203() V204() V205() V206() set is empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V200() V201() V202() V203() V204() V205() V206() set
3 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
4 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
0 is empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V37() ext-real non positive non negative V199() V200() V201() V202() V203() V204() V205() V206() Element of NAT
Seg 1 is non empty trivial V26() 1 -element V200() V201() V202() V203() V204() V205() Element of bool NAT
{1} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set
Seg 2 is non empty V26() 2 -element V200() V201() V202() V203() V204() V205() Element of bool NAT
{1,2} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set
K396() is TopSpace-like SubSpace of K394()
the U1 of K396() is set
C is trivial V13() V16( NAT ) Function-like constant V26() FinSequence-like FinSubsequence-like set
n is set
{n} is non empty trivial V26() 1 -element set
i is set
j is set
[i,j] is non empty set
{i,j} is non empty V26() set
{i} is non empty trivial V26() 1 -element set
{{i,j},{i}} is non empty V26() V30() set
dom C is trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT
<*j*> is non empty trivial V13() V16( NAT ) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like set
C is non empty non trivial V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
Rev C is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n is set
<*n*> is non empty trivial V13() V16( NAT ) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like set
n is set
<*n*> is non empty trivial V13() V16( NAT ) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like set
Rev <*n*> is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
C is non empty set
K238(C) is non empty functional FinSequence-membered M11(C)
n is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
i is V13() V16( NAT ) V17(K238(C)) Function-like V26() FinSequence-like FinSubsequence-like tabular FinSequence of K238(C)
j is set
n -: j is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
j .. n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
n | (j .. n) is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
C is non empty set
K238(C) is non empty functional FinSequence-membered M11(C)
n is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
rng n is V26() set
i is V13() V16( NAT ) V17(K238(C)) Function-like V26() FinSequence-like FinSubsequence-like tabular FinSequence of K238(C)
j is Element of C
n :- j is non empty V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
j .. n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
Emax is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
Emax + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
n /^ Emax is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
n is non empty connected compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Upper_Seq (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
Gauge (n,C) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))
Cage (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty closed connected V222() compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (n,C))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]
the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is set
K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]
K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:]
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set
[: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is set
K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:]
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set
[: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is set
K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (n,C)))),K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) -: (E-max (L~ (Cage (n,C)))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded FinSequence of the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
n is non empty connected compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Lower_Seq (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
Gauge (n,C) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))
Cage (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty closed connected V222() compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (n,C))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]
the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is set
K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]
K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:]
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set
[: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is set
K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (n,C)))),K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:]
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set
[: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is set
K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (n,C)))),K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
rng (Cage (n,C)) is non empty non trivial V26() set
rng (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is non empty non trivial V26() set
(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) :- (E-max (L~ (Cage (n,C)))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C is non empty connected compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
Upper_Seq (C,n) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
Gauge (C,n) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))
Lower_Seq (C,n) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
Gauge (C,n) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))
C is V13() V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular Y_equal-in-column Y_increasing-in-line FinSequence of K238( the U1 of (TOP-REAL 2))
Indices C is set
n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
j is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
[n,j] is non empty set
{n,j} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set
{n} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set
{{n,j},{n}} is non empty V26() V30() set
i is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
Emax is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
[i,Emax] is non empty set
{i,Emax} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set
{i} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set
{{i,Emax},{i}} is non empty V26() V30() set
C * (n,j) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (n,j)) `2 is V11() V12() ext-real Element of REAL
C * (i,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (i,Emax)) `2 is V11() V12() ext-real Element of REAL
width C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
len C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C * (n,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (n,Emax)) `2 is V11() V12() ext-real Element of REAL
C * (1,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (1,Emax)) `2 is V11() V12() ext-real Element of REAL
C is V13() V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))
Indices C is set
n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
j is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
[n,j] is non empty set
{n,j} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set
{n} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set
{{n,j},{n}} is non empty V26() V30() set
i is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
Emax is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
[i,Emax] is non empty set
{i,Emax} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set
{i} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set
{{i,Emax},{i}} is non empty V26() V30() set
C * (n,j) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (n,j)) `1 is V11() V12() ext-real Element of REAL
C * (i,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (i,Emax)) `1 is V11() V12() ext-real Element of REAL
len C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
width C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C * (n,1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (n,1)) `1 is V11() V12() ext-real Element of REAL
C * (n,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(C * (n,Emax)) `1 is V11() V12() ext-real Element of REAL
C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)
C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)
N-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)
NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ C) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set
K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
N-bound (L~ C) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
E-bound (L~ C) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ C)),(NE-corner (L~ C))) is closed closed connected compact compact horizontal Element of bool the U1 of (TOP-REAL 2)
(LSeg ((NW-corner (L~ C)),(NE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (N-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (N-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:]
the U1 of ((TOP-REAL 2) | (N-most (L~ C))) is set
[: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is set
K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
(N-max (L~ C)) `1 is V11() V12() ext-real Element of REAL
(N-min (L~ C)) `1 is V11() V12() ext-real Element of REAL
(N-min (L~ C)) .. C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(N-min (L~ C)) `2 is V11() V12() ext-real Element of REAL
rng C is non empty V26() set
dom C is non empty non trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT
C . ((N-min (L~ C)) .. C) is set
C /. ((N-min (L~ C)) .. C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(N-max (L~ C)) `2 is V11() V12() ext-real Element of REAL
(N-max (L~ C)) `2 is V11() V12() ext-real Element of REAL
((N-min (L~ C)) .. C) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(((N-min (L~ C)) .. C) -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (((N-min (L~ C)) .. C) -' 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg (C,(((N-min (L~ C)) .. C) -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)
((N-min (L~ C)) .. C) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (((N-min (L~ C)) .. C) + 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg (C,((N-min (L~ C)) .. C)) is closed Element of bool the U1 of (TOP-REAL 2)
(C /. (((N-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((N-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((N-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((N-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL
LSeg ((C /. ((N-min (L~ C)) .. C)),(C /. (((N-min (L~ C)) .. C) + 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
LSeg ((C /. ((N-min (L~ C)) .. C)),(C /. (((N-min (L~ C)) .. C) -' 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg (C,(((N-min (L~ C)) .. C) -' 1))) /\ (LSeg (C,((N-min (L~ C)) .. C))) is Element of bool the U1 of (TOP-REAL 2)
((((N-min (L~ C)) .. C) -' 1) + 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(((N-min (L~ C)) .. C) -' 1) + (1 + 1) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
{(C /. ((N-min (L~ C)) .. C))} is non empty trivial V26() 1 -element set
(C /. (((N-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((N-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((N-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((N-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL
C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)
C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)
N-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)
NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ C) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set
K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
N-bound (L~ C) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
E-bound (L~ C) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ C)),(NE-corner (L~ C))) is closed closed connected compact compact horizontal Element of bool the U1 of (TOP-REAL 2)
(LSeg ((NW-corner (L~ C)),(NE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (N-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (N-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:]
the U1 of ((TOP-REAL 2) | (N-most (L~ C))) is set
[: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is set
K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
(N-max (L~ C)) `1 is V11() V12() ext-real Element of REAL
(N-min (L~ C)) `1 is V11() V12() ext-real Element of REAL
C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)
C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)
S-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ C) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set
K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
S-bound (L~ C) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
SE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
E-bound (L~ C) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ C)),(SE-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ C)),(SE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (S-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (S-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (S-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:]
the U1 of ((TOP-REAL 2) | (S-most (L~ C))) is set
[: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is set
K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
(S-max (L~ C)) `1 is V11() V12() ext-real Element of REAL
(S-min (L~ C)) `1 is V11() V12() ext-real Element of REAL
(S-min (L~ C)) .. C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(S-min (L~ C)) `2 is V11() V12() ext-real Element of REAL
rng C is non empty V26() set
dom C is non empty non trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT
C . ((S-min (L~ C)) .. C) is set
C /. ((S-min (L~ C)) .. C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(S-max (L~ C)) `2 is V11() V12() ext-real Element of REAL
(S-max (L~ C)) `2 is V11() V12() ext-real Element of REAL
((S-min (L~ C)) .. C) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(((S-min (L~ C)) .. C) -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (((S-min (L~ C)) .. C) -' 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg (C,(((S-min (L~ C)) .. C) -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)
((S-min (L~ C)) .. C) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (((S-min (L~ C)) .. C) + 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg (C,((S-min (L~ C)) .. C)) is closed Element of bool the U1 of (TOP-REAL 2)
(C /. (((S-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((S-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((S-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((S-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL
LSeg ((C /. ((S-min (L~ C)) .. C)),(C /. (((S-min (L~ C)) .. C) + 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
LSeg ((C /. ((S-min (L~ C)) .. C)),(C /. (((S-min (L~ C)) .. C) -' 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg (C,(((S-min (L~ C)) .. C) -' 1))) /\ (LSeg (C,((S-min (L~ C)) .. C))) is Element of bool the U1 of (TOP-REAL 2)
((((S-min (L~ C)) .. C) -' 1) + 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(((S-min (L~ C)) .. C) -' 1) + (1 + 1) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
{(C /. ((S-min (L~ C)) .. C))} is non empty trivial V26() 1 -element set
(C /. (((S-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((S-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((S-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((S-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL
C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)
C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)
S-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ C) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set
K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
S-bound (L~ C) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
SE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
E-bound (L~ C) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ C)),(SE-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ C)),(SE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (S-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (S-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (S-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:]
the U1 of ((TOP-REAL 2) | (S-most (L~ C))) is set
[: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is set
K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
(S-max (L~ C)) `1 is V11() V12() ext-real Element of REAL
(S-min (L~ C)) `1 is V11() V12() ext-real Element of REAL
C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)
C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)
W-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ C) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set
K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
W-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-bound (L~ C) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-bound (L~ C) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ C)),(NW-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ C)),(NW-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (W-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (W-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:]
the U1 of ((TOP-REAL 2) | (W-most (L~ C))) is set
[: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is set
K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
K507(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),K507(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
(W-max (L~ C)) `2 is V11() V12() ext-real Element of REAL
(W-min (L~ C)) `2 is V11() V12() ext-real Element of REAL
(W-min (L~ C)) .. C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(W-min (L~ C)) `1 is V11() V12() ext-real Element of REAL
rng C is non empty V26() set
dom C is non empty non trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT
C . ((W-min (L~ C)) .. C) is set
C /. ((W-min (L~ C)) .. C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
(W-max (L~ C)) `1 is V11() V12() ext-real Element of REAL
(W-max (L~ C)) `1 is V11() V12() ext-real Element of REAL
((W-min (L~ C)) .. C) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(((W-min (L~ C)) .. C) -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (((W-min (L~ C)) .. C) -' 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg (C,(((W-min (L~ C)) .. C) -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)
((W-min (L~ C)) .. C) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (((W-min (L~ C)) .. C) + 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg (C,((W-min (L~ C)) .. C)) is closed Element of bool the U1 of (TOP-REAL 2)
(C /. (((W-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((W-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((W-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((W-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL
LSeg ((C /. ((W-min (L~ C)) .. C)),(C /. (((W-min (L~ C)) .. C) + 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
LSeg ((C /. ((W-min (L~ C)) .. C)),(C /. (((W-min (L~ C)) .. C) -' 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg (C,(((W-min (L~ C)) .. C) -' 1))) /\ (LSeg (C,((W-min (L~ C)) .. C))) is Element of bool the U1 of (TOP-REAL 2)
((((W-min (L~ C)) .. C) -' 1) + 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
(((W-min (L~ C)) .. C) -' 1) + (1 + 1) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
{(C /. ((W-min (L~ C)) .. C))} is non empty trivial V26() 1 -element set
(C /. (((W-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((W-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL
(C /. (((W-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL
(C /. (((W-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL
C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)
C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)
W-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-bound (L~ C) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set
K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL
W-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
S-bound (L~ C) is V11() V12() ext-real Element of REAL
proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]
K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
N-bound (L~ C) is V11() V12() ext-real Element of REAL
K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ C)),(NW-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ C)),(NW-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (W-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (W-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:]
the U1 of ((TOP-REAL 2) | (W-most (L~ C))) is set
[: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is V13() set
bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is set
K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ C)),K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)
len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT
C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)
W-max (L~ C) is 2 -element FinSequence-like