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