:: JORDAN1G semantic presentation

REAL is V200() V201() V202() V206() set

NAT is non empty non trivial V6() V26() cardinal limit_cardinal V200() V201() V202() V203() V204() V205() V206() Element of bool REAL

bool REAL is set

NAT is non empty non trivial V6() V26() cardinal limit_cardinal V200() V201() V202() V203() V204() V205() V206() set

bool NAT is non empty non trivial V26() set

bool NAT is non empty non trivial V26() set

COMPLEX is V200() V206() set

1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

2 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

K356() is TopStruct

the U1 of K356() is set

[:1,1:] is V13() V26() set

bool [:1,1:] is V26() V30() set

[:[:1,1:],1:] is V13() V26() set

bool [:[:1,1:],1:] is V26() V30() set

[:[:1,1:],REAL:] is V13() set

bool [:[:1,1:],REAL:] is set

[:REAL,REAL:] is V13() set

[:[:REAL,REAL:],REAL:] is V13() set

bool [:[:REAL,REAL:],REAL:] is set

[:2,2:] is V13() V26() set

[:[:2,2:],REAL:] is V13() set

bool [:[:2,2:],REAL:] is set

K384() is V171() L15()

K394() is TopSpace-like T_0 T_1 T_2 TopStruct

RAT is V200() V201() V202() V203() V206() set

INT is V200() V201() V202() V203() V204() V206() set

bool [:REAL,REAL:] is set

TOP-REAL 2 is non empty non trivial TopSpace-like V104() V135() V136() V137() V138() V139() V140() V141() strict RLTopStruct

the U1 of (TOP-REAL 2) is non empty non trivial set

[: the U1 of (TOP-REAL 2),REAL:] is V13() set

bool [: the U1 of (TOP-REAL 2),REAL:] is set

bool the U1 of (TOP-REAL 2) is set

K238( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the U1 of (TOP-REAL 2))

{} is empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V200() V201() V202() V203() V204() V205() V206() set

the empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V200() V201() V202() V203() V204() V205() V206() set is empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V200() V201() V202() V203() V204() V205() V206() set

3 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

4 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

0 is empty trivial V6() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V27() V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V37() ext-real non positive non negative V199() V200() V201() V202() V203() V204() V205() V206() Element of NAT

Seg 1 is non empty trivial V26() 1 -element V200() V201() V202() V203() V204() V205() Element of bool NAT

{1} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set

Seg 2 is non empty V26() 2 -element V200() V201() V202() V203() V204() V205() Element of bool NAT

{1,2} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set

K396() is TopSpace-like SubSpace of K394()

the U1 of K396() is set

C is trivial V13() V16( NAT ) Function-like constant V26() FinSequence-like FinSubsequence-like set

n is set

{n} is non empty trivial V26() 1 -element set

i is set

j is set

[i,j] is non empty set

{i,j} is non empty V26() set

{i} is non empty trivial V26() 1 -element set

{{i,j},{i}} is non empty V26() V30() set

dom C is trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT

<*j*> is non empty trivial V13() V16( NAT ) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like set

C is non empty non trivial V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set

Rev C is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set

n is set

<*n*> is non empty trivial V13() V16( NAT ) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like set

n is set

<*n*> is non empty trivial V13() V16( NAT ) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like set

Rev <*n*> is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set

C is non empty set

K238(C) is non empty functional FinSequence-membered M11(C)

n is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C

i is V13() V16( NAT ) V17(K238(C)) Function-like V26() FinSequence-like FinSubsequence-like tabular FinSequence of K238(C)

j is set

n -: j is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C

j .. n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

n | (j .. n) is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C

C is non empty set

K238(C) is non empty functional FinSequence-membered M11(C)

n is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C

rng n is V26() set

i is V13() V16( NAT ) V17(K238(C)) Function-like V26() FinSequence-like FinSubsequence-like tabular FinSequence of K238(C)

j is Element of C

n :- j is non empty V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C

j .. n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

Emax is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

Emax + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

n /^ Emax is V13() V16( NAT ) V17(C) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C

C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

n is non empty connected compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)

Upper_Seq (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

Gauge (n,C) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))

Cage (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Cage (n,C)) is non empty closed connected V222() compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)

W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ (Cage (n,C))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]

the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is set

K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

W-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]

K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (W-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:]

the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set

[: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is set

K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ (Cage (n,C)))),K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

E-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

E-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (E-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:]

the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set

[: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is set

K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL

|[(E-bound (L~ (Cage (n,C)))),K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) -: (E-max (L~ (Cage (n,C)))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded FinSequence of the U1 of (TOP-REAL 2)

C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

n is non empty connected compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)

Lower_Seq (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

Gauge (n,C) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))

Cage (n,C) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

L~ (Cage (n,C)) is non empty closed connected V222() compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)

