:: JORDAN1J semantic presentation

REAL is V180() V181() V182() V186() set
NAT is non empty non trivial V6() V26() cardinal limit_cardinal V180() V181() V182() V183() V184() V185() V186() Element of bool REAL
bool REAL is set
NAT is non empty non trivial V6() V26() cardinal limit_cardinal V180() V181() V182() V183() V184() V185() V186() set
bool NAT is non empty non trivial V26() set
bool NAT is non empty non trivial V26() set
COMPLEX is V180() V186() set
1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
2 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
RAT is V180() V181() V182() V183() V186() set
INT is V180() V181() V182() V183() V184() V186() set
[:1,1:] is V26() set
bool [:1,1:] is V26() V30() set
[:[:1,1:],1:] is V26() set
bool [:[:1,1:],1:] is V26() V30() set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:2,2:] is V26() set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is set
bool [:REAL,REAL:] is set
TOP-REAL 2 is non empty non trivial TopSpace-like T_0 T_1 T_2 V107() V138() V139() V140() V141() V142() V143() V144() strict add-continuous Mult-continuous RLTopStruct
the U1 of (TOP-REAL 2) is non empty non trivial functional set
K233( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the U1 of (TOP-REAL 2))
[: the U1 of (TOP-REAL 2),REAL:] is set
bool [: the U1 of (TOP-REAL 2),REAL:] is set
bool the U1 of (TOP-REAL 2) is set
{} is empty trivial V6() V10() V11() V12() Function-like functional V26() V30() cardinal {} -element FinSequence-membered ext-real non positive non negative V180() V181() V182() V183() V184() V185() V186() set
the empty trivial V6() V10() V11() V12() Function-like functional V26() V30() cardinal {} -element FinSequence-membered ext-real non positive non negative V180() V181() V182() V183() V184() V185() V186() set is empty trivial V6() V10() V11() V12() Function-like functional V26() V30() cardinal {} -element FinSequence-membered ext-real non positive non negative V180() V181() V182() V183() V184() V185() V186() set
3 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
4 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
0 is empty trivial V6() V10() V11() V12() Function-like functional V26() V30() cardinal {} -element FinSequence-membered V37() ext-real non positive non negative V179() V180() V181() V182() V183() V184() V185() V186() Element of NAT
Seg 1 is non empty trivial V26() 1 -element V180() V181() V182() V183() V184() V185() Element of bool NAT
{1} is non empty trivial V26() V30() 1 -element V180() V181() V182() V183() V184() V185() set
Seg 2 is non empty V26() 2 -element V180() V181() V182() V183() V184() V185() Element of bool NAT
{1,2} is non empty V26() V30() V180() V181() V182() V183() V184() V185() set
K74({}) is set
rng {} is set
X is V13() non empty-yielding V16( NAT ) V17(K233( 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 K233( the U1 of (TOP-REAL 2))
width X is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
len X is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
k is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
k is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
Y is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
j is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
X * (j,k) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (j,k)) `1 is V11() V12() ext-real Element of REAL
X * (Y,k) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (Y,k)) `1 is V11() V12() ext-real Element of REAL
X * (j,k) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (j,k)) `1 is V11() V12() ext-real Element of REAL
X * (j,1) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (j,1)) `1 is V11() V12() ext-real Element of REAL
X is V13() non empty-yielding V16( NAT ) V17(K233( 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 K233( the U1 of (TOP-REAL 2))
len X is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
width X is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
Y is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
j is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
k is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
k is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
X * (j,k) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (j,k)) `2 is V11() V12() ext-real Element of REAL
X * (Y,k) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (Y,k)) `2 is V11() V12() ext-real Element of REAL
X * (Y,k) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (Y,k)) `2 is V11() V12() ext-real Element of REAL
X * (1,k) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(X * (1,k)) `2 is V11() V12() ext-real Element of REAL
X is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
Y is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
X ^' Y is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
len Y is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(2,(len Y)) -cut Y is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
X ^ ((2,(len Y)) -cut Y) is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
X is non empty functional connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Y is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
Cage (X,Y) 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 (X,Y)) is non empty functional V71( TOP-REAL 2) connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
E-max (L~ (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (X,Y))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (X,Y))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ (Cage (X,Y))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y)))),REAL:]
the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y)))) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y)))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y)))),REAL:] is set
K446(((TOP-REAL 2) | (L~ (Cage (X,Y)))),(proj1 | (L~ (Cage (X,Y))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (X,Y))) is functional Element of bool the U1 of (TOP-REAL 2)
SE-corner (L~ (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (X,Y))) is V11() V12() ext-real Element of REAL
proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ (Cage (X,Y))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (X,Y)))),REAL:]
K445(((TOP-REAL 2) | (L~ (Cage (X,Y)))),(proj2 | (L~ (Cage (X,Y))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (X,Y)))),(S-bound (L~ (Cage (X,Y))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (X,Y))) is V11() V12() ext-real Element of REAL
K446(((TOP-REAL 2) | (L~ (Cage (X,Y)))),(proj2 | (L~ (Cage (X,Y))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (X,Y)))),(N-bound (L~ (Cage (X,Y))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (X,Y)))),(NE-corner (L~ (Cage (X,Y))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SE-corner (L~ (Cage (X,Y)))),(NE-corner (L~ (Cage (X,Y)))))) /\ (L~ (Cage (X,Y))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (E-most (L~ (Cage (X,Y)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (X,Y)))) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (X,Y)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (X,Y))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (X,Y))))),REAL:]
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (X,Y))))) is set
[: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (X,Y))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (X,Y))))),REAL:] is set
K446(((TOP-REAL 2) | (E-most (L~ (Cage (X,Y))))),(proj2 | (E-most (L~ (Cage (X,Y)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (X,Y)))),K446(((TOP-REAL 2) | (E-most (L~ (Cage (X,Y))))),(proj2 | (E-most (L~ (Cage (X,Y))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(Cage (X,Y)) -: (E-max (L~ (Cage (X,Y)))) 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)
L~ ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y))))) is functional V71( TOP-REAL 2) bounded compact Element of bool the U1 of (TOP-REAL 2)
(Cage (X,Y)) :- (E-max (L~ (Cage (X,Y)))) 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)
L~ ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y))))) is functional V71( TOP-REAL 2) bounded compact Element of bool the U1 of (TOP-REAL 2)
(L~ ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y)))))) /\ (L~ ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y)))))) is functional Element of bool the U1 of (TOP-REAL 2)
N-min (L~ (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Cage (X,Y))) is functional Element of bool the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (X,Y))) is V11() V12() ext-real Element of REAL
K445(((TOP-REAL 2) | (L~ (Cage (X,Y)))),(proj1 | (L~ (Cage (X,Y))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (X,Y)))),(N-bound (L~ (Cage (X,Y))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (X,Y)))),(NE-corner (L~ (Cage (X,Y))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((NW-corner (L~ (Cage (X,Y)))),(NE-corner (L~ (Cage (X,Y)))))) /\ (L~ (Cage (X,Y))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (N-most (L~ (Cage (X,Y)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (X,Y)))) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (X,Y)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))),REAL:]
the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))) is set
[: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))),REAL:] is set
K445(((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))),(proj1 | (N-most (L~ (Cage (X,Y)))))) is V11() V12() ext-real Element of REAL
|[K445(((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))),(proj1 | (N-most (L~ (Cage (X,Y)))))),(N-bound (L~ (Cage (X,Y))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
{(N-min (L~ (Cage (X,Y)))),(E-max (L~ (Cage (X,Y))))} is non empty functional V26() V30() set
(E-max (L~ (Cage (X,Y)))) `1 is V11() V12() ext-real Element of REAL
rng (Cage (X,Y)) is non empty non trivial V26() set
((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y))))) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
rng ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y))))) is V26() set
len ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y))))) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y))))) /. (len ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y)))))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
len (Cage (X,Y)) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(Cage (X,Y)) /. (len (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(Cage (X,Y)) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LS is set
card {(N-min (L~ (Cage (X,Y)))),(E-max (L~ (Cage (X,Y))))} is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
card (rng ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
dom ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y))))) is V26() V180() V181() V182() V183() V184() V185() Element of bool NAT
card (dom ((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
N-max (L~ (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
K446(((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))),(proj1 | (N-most (L~ (Cage (X,Y)))))) is V11() V12() ext-real Element of REAL
|[K446(((TOP-REAL 2) | (N-most (L~ (Cage (X,Y))))),(proj1 | (N-most (L~ (Cage (X,Y)))))),(N-bound (L~ (Cage (X,Y))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Cage (X,Y)))) `1 is V11() V12() ext-real Element of REAL
len ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y))))) /. (len ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y)))))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
rng ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y))))) is V26() set
((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y))))) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LS is set
card (rng ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
dom ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y))))) is V26() V180() V181() V182() V183() V184() V185() Element of bool NAT
card (dom ((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
LS is set
UA is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
Wmin is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
Wmin + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
LSeg (((Cage (X,Y)) -: (E-max (L~ (Cage (X,Y))))),Wmin) is functional Element of bool the U1 of (TOP-REAL 2)
LSeg ((Cage (X,Y)),Wmin) is functional Element of bool the U1 of (TOP-REAL 2)
Emax is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
Emax + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
LSeg (((Cage (X,Y)) :- (E-max (L~ (Cage (X,Y))))),Emax) is functional Element of bool the U1 of (TOP-REAL 2)
Emax -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(Emax -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
1 + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Emax -' 1) + 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(len (Cage (X,Y))) - ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is V11() V12() ext-real set
((len (Cage (X,Y))) - ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y)))) + 1 is V11() V12() ext-real set
Emax - 1 is V11() V12() ext-real set
(Emax - 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is V11() V12() ext-real set
1 - 1 is V11() V12() ext-real set
(Emax -' 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
LSeg ((Cage (X,Y)),((Emax -' 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))))) is functional Element of bool the U1 of (TOP-REAL 2)
((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Emax -' 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y)))) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(LSeg ((Cage (X,Y)),Wmin)) /\ (LSeg ((Cage (X,Y)),((Emax -' 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y)))))) is functional Element of bool the U1 of (TOP-REAL 2)
0 + 2 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(LSeg ((Cage (X,Y)),Wmin)) /\ (LSeg ((Cage (X,Y)),((Emax -' 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y)))))) is functional Element of bool the U1 of (TOP-REAL 2)
(len (Cage (X,Y))) - 1 is V11() V12() ext-real set
(len (Cage (X,Y))) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(LSeg ((Cage (X,Y)),Wmin)) /\ (LSeg ((Cage (X,Y)),((Emax -' 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y)))))) is functional Element of bool the U1 of (TOP-REAL 2)
{((Cage (X,Y)) /. 1)} is non empty trivial functional V26() V30() 1 -element set
1 + 2 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
LSeg ((Cage (X,Y)),1) is functional Element of bool the U1 of (TOP-REAL 2)
1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
LSeg ((Cage (X,Y)),(1 + 1)) is functional Element of bool the U1 of (TOP-REAL 2)
(LSeg ((Cage (X,Y)),1)) /\ (LSeg ((Cage (X,Y)),(1 + 1))) is functional Element of bool the U1 of (TOP-REAL 2)
(Cage (X,Y)) /. (1 + 1) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
{((Cage (X,Y)) /. (1 + 1))} is non empty trivial functional V26() V30() 1 -element set
0 + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
0 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) -' 1) + (1 + 1) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
0 + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(LSeg ((Cage (X,Y)),Wmin)) /\ (LSeg ((Cage (X,Y)),((Emax -' 1) + ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y)))))) is functional Element of bool the U1 of (TOP-REAL 2)
(Cage (X,Y)) /. ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
{((Cage (X,Y)) /. ((E-max (L~ (Cage (X,Y)))) .. (Cage (X,Y))))} is non empty trivial functional V26() V30() 1 -element set
LS is set
X is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
Y is non empty functional connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Upper_Seq (Y,X) 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 standard FinSequence of the U1 of (TOP-REAL 2)
Cage (Y,X) 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 (Y,X)) is non empty functional V71( TOP-REAL 2) connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
E-max (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (Y,X))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ (Cage (Y,X))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:]
the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:] is set
K446(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj1 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
SE-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ (Cage (Y,X))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:]
K445(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj2 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (Y,X)))),(S-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
K446(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj2 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (Y,X)))),(N-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (Y,X)))),(NE-corner (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SE-corner (L~ (Cage (Y,X)))),(NE-corner (L~ (Cage (Y,X)))))) /\ (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (E-most (L~ (Cage (Y,X)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (Y,X)))) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),REAL:]
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))) is set
[: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),REAL:] is set
K446(((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),(proj2 | (E-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (Y,X)))),K446(((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),(proj2 | (E-most (L~ (Cage (Y,X))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (Y,X)),(E-max (L~ (Cage (Y,X))))) 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)
W-min (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
K445(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj1 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
|[(W-bound (L~ (Cage (Y,X)))),(S-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
|[(W-bound (L~ (Cage (Y,X)))),(N-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (Y,X)))),(NW-corner (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ (Cage (Y,X)))),(NW-corner (L~ (Cage (Y,X)))))) /\ (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (W-most (L~ (Cage (Y,X)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (Y,X)))) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),REAL:]
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))) is set
[: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),REAL:] is set
K445(((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),(proj2 | (W-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (Y,X)))),K445(((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),(proj2 | (W-most (L~ (Cage (Y,X))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (Y,X)),(E-max (L~ (Cage (Y,X)))))) :- (W-min (L~ (Cage (Y,X)))) 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)
N-min (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (Y,X)))),(NE-corner (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((NW-corner (L~ (Cage (Y,X)))),(NE-corner (L~ (Cage (Y,X)))))) /\ (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (N-most (L~ (Cage (Y,X)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (Y,X)))) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (Y,X)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))),REAL:]
the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))) is set
[: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))),REAL:] is set
K445(((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))),(proj1 | (N-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[K445(((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))),(proj1 | (N-most (L~ (Cage (Y,X)))))),(N-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
N-max (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
K446(((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))),(proj1 | (N-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[K446(((TOP-REAL 2) | (N-most (L~ (Cage (Y,X))))),(proj1 | (N-most (L~ (Cage (Y,X)))))),(N-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
W-max (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
K446(((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),(proj2 | (W-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (Y,X)))),K446(((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),(proj2 | (W-most (L~ (Cage (Y,X))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
E-min (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
K445(((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),(proj2 | (E-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (Y,X)))),K445(((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),(proj2 | (E-most (L~ (Cage (Y,X))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
S-max (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
S-most (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (Y,X)))),(SE-corner (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ (Cage (Y,X)))),(SE-corner (L~ (Cage (Y,X)))))) /\ (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (S-most (L~ (Cage (Y,X)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj1 | (S-most (L~ (Cage (Y,X)))) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (Y,X)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))),REAL:]
the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))) is set
[: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))),REAL:] is set
K446(((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))),(proj1 | (S-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[K446(((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))),(proj1 | (S-most (L~ (Cage (Y,X)))))),(S-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
S-min (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
K445(((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))),(proj1 | (S-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[K445(((TOP-REAL 2) | (S-most (L~ (Cage (Y,X))))),(proj1 | (S-most (L~ (Cage (Y,X)))))),(S-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (Y,X)),(W-min (L~ (Cage (Y,X))))) 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)
rng (Cage (Y,X)) is non empty non trivial V26() set
(Cage (Y,X)) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Cage (Y,X)))) .. (Cage (Y,X)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(S-max (L~ (Cage (Y,X)))) .. (Cage (Y,X)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(E-max (L~ (Cage (Y,X)))) .. (Cage (Y,X)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(S-min (L~ (Cage (Y,X)))) .. (Cage (Y,X)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(W-min (L~ (Cage (Y,X)))) .. (Cage (Y,X)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(Cage (Y,X)) :- (E-max (L~ (Cage (Y,X)))) 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)
((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
rng ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) is V26() set
len ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) /. (len ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X)))))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
len (Cage (Y,X)) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(Cage (Y,X)) /. (len (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
{(N-min (L~ (Cage (Y,X)))),(E-max (L~ (Cage (Y,X))))} is non empty functional V26() V30() set
Ebo is set
card {(N-min (L~ (Cage (Y,X)))),(E-max (L~ (Cage (Y,X))))} is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
card (rng ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(Cage (Y,X)) -: (W-min (L~ (Cage (Y,X)))) 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)
len ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /. (len ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X)))))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
rng ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) is V26() set
((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
{(N-min (L~ (Cage (Y,X)))),(W-min (L~ (Cage (Y,X))))} is non empty functional V26() V30() set
Ebo is set
card {(N-min (L~ (Cage (Y,X)))),(W-min (L~ (Cage (Y,X))))} is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
card (rng ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
dom ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) is V26() V180() V181() V182() V183() V184() V185() Element of bool NAT
card (dom ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(N-min (L~ (Cage (Y,X)))) `2 is V11() V12() ext-real Element of REAL
(N-max (L~ (Cage (Y,X)))) `1 is V11() V12() ext-real Element of REAL
(NE-corner (L~ (Cage (Y,X)))) `1 is V11() V12() ext-real Element of REAL
(N-min (L~ (Cage (Y,X)))) `1 is V11() V12() ext-real Element of REAL
(W-max (L~ (Cage (Y,X)))) `2 is V11() V12() ext-real Element of REAL
L~ ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) bounded compact Element of bool the U1 of (TOP-REAL 2)
(Cage (Y,X)) :- (W-min (L~ (Cage (Y,X)))) 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)
rng ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) is V26() set
((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
len ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) /. (len ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X)))))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
Ebo is set
card (rng ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
dom ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) is V26() V180() V181() V182() V183() V184() V185() Element of bool NAT
card (dom ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
L~ ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) bounded compact Element of bool the U1 of (TOP-REAL 2)
(L~ ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X)))))) /\ (L~ ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X)))))) is functional Element of bool the U1 of (TOP-REAL 2)
(N-max (L~ (Cage (Y,X)))) .. (Cage (Y,X)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(N-min (L~ (Cage (Y,X)))) .. (Cage (Y,X)) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(E-max (L~ (Cage (Y,X)))) .. ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
(N-min (L~ (Cage (Y,X)))) .. ((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1 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)
rng (((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1) is V26() set
(rng (((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1)) \ (rng ((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X)))))) is V26() Element of bool (rng (((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1))
bool (rng (((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1)) is V26() V30() set
dom ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) is V26() V180() V181() V182() V183() V184() V185() Element of bool NAT
card (dom ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
L~ ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) bounded compact Element of bool the U1 of (TOP-REAL 2)
(Cage (Y,X)) -: (E-max (L~ (Cage (Y,X)))) 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)
rng ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) is V26() set
len ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) /. (len ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X)))))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) /. ((E-max (L~ (Cage (Y,X)))) .. (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) /. 1 is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
Ebo is set
card (rng ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
dom ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) is V26() V180() V181() V182() V183() V184() V185() Element of bool NAT
card (dom ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X)))))) is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
L~ ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) bounded compact Element of bool the U1 of (TOP-REAL 2)
(L~ ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X)))))) /\ (L~ ((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X)))))) is functional Element of bool the U1 of (TOP-REAL 2)
(rng (Cage (Y,X))) \ (rng ((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X)))))) is V26() Element of bool (rng (Cage (Y,X)))
bool (rng (Cage (Y,X))) is V26() V30() set
(Rotate ((Cage (Y,X)),(W-min (L~ (Cage (Y,X)))))) -: (E-max (L~ (Cage (Y,X)))) 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)
((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) ^ (((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1) 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)
(((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) ^ (((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1)) -: (E-max (L~ (Cage (Y,X)))) is 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)
(((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1) -: (E-max (L~ (Cage (Y,X)))) 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)
((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) ^ ((((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) /^ 1) -: (E-max (L~ (Cage (Y,X))))) 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)
((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) -: (E-max (L~ (Cage (Y,X)))) 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)
(((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) -: (E-max (L~ (Cage (Y,X))))) /^ 1 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)
((Cage (Y,X)) :- (W-min (L~ (Cage (Y,X))))) ^ ((((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) -: (E-max (L~ (Cage (Y,X))))) /^ 1) 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)
((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) :- (W-min (L~ (Cage (Y,X)))) 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)
(((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) :- (W-min (L~ (Cage (Y,X))))) ^ ((((Cage (Y,X)) -: (W-min (L~ (Cage (Y,X))))) -: (E-max (L~ (Cage (Y,X))))) /^ 1) 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)
((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) /^ 1 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)
(((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) :- (W-min (L~ (Cage (Y,X))))) ^ (((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) /^ 1) 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)
((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) ^ (((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) /^ 1) 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)
(((Cage (Y,X)) :- (E-max (L~ (Cage (Y,X))))) ^ (((Cage (Y,X)) -: (E-max (L~ (Cage (Y,X))))) /^ 1)) :- (W-min (L~ (Cage (Y,X)))) 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)
X is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V179() V180() V181() V182() V183() V184() V185() Element of NAT
Y is non empty functional bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Cage (Y,X) 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 (Y,X)) is non empty functional V71( TOP-REAL 2) connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
W-min (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (Y,X))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
proj1 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj1 | (L~ (Cage (Y,X))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:]
the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))) is non empty set
[: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:] is set
K445(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj1 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
SW-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
proj2 | (L~ (Cage (Y,X))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (Y,X)))),REAL:]
K445(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj2 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (Y,X)))),(S-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
K446(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj2 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (Y,X)))),(N-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (Y,X)))),(NW-corner (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SW-corner (L~ (Cage (Y,X)))),(NW-corner (L~ (Cage (Y,X)))))) /\ (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (W-most (L~ (Cage (Y,X)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (Y,X)))) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),REAL:]
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))) is set
[: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),REAL:] is set
K445(((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),(proj2 | (W-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (Y,X)))),K445(((TOP-REAL 2) | (W-most (L~ (Cage (Y,X))))),(proj2 | (W-most (L~ (Cage (Y,X))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
Upper_Seq (Y,X) 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)
rng (Upper_Seq (Y,X)) is V26() set
L~ (Upper_Seq (Y,X)) is non empty functional V71( TOP-REAL 2) bounded compact Element of bool the U1 of (TOP-REAL 2)
rng (Cage (Y,X)) is non empty non trivial V26() set
E-max (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (Y,X))) is V11() V12() ext-real Element of REAL
K446(((TOP-REAL 2) | (L~ (Cage (Y,X)))),(proj1 | (L~ (Cage (Y,X))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
SE-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (Y,X)))),(S-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (Y,X))) is V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (Y,X)))),(N-bound (L~ (Cage (Y,X))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V171() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (Y,X)))),(NE-corner (L~ (Cage (Y,X))))) is functional V71( TOP-REAL 2) connected bounded bounded compact compact Element of bool the U1 of (TOP-REAL 2)
(LSeg ((SE-corner (L~ (Cage (Y,X)))),(NE-corner (L~ (Cage (Y,X)))))) /\ (L~ (Cage (Y,X))) is functional Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (E-most (L~ (Cage (Y,X)))) is strict TopSpace-like SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (Y,X)))) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),REAL:]
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))) is set
[: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),REAL:] is set
bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),REAL:] is set
K446(((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),(proj2 | (E-most (L~ (Cage (Y,X)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (Y,X)))),K446(((TOP-REAL 2) | (E-most (L~ (Cage (Y,X))))),(proj2 | (