REAL is non empty V26() V93() V94() V95() V99() set
NAT is non empty V4() V5() V6() V93() V94() V95() V96() V97() V98() V99() Element of K6(REAL)
K6(REAL) is set
NAT is non empty V4() V5() V6() V93() V94() V95() V96() V97() V98() V99() set
K6(NAT) is set
K6(NAT) is set
COMPLEX is non empty V26() V93() V99() set
RAT is non empty V26() V93() V94() V95() V96() V99() set
INT is non empty V26() V93() V94() V95() V96() V97() V99() set
1 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V92() V93() V94() V95() V96() V97() V98() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V92() V93() V94() V95() V96() V97() V98() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty V49() TopSpace-like V131() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous RLTopStruct
the U1 of (TOP-REAL 2) is non empty V2() set
K286( the U1 of (TOP-REAL 2)) is M11( the U1 of (TOP-REAL 2))
K7( the U1 of (TOP-REAL 2),REAL) is set
K6(K7( the U1 of (TOP-REAL 2),REAL)) is set
K6( the U1 of (TOP-REAL 2)) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
{} is empty V4() V5() V6() V8() V9() V10() Function-like functional V93() V94() V95() V96() V97() V98() V99() set
3 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V92() V93() V94() V95() V96() V97() V98() Element of NAT
4 is non empty V4() V5() V6() V10() V11() V12() V37() ext-real positive V92() V93() V94() V95() V96() V97() V98() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() Function-like functional V37() ext-real V92() V93() V94() V95() V96() V97() V98() V99() Element of NAT
proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) Element of K6(K7( the U1 of (TOP-REAL 2),REAL))
1 / 2 is V11() V12() ext-real Element of REAL
i is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
k is non empty connected bounded compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
Cage (k,i) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (k,i)) is non empty boundary connected bounded being_simple_closed_curve compact Element of K6( the U1 of (TOP-REAL 2))
W-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (k,i))) is strict 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 K6(K7( the U1 of (TOP-REAL 2),REAL))
proj1 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is set
K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL)) is set
lower_bound (proj1 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
lower_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (k,i)))),(NW-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (k,i)))),(NW-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(lower_bound (proj2 | (W-most (L~ (Cage (k,i))))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Cage (k,i)) /. 1 is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
NE-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL)) is set
lower_bound (proj1 | (N-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (N-most (L~ (Cage (k,i)))))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
upper_bound (proj1 | (N-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(upper_bound (proj1 | (N-most (L~ (Cage (k,i)))))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
E-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
E-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
SE-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (k,i)))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(upper_bound (proj2 | (E-most (L~ (Cage (k,i))))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
E-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
lower_bound (proj2 | (E-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
lower_bound ((proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(lower_bound (proj2 | (E-most (L~ (Cage (k,i))))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
S-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
S-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ (Cage (k,i)))),(SE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (k,i)))),(SE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj1 | (S-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))),REAL)) is set
upper_bound (proj1 | (S-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj1 | (S-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
upper_bound ((proj1 | (S-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(upper_bound (proj1 | (S-most (L~ (Cage (k,i)))))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
S-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
lower_bound (proj1 | (S-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
lower_bound ((proj1 | (S-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (S-most (L~ (Cage (k,i)))))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
i is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
k is non empty connected bounded compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
Cage (k,i) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (k,i)) is non empty boundary connected bounded being_simple_closed_curve compact Element of K6( the U1 of (TOP-REAL 2))
E-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (k,i))) is strict 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 K6(K7( the U1 of (TOP-REAL 2),REAL))
proj1 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is set
K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL)) is set
upper_bound (proj1 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
upper_bound ((proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
E-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
SE-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
lower_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(upper_bound (proj2 | (E-most (L~ (Cage (k,i))))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Cage (k,i)) /. 1 is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
NW-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
lower_bound (proj1 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
lower_bound ((proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL)) is set
lower_bound (proj1 | (N-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (N-most (L~ (Cage (k,i)))))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
upper_bound (proj1 | (N-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(upper_bound (proj1 | (N-most (L~ (Cage (k,i)))))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
i is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
k is non empty connected bounded compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
Cage (k,i) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (k,i)) is non empty boundary connected bounded being_simple_closed_curve compact Element of K6( the U1 of (TOP-REAL 2))
S-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
S-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (k,i))) is strict 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 K6(K7( the U1 of (TOP-REAL 2),REAL))
proj1 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is set
K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL)) is set
lower_bound (proj1 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
S-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
lower_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
SE-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
upper_bound (proj1 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (k,i)))),(SE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (k,i)))),(SE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj1 | (S-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))),REAL)) is set
upper_bound (proj1 | (S-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj1 | (S-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
upper_bound ((proj1 | (S-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (S-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(upper_bound (proj1 | (S-most (L~ (Cage (k,i)))))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Cage (k,i)) /. 1 is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
NW-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ (Cage (k,i)))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))),REAL)) is set
lower_bound (proj1 | (N-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(lower_bound (proj1 | (N-most (L~ (Cage (k,i)))))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
upper_bound (proj1 | (N-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
upper_bound ((proj1 | (N-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (N-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(upper_bound (proj1 | (N-most (L~ (Cage (k,i)))))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
E-max (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
E-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ (Cage (k,i)))),(NE-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj2 | (E-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))),REAL)) is set
upper_bound (proj2 | (E-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
upper_bound ((proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(upper_bound (proj2 | (E-most (L~ (Cage (k,i))))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
E-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
lower_bound (proj2 | (E-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
lower_bound ((proj2 | (E-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (E-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Cage (k,i)))),(lower_bound (proj2 | (E-most (L~ (Cage (k,i))))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
k is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng k is V2() Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
C .. k is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
left_cell (k,(C .. k)) is Element of K6( the U1 of (TOP-REAL 2))
Rotate (k,C) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
left_cell ((Rotate (k,C)),1) is Element of K6( the U1 of (TOP-REAL 2))
len k is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(C .. k) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
GoB (Rotate (k,C)) is V13() non empty-yielding V16( NAT ) V17(K286( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K286( the U1 of (TOP-REAL 2))
Indices (GoB (Rotate (k,C))) is set
(Rotate (k,C)) /. 1 is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (1 + 1) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(1 + 1) + (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
((1 + 1) + (C .. k)) -' (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (((1 + 1) + (C .. k)) -' (C .. k)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
((C .. k) + 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(((C .. k) + 1) + 1) -' (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. ((((C .. k) + 1) + 1) -' (C .. k)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
f is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
[f,G] is set
{f,G} is non empty V93() V94() V95() V96() V97() V98() set
{f} is non empty V93() V94() V95() V96() V97() V98() set
{{f,G},{f}} is non empty set
n is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
c8 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
[n,c8] is set
{n,c8} is non empty V93() V94() V95() V96() V97() V98() set
{n} is non empty V93() V94() V95() V96() V97() V98() set
{{n,c8},{n}} is non empty set
(GoB (Rotate (k,C))) * (f,G) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(GoB (Rotate (k,C))) * (n,c8) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
G + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),(f -' 1),G) is Element of K6( the U1 of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),f,G) is Element of K6( the U1 of (TOP-REAL 2))
n + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
c8 -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),n,(c8 -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
c8 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),f,c8) is Element of K6( the U1 of (TOP-REAL 2))
GoB k is V13() non empty-yielding V16( NAT ) V17(K286( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K286( the U1 of (TOP-REAL 2))
len (Rotate (k,C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (len k) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(C .. k) + (len k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
((C .. k) + (len k)) -' (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (((C .. k) + (len k)) -' (C .. k)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
k /. (C .. k) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(GoB k) * (f,G) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
k /. ((C .. k) + 1) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(GoB k) * (n,c8) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
cell ((GoB k),(f -' 1),G) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),f,G) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),n,(c8 -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),f,c8) is Element of K6( the U1 of (TOP-REAL 2))
len (Rotate (k,C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
k is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng k is V2() Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
C .. k is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
right_cell (k,(C .. k)) is Element of K6( the U1 of (TOP-REAL 2))
Rotate (k,C) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
right_cell ((Rotate (k,C)),1) is Element of K6( the U1 of (TOP-REAL 2))
len k is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(C .. k) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
GoB (Rotate (k,C)) is V13() non empty-yielding V16( NAT ) V17(K286( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K286( the U1 of (TOP-REAL 2))
Indices (GoB (Rotate (k,C))) is set
(Rotate (k,C)) /. 1 is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (1 + 1) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(1 + 1) + (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
((1 + 1) + (C .. k)) -' (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (((1 + 1) + (C .. k)) -' (C .. k)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
((C .. k) + 1) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(((C .. k) + 1) + 1) -' (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. ((((C .. k) + 1) + 1) -' (C .. k)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
f is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
G is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
[f,G] is set
{f,G} is non empty V93() V94() V95() V96() V97() V98() set
{f} is non empty V93() V94() V95() V96() V97() V98() set
{{f,G},{f}} is non empty set
n is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
c8 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
[n,c8] is set
{n,c8} is non empty V93() V94() V95() V96() V97() V98() set
{n} is non empty V93() V94() V95() V96() V97() V98() set
{{n,c8},{n}} is non empty set
(GoB (Rotate (k,C))) * (f,G) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(GoB (Rotate (k,C))) * (n,c8) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
G + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),f,G) is Element of K6( the U1 of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
G -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),f,(G -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
n + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),n,c8) is Element of K6( the U1 of (TOP-REAL 2))
c8 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
cell ((GoB (Rotate (k,C))),(f -' 1),c8) is Element of K6( the U1 of (TOP-REAL 2))
GoB k is V13() non empty-yielding V16( NAT ) V17(K286( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K286( the U1 of (TOP-REAL 2))
len (Rotate (k,C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (len k) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(C .. k) + (len k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
((C .. k) + (len k)) -' (C .. k) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Rotate (k,C)) /. (((C .. k) + (len k)) -' (C .. k)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
k /. (C .. k) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(GoB k) * (f,G) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
k /. ((C .. k) + 1) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(GoB k) * (n,c8) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
cell ((GoB k),f,G) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),f,(G -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),n,c8) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),(f -' 1),c8) is Element of K6( the U1 of (TOP-REAL 2))
len (Rotate (k,C)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
i is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
k is non empty connected bounded compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
W-min k is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
W-bound k is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | k is strict 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 K6(K7( the U1 of (TOP-REAL 2),REAL))
proj1 | k is V13() V16( the U1 of ((TOP-REAL 2) | k)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | k), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | k),REAL))
the U1 of ((TOP-REAL 2) | k) is set
K7( the U1 of ((TOP-REAL 2) | k),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | k),REAL)) is set
lower_bound (proj1 | k) is V11() V12() ext-real Element of REAL
(proj1 | k) .: the U1 of ((TOP-REAL 2) | k) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj1 | k) .: the U1 of ((TOP-REAL 2) | k)) is V11() V12() ext-real Element of REAL
W-most k is Element of K6( the U1 of (TOP-REAL 2))
SW-corner k is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
S-bound k is V11() V12() ext-real Element of REAL
proj2 | k is V13() V16( the U1 of ((TOP-REAL 2) | k)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | k), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | k),REAL))
lower_bound (proj2 | k) is V11() V12() ext-real Element of REAL
(proj2 | k) .: the U1 of ((TOP-REAL 2) | k) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | k) .: the U1 of ((TOP-REAL 2) | k)) is V11() V12() ext-real Element of REAL
|[(W-bound k),(S-bound k)]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
NW-corner k is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-bound k is V11() V12() ext-real Element of REAL
upper_bound (proj2 | k) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | k) .: the U1 of ((TOP-REAL 2) | k)) is V11() V12() ext-real Element of REAL
|[(W-bound k),(N-bound k)]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner k),(NW-corner k)) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner k),(NW-corner k))) /\ k is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most k) is strict SubSpace of TOP-REAL 2
proj2 | (W-most k) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most k))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most k)), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most k)),REAL))
the U1 of ((TOP-REAL 2) | (W-most k)) is set
K7( the U1 of ((TOP-REAL 2) | (W-most k)),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most k)),REAL)) is set
lower_bound (proj2 | (W-most k)) is V11() V12() ext-real Element of REAL
(proj2 | (W-most k)) .: the U1 of ((TOP-REAL 2) | (W-most k)) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | (W-most k)) .: the U1 of ((TOP-REAL 2) | (W-most k))) is V11() V12() ext-real Element of REAL
|[(W-bound k),(lower_bound (proj2 | (W-most k)))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
Cage (k,i) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (k,i)) is non empty boundary connected bounded being_simple_closed_curve compact Element of K6( the U1 of (TOP-REAL 2))
W-min (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Cage (k,i))) is strict SubSpace of TOP-REAL 2
proj1 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is set
K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL)) is set
lower_bound (proj1 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj1 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
W-most (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
SW-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Cage (k,i))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))),REAL))
lower_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
(proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i)))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(S-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (k,i))) is V11() V12() ext-real Element of REAL
upper_bound (proj2 | (L~ (Cage (k,i)))) is V11() V12() ext-real Element of REAL
upper_bound ((proj2 | (L~ (Cage (k,i)))) .: the U1 of ((TOP-REAL 2) | (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(N-bound (L~ (Cage (k,i))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ (Cage (k,i)))),(NW-corner (L~ (Cage (k,i))))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ (Cage (k,i)))),(NW-corner (L~ (Cage (k,i)))))) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ (Cage (k,i)))) is strict SubSpace of TOP-REAL 2
proj2 | (W-most (L~ (Cage (k,i)))) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i)))))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))),REAL)) is set
lower_bound (proj2 | (W-most (L~ (Cage (k,i))))) is V11() V12() ext-real Element of REAL
(proj2 | (W-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i))))) is V93() V94() V95() Element of K6(REAL)
lower_bound ((proj2 | (W-most (L~ (Cage (k,i))))) .: the U1 of ((TOP-REAL 2) | (W-most (L~ (Cage (k,i)))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Cage (k,i)))),(lower_bound (proj2 | (W-most (L~ (Cage (k,i))))))]| is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (k,i)),(W-min (L~ (Cage (k,i))))) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
right_cell ((Rotate ((Cage (k,i)),(W-min (L~ (Cage (k,i)))))),1) is Element of K6( the U1 of (TOP-REAL 2))
Gauge (k,i) is V13() non empty-yielding V16( NAT ) V17(K286( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K286( the U1 of (TOP-REAL 2))
width (Gauge (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
f is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Gauge (k,i)) * (1,f) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
len (Gauge (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(W-min (L~ (Cage (k,i)))) .. (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
rng (Cage (k,i)) is V2() Element of K6( the U1 of (TOP-REAL 2))
dom (Cage (k,i)) is V2() V93() V94() V95() V96() V97() V98() Element of K6(NAT)
(Cage (k,i)) . ((W-min (L~ (Cage (k,i)))) .. (Cage (k,i))) is set
(Cage (k,i)) /. ((W-min (L~ (Cage (k,i)))) .. (Cage (k,i))) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
len (Cage (k,i)) is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Cage (k,i)) /. 1 is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(Cage (k,i)) . 1 is set
[1,f] is set
{1,f} is non empty V93() V94() V95() V96() V97() V98() set
{1} is non empty V93() V94() V95() V96() V97() V98() set
{{1,f},{1}} is non empty set
Indices (Gauge (k,i)) is set
GoB (Cage (k,i)) is V13() non empty-yielding V16( NAT ) V17(K286( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K286( the U1 of (TOP-REAL 2))
Indices (GoB (Cage (k,i))) is set
((W-min (L~ (Cage (k,i)))) .. (Cage (k,i))) + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(GoB (Cage (k,i))) * (1,f) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(Cage (k,i)) /. (((W-min (L~ (Cage (k,i)))) .. (Cage (k,i))) + 1) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
c8 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
t is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
[c8,t] is set
{c8,t} is non empty V93() V94() V95() V96() V97() V98() set
{c8} is non empty V93() V94() V95() V96() V97() V98() set
{{c8,t},{c8}} is non empty set
(Gauge (k,i)) * (c8,t) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
((Cage (k,i)) /. (((W-min (L~ (Cage (k,i)))) .. (Cage (k,i))) + 1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * (1,f)) `1 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * (c8,t)) `1 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * (1,f)) `2 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * (c8,t)) `2 is V11() V12() ext-real Element of REAL
(GoB (Cage (k,i))) * (c8,t) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
1 - c8 is V11() V12() ext-real Element of REAL
abs (1 - c8) is V11() V12() ext-real Element of REAL
f - t is V11() V12() ext-real Element of REAL
abs (f - t) is V11() V12() ext-real Element of REAL
(abs (1 - c8)) + (abs (f - t)) is V11() V12() ext-real Element of REAL
0 + (abs (f - t)) is V11() V12() ext-real Element of REAL
f + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Gauge (k,i)) * (1,(f + 1)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
[1,(f + 1)] is set
{1,(f + 1)} is non empty V93() V94() V95() V96() V97() V98() set
{{1,(f + 1)},{1}} is non empty set
right_cell ((Cage (k,i)),((W-min (L~ (Cage (k,i)))) .. (Cage (k,i))),(Gauge (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
cell ((Gauge (k,i)),1,f) is Element of K6( the U1 of (TOP-REAL 2))
(Gauge (k,i)) * (2,(f + 1)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
((Gauge (k,i)) * (2,(f + 1))) `1 is V11() V12() ext-real Element of REAL
1 + 1 is V4() V5() V6() V10() V11() V12() V37() ext-real V92() V93() V94() V95() V96() V97() V98() Element of NAT
(Gauge (k,i)) * ((1 + 1),f) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(Gauge (k,i)) * ((1 + 1),(f + 1)) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (k,i)) * ((1 + 1),f)),((Gauge (k,i)) * ((1 + 1),(f + 1)))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(Gauge (k,i)) * (2,f) is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (k,i)) * (2,f)),((Gauge (k,i)) * (2,(f + 1)))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
((Gauge (k,i)) * (2,f)) `1 is V11() V12() ext-real Element of REAL
(W-min k) `1 is V11() V12() ext-real Element of REAL
(W-min k) `2 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * (2,(f + 1))) `2 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * (2,f)) `2 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * (1,(f + 1))) `2 is V11() V12() ext-real Element of REAL
(cell ((Gauge (k,i)),1,f)) /\ k is Element of K6( the U1 of (TOP-REAL 2))
s is set
a is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
a `1 is V11() V12() ext-real Element of REAL
((Gauge (k,i)) * ((1 + 1),f)) `1 is V11() V12() ext-real Element of REAL
a `2 is V11() V12() ext-real Element of REAL
west_halfline (W-min k) is Element of K6( the U1 of (TOP-REAL 2))
s is set
a is V33(2) FinSequence-like V84() Element of the U1 of (TOP-REAL 2)
(west_halfline (W-min k)) /\ (L~ (Cage (k,i))) is Element of K6( the U1 of (TOP-REAL 2))
a `1 is V11() V12() ext-real Element of REAL
(W-min (L~ (Cage (k,i)))) `2 is V11() V12() ext-real Element of REAL
a `2 is V11() V12() ext-real Element of REAL
((