W-min (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ (Cage (n,C))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]

the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:] is set

K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

W-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

SW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ (Cage (n,C))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ (Cage (n,C)))),REAL:]

K506(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NW-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj2 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SW-corner (L~ (Cage (n,C)))),(NW-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (W-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (W-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:]

the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))) is set

[: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),REAL:] is set

K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ (Cage (n,C)))),K506(((TOP-REAL 2) | (W-most (L~ (Cage (n,C))))),(proj2 | (W-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C))))) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

E-max (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

E-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ (Cage (n,C)))),(proj1 | (L~ (Cage (n,C))))) is V11() V12() ext-real Element of REAL

E-most (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

SE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

|[(E-bound (L~ (Cage (n,C)))),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NE-corner (L~ (Cage (n,C))) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

|[(E-bound (L~ (Cage (n,C)))),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C))))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SE-corner (L~ (Cage (n,C)))),(NE-corner (L~ (Cage (n,C)))))) /\ (L~ (Cage (n,C))) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (E-most (L~ (Cage (n,C)))) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (E-most (L~ (Cage (n,C)))) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:]

the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))) is set

[: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),REAL:] is set

K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C)))))) is V11() V12() ext-real Element of REAL

|[(E-bound (L~ (Cage (n,C)))),K507(((TOP-REAL 2) | (E-most (L~ (Cage (n,C))))),(proj2 | (E-most (L~ (Cage (n,C))))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

rng (Cage (n,C)) is non empty non trivial V26() set

rng (Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) is non empty non trivial V26() set

(Rotate ((Cage (n,C)),(W-min (L~ (Cage (n,C)))))) :- (E-max (L~ (Cage (n,C)))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

C is non empty connected compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)

n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

Upper_Seq (C,n) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

Gauge (C,n) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))

Lower_Seq (C,n) is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

Gauge (C,n) is V13() non empty-yielding V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))

C is V13() V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular Y_equal-in-column Y_increasing-in-line FinSequence of K238( the U1 of (TOP-REAL 2))

Indices C is set

n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

j is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

[n,j] is non empty set

{n,j} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set

{n} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set

{{n,j},{n}} is non empty V26() V30() set

i is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

Emax is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

[i,Emax] is non empty set

{i,Emax} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set

{i} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set

{{i,Emax},{i}} is non empty V26() V30() set

C * (n,j) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (n,j)) `2 is V11() V12() ext-real Element of REAL

C * (i,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (i,Emax)) `2 is V11() V12() ext-real Element of REAL

width C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

len C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C * (n,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (n,Emax)) `2 is V11() V12() ext-real Element of REAL

C * (1,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (1,Emax)) `2 is V11() V12() ext-real Element of REAL

C is V13() V16( NAT ) V17(K238( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line X_increasing-in-column FinSequence of K238( the U1 of (TOP-REAL 2))

Indices C is set

n is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

j is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

[n,j] is non empty set

{n,j} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set

{n} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set

{{n,j},{n}} is non empty V26() V30() set

i is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

Emax is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

[i,Emax] is non empty set

{i,Emax} is non empty V26() V30() V200() V201() V202() V203() V204() V205() set

{i} is non empty trivial V26() V30() 1 -element V200() V201() V202() V203() V204() V205() set

{{i,Emax},{i}} is non empty V26() V30() set

C * (n,j) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (n,j)) `1 is V11() V12() ext-real Element of REAL

C * (i,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (i,Emax)) `1 is V11() V12() ext-real Element of REAL

len C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

width C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C * (n,1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (n,1)) `1 is V11() V12() ext-real Element of REAL

C * (n,Emax) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(C * (n,Emax)) `1 is V11() V12() ext-real Element of REAL

C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)

C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

N-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)

NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ C) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set

K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

N-bound (L~ C) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

