:: 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 | (