:: JORDAN15 semantic presentation

REAL is non empty V32() V168() V169() V170() V174() V266() set
NAT is V168() V169() V170() V171() V172() V173() V174() V266() Element of K6(REAL)
K6(REAL) is set
omega is V168() V169() V170() V171() V172() V173() V174() V266() set
K6(omega) is set
K6(NAT) is set
COMPLEX is non empty V32() V168() V174() set
RAT is non empty V32() V168() V169() V170() V171() V174() set
INT is non empty V32() V168() V169() V170() V171() V172() V174() set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
K305() is set
1 is non empty ordinal natural V11() real ext-real positive non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
2 is non empty ordinal natural V11() real ext-real positive non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
K7(2,2) is set
K7(K7(2,2),2) is set
K6(K7(K7(2,2),2)) is set
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(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty non trivial TopSpace-like T_2 V105() V130() V131() V132() V133() V134() V135() V136() strict add-continuous Mult-continuous RLTopStruct
the U1 of (TOP-REAL 2) is non empty non trivial functional set
K295( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M9( 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,REAL) is set
K6(K7(COMPLEX,REAL)) is set
ExtREAL is non empty V169() set
{} is empty Function-like functional FinSequence-membered V168() V169() V170() V171() V172() V173() V174() set
the empty Function-like functional FinSequence-membered V168() V169() V170() V171() V172() V173() V174() set is empty Function-like functional FinSequence-membered V168() V169() V170() V171() V172() V173() V174() set
3 is non empty ordinal natural V11() real ext-real positive non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
Seg 1 is non empty V32() V39(1) V168() V169() V170() V171() V172() V173() Element of K6(NAT)
{1} is non empty V168() V169() V170() V171() V172() V173() set
Seg 2 is non empty V32() V39(2) V168() V169() V170() V171() V172() V173() Element of K6(NAT)
{1,2} is non empty V168() V169() V170() V171() V172() V173() set
Seg 3 is non empty V32() V39(3) V168() V169() V170() V171() V172() V173() Element of K6(NAT)
{1,2,3} is V168() V169() V170() V171() V172() V173() set
proj1 is V19() V22( the U1 of (TOP-REAL 2)) V23( REAL ) Function-like V46( the U1 of (TOP-REAL 2), REAL ) V205( TOP-REAL 2) Element of K6(K7( the U1 of (TOP-REAL 2),REAL))
proj2 is V19() V22( the U1 of (TOP-REAL 2)) V23( REAL ) Function-like V46( the U1 of (TOP-REAL 2), REAL ) V205( TOP-REAL 2) Element of K6(K7( the U1 of (TOP-REAL 2),REAL))
4 is non empty ordinal natural V11() real ext-real positive non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
0 is empty ordinal natural V11() real ext-real non positive non negative Function-like functional FinSequence-membered V43() V49() V168() V169() V170() V171() V172() V173() V174() Element of NAT
n is functional Element of K6( the U1 of (TOP-REAL 2))
C is functional Element of K6( the U1 of (TOP-REAL 2))
proj1 .: n is V168() V169() V170() Element of K6(REAL)
proj1 .: C is V168() V169() V170() Element of K6(REAL)
i is set
j is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
j `1 is V11() real ext-real Element of REAL
proj1 . j is set
n is functional Element of K6( the U1 of (TOP-REAL 2))
C is functional Element of K6( the U1 of (TOP-REAL 2))
proj1 .: n is V168() V169() V170() Element of K6(REAL)
proj1 .: C is V168() V169() V170() Element of K6(REAL)
i is real set
Horizontal_Line i is functional Element of K6( the U1 of (TOP-REAL 2))
j is set
k is V11() real ext-real Element of REAL
k is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
proj1 . k is set
k `2 is V11() real ext-real Element of REAL
G is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
proj1 . G is set
G `2 is V11() real ext-real Element of REAL
G `1 is V11() real ext-real Element of REAL
|[(G `1),(k `2)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
|[k,(k `2)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
|[(k `1),(k `2)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n is functional closed Element of K6( the U1 of (TOP-REAL 2))
proj1 .: n is V168() V169() V170() Element of K6(REAL)
Cl (proj1 .: n) is closed V168() V169() V170() Element of K6(REAL)
Cl n is functional Element of K6( the U1 of (TOP-REAL 2))
proj1 .: (Cl n) is V168() V169() V170() Element of K6(REAL)
n is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
proj1 .: n is V168() V169() V170() Element of K6(REAL)
n is V19() non empty-yielding V22( NAT ) V23(K295( the U1 of (TOP-REAL 2))) Function-like V32() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the U1 of (TOP-REAL 2))
len n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
width n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
C is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
i is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
j is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
n * (C,k) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * (C,k) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * (C,k)),(n * (C,k))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
n * (C,i) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * (C,j) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * (C,i)),(n * (C,j))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(n * (C,k)) `2 is V11() real ext-real Element of REAL
(n * (C,j)) `2 is V11() real ext-real Element of REAL
(n * (C,i)) `1 is V11() real ext-real Element of REAL
n * (C,1) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
(n * (C,1)) `1 is V11() real ext-real Element of REAL
(n * (C,j)) `1 is V11() real ext-real Element of REAL
(n * (C,i)) `2 is V11() real ext-real Element of REAL
(n * (C,k)) `2 is V11() real ext-real Element of REAL
(n * (C,k)) `1 is V11() real ext-real Element of REAL
(n * (C,k)) `1 is V11() real ext-real Element of REAL
n is V19() non empty-yielding V22( NAT ) V23(K295( the U1 of (TOP-REAL 2))) Function-like V32() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the U1 of (TOP-REAL 2))
width n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
len n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
C is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
i is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
j is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
n * (k,C) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * (k,C) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * (k,C)),(n * (k,C))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
n * (i,C) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * (j,C) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * (i,C)),(n * (j,C))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(n * (k,C)) `1 is V11() real ext-real Element of REAL
(n * (j,C)) `1 is V11() real ext-real Element of REAL
(n * (i,C)) `2 is V11() real ext-real Element of REAL
n * (1,C) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
(n * (1,C)) `2 is V11() real ext-real Element of REAL
(n * (j,C)) `2 is V11() real ext-real Element of REAL
(n * (i,C)) `1 is V11() real ext-real Element of REAL
(n * (k,C)) `1 is V11() real ext-real Element of REAL
(n * (k,C)) `2 is V11() real ext-real Element of REAL
(n * (k,C)) `2 is V11() real ext-real Element of REAL
n is V19() non empty-yielding V22( NAT ) V23(K295( the U1 of (TOP-REAL 2))) Function-like V32() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the U1 of (TOP-REAL 2))
width n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
Center n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
C is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
j is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
i is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
n * ((Center n),j) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * ((Center n),k) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * ((Center n),j)),(n * ((Center n),k))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
n * ((Center n),C) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * ((Center n),i) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * ((Center n),C)),(n * ((Center n),i))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
len n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
n is V19() non empty-yielding V22( NAT ) V23(K295( the U1 of (TOP-REAL 2))) Function-like V32() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the U1 of (TOP-REAL 2))
len n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
width n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
Center n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
C is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
j is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
i is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
n * (j,(Center n)) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * (k,(Center n)) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * (j,(Center n))),(n * (k,(Center n)))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
n * (C,(Center n)) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
n * (i,(Center n)) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((n * (C,(Center n))),(n * (i,(Center n)))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
C is non empty functional closed connected bounded compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
Gauge (C,n) is V19() non empty-yielding V22( NAT ) V23(K295( the U1 of (TOP-REAL 2))) Function-like V32() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the U1 of (TOP-REAL 2))
len (Gauge (C,n)) is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
Lower_Seq (C,n) is non empty non trivial V19() V22( NAT ) V23( the U1 of (TOP-REAL 2)) Function-like one-to-one V32() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
L~ (Lower_Seq (C,n)) is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
i is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
j is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
(Gauge (C,n)) * (i,j) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
(Gauge (C,n)) * (i,k) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
[i,k] is set
{i,k} is non empty V168() V169() V170() V171() V172() V173() set
{i} is non empty V168() V169() V170() V171() V172() V173() set
{{i,k},{i}} is non empty set
Indices (Gauge (C,n)) is set
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
(Gauge (C,n)) * (i,1) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,1)) `1 is V11() real ext-real Element of REAL
proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V168() V169() V170() Element of K6(REAL)
upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is V11() real ext-real Element of REAL
[i,j] is set
{i,j} is non empty V168() V169() V170() V171() V172() V173() set
{{i,j},{i}} is non empty set
Gik is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
(Gauge (C,n)) * (i,Gik) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,Gik)) `2 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,k)) `1 is V11() real ext-real Element of REAL
((Gauge (C,n)) * (i,j)) `1 is V11() real ext-real Element of REAL
LSeg (((Gauge (C,n)) * (i,Gik)),((Gauge (C,n)) * (i,k))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,Gik)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
{((Gauge (C,n)) * (i,Gik))} is non empty functional set
j1 is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
N-most j1 is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
NW-corner j1 is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
W-bound j1 is V11() real ext-real Element of REAL
(TOP-REAL 2) | j1 is strict T_2 compact SubSpace of TOP-REAL 2
proj1 | j1 is V19() V22( the U1 of ((TOP-REAL 2) | j1)) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | j1), REAL ) V205((TOP-REAL 2) | j1) Element of K6(K7( the U1 of ((TOP-REAL 2) | j1),REAL))
the U1 of ((TOP-REAL 2) | j1) is set
K7( the U1 of ((TOP-REAL 2) | j1),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | j1),REAL)) is set
lower_bound (proj1 | j1) is V11() real ext-real Element of REAL
(proj1 | j1) .: the U1 of ((TOP-REAL 2) | j1) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj1 | j1) .: the U1 of ((TOP-REAL 2) | j1)) is V11() real ext-real Element of REAL
N-bound j1 is V11() real ext-real Element of REAL
proj2 | j1 is V19() V22( the U1 of ((TOP-REAL 2) | j1)) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | j1), REAL ) V205((TOP-REAL 2) | j1) Element of K6(K7( the U1 of ((TOP-REAL 2) | j1),REAL))
upper_bound (proj2 | j1) is V11() real ext-real Element of REAL
(proj2 | j1) .: the U1 of ((TOP-REAL 2) | j1) is V168() V169() V170() Element of K6(REAL)
upper_bound ((proj2 | j1) .: the U1 of ((TOP-REAL 2) | j1)) is V11() real ext-real Element of REAL
|[(W-bound j1),(N-bound j1)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
NE-corner j1 is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
E-bound j1 is V11() real ext-real Element of REAL
upper_bound (proj1 | j1) is V11() real ext-real Element of REAL
upper_bound ((proj1 | j1) .: the U1 of ((TOP-REAL 2) | j1)) is V11() real ext-real Element of REAL
|[(E-bound j1),(N-bound j1)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner j1),(NE-corner j1)) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner j1),(NE-corner j1))) /\ j1 is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
Wbo is set
go is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,Gik)) `1 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 is V11() real ext-real Element of REAL
((Gauge (C,n)) * (i,k)) `2 is V11() real ext-real Element of REAL
N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V11() real ext-real Element of REAL
(TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is strict T_2 SubSpace of TOP-REAL 2
proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V19() V22( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))), REAL ) V205((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) Element of K6(K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),REAL))
the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is set
K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),REAL)) is set
upper_bound (proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is V11() real ext-real Element of REAL
(proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is V168() V169() V170() Element of K6(REAL)
upper_bound ((proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) is V11() real ext-real Element of REAL
N-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is functional Element of K6( the U1 of (TOP-REAL 2))
NW-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
W-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V11() real ext-real Element of REAL
proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V19() V22( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))), REAL ) V205((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) Element of K6(K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),REAL))
lower_bound (proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is V11() real ext-real Element of REAL
(proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) is V11() real ext-real Element of REAL
|[(W-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),(N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
NE-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
E-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is V11() real ext-real Element of REAL
upper_bound (proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is V11() real ext-real Element of REAL
upper_bound ((proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) is V11() real ext-real Element of REAL
|[(E-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),(N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),(NE-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))),(NE-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))) /\ ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) is V19() V22( the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))), REAL ) V205((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))),REAL))
the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) is set
K7( the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))),REAL)) is set
lower_bound (proj1 | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) is V11() real ext-real Element of REAL
(proj1 | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) .: the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj1 | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))) .: the U1 of ((TOP-REAL 2) | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))) is V11() real ext-real Element of REAL
|[(lower_bound (proj1 | (N-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))),(N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
(N-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) `2 is V11() real ext-real Element of REAL
go `2 is V11() real ext-real Element of REAL
go `1 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 is V11() real ext-real Element of REAL
LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
Gij is set
do is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
proj2 .: do is V168() V169() V170() Element of K6(REAL)
((Gauge (C,n)) * (i,j)) `2 is V11() real ext-real Element of REAL
LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
LA is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LA `2 is V11() real ext-real Element of REAL
proj2 . LA is set
pion is compact V168() V169() V170() Element of K6(REAL)
LA `1 is V11() real ext-real Element of REAL
n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
C is non empty functional closed connected bounded compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
Gauge (C,n) is V19() non empty-yielding V22( NAT ) V23(K295( the U1 of (TOP-REAL 2))) Function-like V32() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the U1 of (TOP-REAL 2))
len (Gauge (C,n)) is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
Upper_Seq (C,n) is non empty non trivial V19() V22( NAT ) V23( the U1 of (TOP-REAL 2)) Function-like one-to-one V32() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
L~ (Upper_Seq (C,n)) is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
i is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
j is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
(Gauge (C,n)) * (i,k) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
(Gauge (C,n)) * (i,j) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
[i,k] is set
{i,k} is non empty V168() V169() V170() V171() V172() V173() set
{i} is non empty V168() V169() V170() V171() V172() V173() set
{{i,k},{i}} is non empty set
Indices (Gauge (C,n)) is set
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
(Gauge (C,n)) * (i,1) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,1)) `1 is V11() real ext-real Element of REAL
proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V168() V169() V170() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V11() real ext-real Element of REAL
[i,j] is set
{i,j} is non empty V168() V169() V170() V171() V172() V173() set
{{i,j},{i}} is non empty set
Gik is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
(Gauge (C,n)) * (i,Gik) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,Gik)) `2 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,j)) `1 is V11() real ext-real Element of REAL
((Gauge (C,n)) * (i,k)) `1 is V11() real ext-real Element of REAL
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,Gik))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,Gik)))) /\ (L~ (Upper_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
{((Gauge (C,n)) * (i,Gik))} is non empty functional set
j1 is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
S-most j1 is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
SW-corner j1 is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
W-bound j1 is V11() real ext-real Element of REAL
(TOP-REAL 2) | j1 is strict T_2 compact SubSpace of TOP-REAL 2
proj1 | j1 is V19() V22( the U1 of ((TOP-REAL 2) | j1)) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | j1), REAL ) V205((TOP-REAL 2) | j1) Element of K6(K7( the U1 of ((TOP-REAL 2) | j1),REAL))
the U1 of ((TOP-REAL 2) | j1) is set
K7( the U1 of ((TOP-REAL 2) | j1),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | j1),REAL)) is set
lower_bound (proj1 | j1) is V11() real ext-real Element of REAL
(proj1 | j1) .: the U1 of ((TOP-REAL 2) | j1) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj1 | j1) .: the U1 of ((TOP-REAL 2) | j1)) is V11() real ext-real Element of REAL
S-bound j1 is V11() real ext-real Element of REAL
proj2 | j1 is V19() V22( the U1 of ((TOP-REAL 2) | j1)) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | j1), REAL ) V205((TOP-REAL 2) | j1) Element of K6(K7( the U1 of ((TOP-REAL 2) | j1),REAL))
lower_bound (proj2 | j1) is V11() real ext-real Element of REAL
(proj2 | j1) .: the U1 of ((TOP-REAL 2) | j1) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj2 | j1) .: the U1 of ((TOP-REAL 2) | j1)) is V11() real ext-real Element of REAL
|[(W-bound j1),(S-bound j1)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
SE-corner j1 is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
E-bound j1 is V11() real ext-real Element of REAL
upper_bound (proj1 | j1) is V11() real ext-real Element of REAL
upper_bound ((proj1 | j1) .: the U1 of ((TOP-REAL 2) | j1)) is V11() real ext-real Element of REAL
|[(E-bound j1),(S-bound j1)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner j1),(SE-corner j1)) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner j1),(SE-corner j1))) /\ j1 is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
Wbo is set
((Gauge (C,n)) * (i,Gik)) `1 is V11() real ext-real Element of REAL
((Gauge (C,n)) * (i,j)) `2 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `2 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `1 is V11() real ext-real Element of REAL
go is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
S-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V11() real ext-real Element of REAL
(TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is strict T_2 SubSpace of TOP-REAL 2
proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V19() V22( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))), REAL ) V205((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) Element of K6(K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),REAL))
the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is set
K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),REAL)) is set
lower_bound (proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V11() real ext-real Element of REAL
(proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj2 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) is V11() real ext-real Element of REAL
S-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is functional Element of K6( the U1 of (TOP-REAL 2))
SW-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
W-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V11() real ext-real Element of REAL
proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V19() V22( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))), REAL ) V205((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) Element of K6(K7( the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),REAL))
lower_bound (proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V11() real ext-real Element of REAL
(proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) is V11() real ext-real Element of REAL
|[(W-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),(S-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
SE-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
E-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V11() real ext-real Element of REAL
upper_bound (proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V11() real ext-real Element of REAL
upper_bound ((proj1 | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) .: the U1 of ((TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) is V11() real ext-real Element of REAL
|[(E-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),(S-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),(SE-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))),(SE-corner ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))) /\ ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V19() V22( the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))), REAL ) V205((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))),REAL))
the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))),REAL)) is set
lower_bound (proj1 | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) is V11() real ext-real Element of REAL
(proj1 | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) .: the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj1 | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))) .: the U1 of ((TOP-REAL 2) | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))) is V11() real ext-real Element of REAL
|[(lower_bound (proj1 | (S-most ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))),(S-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
(S-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) `2 is V11() real ext-real Element of REAL
go `2 is V11() real ext-real Element of REAL
go `1 is V11() real ext-real Element of REAL
LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
Gij is set
do is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
proj2 .: do is V168() V169() V170() Element of K6(REAL)
((Gauge (C,n)) * (i,k)) `2 is V11() real ext-real Element of REAL
LA is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LA `2 is V11() real ext-real Element of REAL
proj2 . LA is set
pion is compact V168() V169() V170() Element of K6(REAL)
LA `1 is V11() real ext-real Element of REAL
n is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
C is non empty functional closed connected bounded compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
Gauge (C,n) is V19() non empty-yielding V22( NAT ) V23(K295( the U1 of (TOP-REAL 2))) Function-like V32() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K295( the U1 of (TOP-REAL 2))
len (Gauge (C,n)) is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
Lower_Seq (C,n) is non empty non trivial V19() V22( NAT ) V23( the U1 of (TOP-REAL 2)) Function-like one-to-one V32() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
L~ (Lower_Seq (C,n)) is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
Upper_Seq (C,n) is non empty non trivial V19() V22( NAT ) V23( the U1 of (TOP-REAL 2)) Function-like one-to-one V32() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)
L~ (Upper_Seq (C,n)) is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
i is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
j is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
k is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
(Gauge (C,n)) * (i,j) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
(Gauge (C,n)) * (i,k) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
[i,j] is set
{i,j} is non empty V168() V169() V170() V171() V172() V173() set
{i} is non empty V168() V169() V170() V171() V172() V173() set
{{i,j},{i}} is non empty set
Indices (Gauge (C,n)) is set
(Gauge (C,n)) * (i,1) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,1)) `1 is V11() real ext-real Element of REAL
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) is V168() V169() V170() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) is V11() real ext-real Element of REAL
[i,k] is set
{i,k} is non empty V168() V169() V170() V171() V172() V173() set
{{i,k},{i}} is non empty set
pp is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
(Gauge (C,n)) * (i,pp) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,pp)) `2 is V11() real ext-real Element of REAL
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,pp))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,pp)))) /\ (L~ (Lower_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
Gik is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
N-most Gik is non empty functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
NW-corner Gik is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
W-bound Gik is V11() real ext-real Element of REAL
(TOP-REAL 2) | Gik is strict T_2 compact SubSpace of TOP-REAL 2
proj1 | Gik is V19() V22( the U1 of ((TOP-REAL 2) | Gik)) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | Gik), REAL ) V205((TOP-REAL 2) | Gik) Element of K6(K7( the U1 of ((TOP-REAL 2) | Gik),REAL))
the U1 of ((TOP-REAL 2) | Gik) is set
K7( the U1 of ((TOP-REAL 2) | Gik),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | Gik),REAL)) is set
lower_bound (proj1 | Gik) is V11() real ext-real Element of REAL
(proj1 | Gik) .: the U1 of ((TOP-REAL 2) | Gik) is V168() V169() V170() Element of K6(REAL)
lower_bound ((proj1 | Gik) .: the U1 of ((TOP-REAL 2) | Gik)) is V11() real ext-real Element of REAL
N-bound Gik is V11() real ext-real Element of REAL
proj2 | Gik is V19() V22( the U1 of ((TOP-REAL 2) | Gik)) V23( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | Gik), REAL ) V205((TOP-REAL 2) | Gik) Element of K6(K7( the U1 of ((TOP-REAL 2) | Gik),REAL))
upper_bound (proj2 | Gik) is V11() real ext-real Element of REAL
(proj2 | Gik) .: the U1 of ((TOP-REAL 2) | Gik) is V168() V169() V170() Element of K6(REAL)
upper_bound ((proj2 | Gik) .: the U1 of ((TOP-REAL 2) | Gik)) is V11() real ext-real Element of REAL
|[(W-bound Gik),(N-bound Gik)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
NE-corner Gik is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
E-bound Gik is V11() real ext-real Element of REAL
upper_bound (proj1 | Gik) is V11() real ext-real Element of REAL
upper_bound ((proj1 | Gik) .: the U1 of ((TOP-REAL 2) | Gik)) is V11() real ext-real Element of REAL
|[(E-bound Gik),(N-bound Gik)]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner Gik),(NE-corner Gik)) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner Gik),(NE-corner Gik))) /\ Gik is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
Wmin is set
Wbo is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (C,n)) * (i,j)),|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,j)),|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n)))) is V168() V169() V170() Element of K6(REAL)
upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))))) is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))))))]| is non empty V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,pp)) `1 is V11() real ext-real Element of REAL
[i,pp] is set
{i,pp} is non empty V168() V169() V170() V171() V172() V173() set
{{i,pp},{i}} is non empty set
pion is ordinal natural V11() real ext-real non negative V43() V49() V168() V169() V170() V171() V172() V173() Element of NAT
(Gauge (C,n)) * (i,pion) is V19() V22( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V160() Element of the U1 of (TOP-REAL 2)
((Gauge (C,n)) * (i,pion)) `2 is V11() real ext-real Element of REAL
{((Gauge (C,n)) * (i,pion))} is non empty functional set
LSeg (((Gauge (C,n)) * (i,pion)),((Gauge (C,n)) * (i,pp))) is non empty functional closed closed connected bounded bounded compact compact V264( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,pion)),((Gauge (C,n)) * (i,pp)))) /\ (L~ (Lower_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((Gauge (C,n)) * (i,pion)),((Gauge (C,n)) * (i,pp)))) /\ (L~ (Upper_Seq (C,n))) is functional closed bounded compact Element of K6( the U1 of (TOP-REAL 2))
{((Gauge (C,n)) * (i,pp))} is non empty functional set
((Gauge (C,n)) * (i,pion)) `1 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))))))]| `2 is V11() real ext-real Element of REAL
|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `2 is V11() real ext-real Element of REAL
N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,pp)))) /\ (L~ (Lower_Seq (C,n)))) is V11() real ext-real Element of REAL
(TOP-REAL 2) | ((LSeg (((Gauge (C,n)) * (i,