E-bound (L~ C) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(E-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((NW-corner (L~ C)),(NE-corner (L~ C))) is closed closed connected compact compact horizontal Element of bool the U1 of (TOP-REAL 2)

(LSeg ((NW-corner (L~ C)),(NE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (N-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2

proj1 | (N-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:]

the U1 of ((TOP-REAL 2) | (N-most (L~ C))) is set

[: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is set

K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

(N-max (L~ C)) `1 is V11() V12() ext-real Element of REAL

(N-min (L~ C)) `1 is V11() V12() ext-real Element of REAL

(N-min (L~ C)) .. C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(N-min (L~ C)) `2 is V11() V12() ext-real Element of REAL

rng C is non empty V26() set

dom C is non empty non trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT

C . ((N-min (L~ C)) .. C) is set

C /. ((N-min (L~ C)) .. C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(N-max (L~ C)) `2 is V11() V12() ext-real Element of REAL

(N-max (L~ C)) `2 is V11() V12() ext-real Element of REAL

((N-min (L~ C)) .. C) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(((N-min (L~ C)) .. C) -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (((N-min (L~ C)) .. C) -' 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg (C,(((N-min (L~ C)) .. C) -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)

((N-min (L~ C)) .. C) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (((N-min (L~ C)) .. C) + 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg (C,((N-min (L~ C)) .. C)) is closed Element of bool the U1 of (TOP-REAL 2)

(C /. (((N-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((N-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((N-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((N-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL

LSeg ((C /. ((N-min (L~ C)) .. C)),(C /. (((N-min (L~ C)) .. C) + 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

LSeg ((C /. ((N-min (L~ C)) .. C)),(C /. (((N-min (L~ C)) .. C) -' 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg (C,(((N-min (L~ C)) .. C) -' 1))) /\ (LSeg (C,((N-min (L~ C)) .. C))) is Element of bool the U1 of (TOP-REAL 2)

((((N-min (L~ C)) .. C) -' 1) + 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(((N-min (L~ C)) .. C) -' 1) + (1 + 1) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

{(C /. ((N-min (L~ C)) .. C))} is non empty trivial V26() 1 -element set

(C /. (((N-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((N-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((N-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((N-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL

C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)

C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

N-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)

NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ C) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set

K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

N-bound (L~ C) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

E-bound (L~ C) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(E-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((NW-corner (L~ C)),(NE-corner (L~ C))) is closed closed connected compact compact horizontal Element of bool the U1 of (TOP-REAL 2)

(LSeg ((NW-corner (L~ C)),(NE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (N-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2

proj1 | (N-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:]

the U1 of ((TOP-REAL 2) | (N-most (L~ C))) is set

[: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (N-most (L~ C))),REAL:] is set

K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K506(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K507(((TOP-REAL 2) | (N-most (L~ C))),(proj1 | (N-most (L~ C)))),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

(N-max (L~ C)) `1 is V11() V12() ext-real Element of REAL

(N-min (L~ C)) `1 is V11() V12() ext-real Element of REAL

C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)

C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

S-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)

SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ C) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set

K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

S-bound (L~ C) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

SE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

E-bound (L~ C) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(E-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SW-corner (L~ C)),(SE-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SW-corner (L~ C)),(SE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (S-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2

proj1 | (S-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (S-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:]

the U1 of ((TOP-REAL 2) | (S-most (L~ C))) is set

[: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is set

K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

(S-max (L~ C)) `1 is V11() V12() ext-real Element of REAL

(S-min (L~ C)) `1 is V11() V12() ext-real Element of REAL

(S-min (L~ C)) .. C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(S-min (L~ C)) `2 is V11() V12() ext-real Element of REAL

rng C is non empty V26() set

dom C is non empty non trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT

C . ((S-min (L~ C)) .. C) is set

C /. ((S-min (L~ C)) .. C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(S-max (L~ C)) `2 is V11() V12() ext-real Element of REAL

(S-max (L~ C)) `2 is V11() V12() ext-real Element of REAL

((S-min (L~ C)) .. C) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(((S-min (L~ C)) .. C) -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (((S-min (L~ C)) .. C) -' 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg (C,(((S-min (L~ C)) .. C) -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)

((S-min (L~ C)) .. C) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (((S-min (L~ C)) .. C) + 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg (C,((S-min (L~ C)) .. C)) is closed Element of bool the U1 of (TOP-REAL 2)

(C /. (((S-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((S-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((S-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((S-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL

LSeg ((C /. ((S-min (L~ C)) .. C)),(C /. (((S-min (L~ C)) .. C) + 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

LSeg ((C /. ((S-min (L~ C)) .. C)),(C /. (((S-min (L~ C)) .. C) -' 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg (C,(((S-min (L~ C)) .. C) -' 1))) /\ (LSeg (C,((S-min (L~ C)) .. C))) is Element of bool the U1 of (TOP-REAL 2)

((((S-min (L~ C)) .. C) -' 1) + 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(((S-min (L~ C)) .. C) -' 1) + (1 + 1) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

{(C /. ((S-min (L~ C)) .. C))} is non empty trivial V26() 1 -element set

(C /. (((S-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((S-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((S-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((S-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL

C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)

C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

S-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)

SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ C) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set

K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

S-bound (L~ C) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

SE-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

E-bound (L~ C) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(E-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SW-corner (L~ C)),(SE-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SW-corner (L~ C)),(SE-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (S-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2

proj1 | (S-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (S-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:]

the U1 of ((TOP-REAL 2) | (S-most (L~ C))) is set

[: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (S-most (L~ C))),REAL:] is set

K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K506(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[K507(((TOP-REAL 2) | (S-most (L~ C))),(proj1 | (S-most (L~ C)))),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

(S-max (L~ C)) `1 is V11() V12() ext-real Element of REAL

(S-min (L~ C)) `1 is V11() V12() ext-real Element of REAL

C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)

C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

W-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ C) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set

K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

W-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)

SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-bound (L~ C) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-bound (L~ C) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SW-corner (L~ C)),(NW-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SW-corner (L~ C)),(NW-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (W-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (W-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:]

the U1 of ((TOP-REAL 2) | (W-most (L~ C))) is set

[: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is set

K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-max (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

K507(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),K507(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

(W-max (L~ C)) `2 is V11() V12() ext-real Element of REAL

(W-min (L~ C)) `2 is V11() V12() ext-real Element of REAL

(W-min (L~ C)) .. C is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(W-min (L~ C)) `1 is V11() V12() ext-real Element of REAL

rng C is non empty V26() set

dom C is non empty non trivial V26() V200() V201() V202() V203() V204() V205() Element of bool NAT

C . ((W-min (L~ C)) .. C) is set

C /. ((W-min (L~ C)) .. C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

(W-max (L~ C)) `1 is V11() V12() ext-real Element of REAL

(W-max (L~ C)) `1 is V11() V12() ext-real Element of REAL

((W-min (L~ C)) .. C) -' 1 is V6() V10() V11() V12() V26() cardinal V37() ext-real non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(((W-min (L~ C)) .. C) -' 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (((W-min (L~ C)) .. C) -' 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg (C,(((W-min (L~ C)) .. C) -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)

((W-min (L~ C)) .. C) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (((W-min (L~ C)) .. C) + 1) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg (C,((W-min (L~ C)) .. C)) is closed Element of bool the U1 of (TOP-REAL 2)

(C /. (((W-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((W-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((W-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((W-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL

LSeg ((C /. ((W-min (L~ C)) .. C)),(C /. (((W-min (L~ C)) .. C) + 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

LSeg ((C /. ((W-min (L~ C)) .. C)),(C /. (((W-min (L~ C)) .. C) -' 1))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg (C,(((W-min (L~ C)) .. C) -' 1))) /\ (LSeg (C,((W-min (L~ C)) .. C))) is Element of bool the U1 of (TOP-REAL 2)

((((W-min (L~ C)) .. C) -' 1) + 1) + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

1 + 1 is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

(((W-min (L~ C)) .. C) -' 1) + (1 + 1) is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

{(C /. ((W-min (L~ C)) .. C))} is non empty trivial V26() 1 -element set

(C /. (((W-min (L~ C)) .. C) -' 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((W-min (L~ C)) .. C) -' 1)) `2 is V11() V12() ext-real Element of REAL

(C /. (((W-min (L~ C)) .. C) + 1)) `1 is V11() V12() ext-real Element of REAL

(C /. (((W-min (L~ C)) .. C) + 1)) `2 is V11() V12() ext-real Element of REAL

C is non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded standard FinSequence of the U1 of (TOP-REAL 2)

C /. 1 is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

L~ C is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

W-min (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-bound (L~ C) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ C) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

proj1 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

the U1 of ((TOP-REAL 2) | (L~ C)) is non empty set

[: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:] is set

K506(((TOP-REAL 2) | (L~ C)),(proj1 | (L~ C))) is V11() V12() ext-real Element of REAL

W-most (L~ C) is Element of bool the U1 of (TOP-REAL 2)

SW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

S-bound (L~ C) is V11() V12() ext-real Element of REAL

proj2 is V13() Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | (L~ C) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (L~ C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (L~ C)),REAL:]

K506(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(S-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

NW-corner (L~ C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

N-bound (L~ C) is V11() V12() ext-real Element of REAL

K507(((TOP-REAL 2) | (L~ C)),(proj2 | (L~ C))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),(N-bound (L~ C))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

LSeg ((SW-corner (L~ C)),(NW-corner (L~ C))) is closed closed connected compact compact Element of bool the U1 of (TOP-REAL 2)

(LSeg ((SW-corner (L~ C)),(NW-corner (L~ C)))) /\ (L~ C) is Element of bool the U1 of (TOP-REAL 2)

(TOP-REAL 2) | (W-most (L~ C)) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (W-most (L~ C)) is V13() Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ C))), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:]

the U1 of ((TOP-REAL 2) | (W-most (L~ C))) is set

[: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is V13() set

bool [: the U1 of ((TOP-REAL 2) | (W-most (L~ C))),REAL:] is set

K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C)))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ C)),K506(((TOP-REAL 2) | (W-most (L~ C))),(proj2 | (W-most (L~ C))))]| is non empty non trivial V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V191() Element of the U1 of (TOP-REAL 2)

len C is non empty V6() V10() V11() V12() V26() cardinal V37() ext-real positive non negative V199() V200() V201() V202() V203() V204() V205() Element of NAT

C /. (len C) is 2 -element FinSequence-like V191() Element of the U1 of (TOP-REAL 2)

W-max (L~ C) is 2 -element FinSequence-like