JORDAN8

:: JORDAN8 semantic presentation

for D being ( ( ) ( ) set )
for G being ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₁ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₁ : ( ( ) ( ) set ) )) ) holds <*> D : ( ( ) ( ) set ) : ( ( ) ( V1() non-empty empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₁ : ( ( ) ( ) set ) ) Function-like functional empty V28() FinSequence-like FinSubsequence-like FinSequence-membered V75() V76() V77() V78() V86() V87() V88() V89() V90() V91() V92() ) FinSequence of b₁ : ( ( ) ( ) set ) ) is_sequence_on G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₁ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₁ : ( ( ) ( ) set ) )) ) ;

theorem :: JORDAN8:2

for m being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) )
for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for G being ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( non empty ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( non empty ) ( non empty ) set ) )) ) st f : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of b₂ : ( ( non empty ) ( non empty ) set ) ) is_sequence_on G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( non empty ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( non empty ) ( non empty ) set ) )) ) holds
f : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of b₂ : ( ( non empty ) ( non empty ) set ) ) /^ m : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of b₂ : ( ( non empty ) ( non empty ) set ) ) is_sequence_on G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( non empty ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( non empty ) ( non empty ) set ) )) ) ;

theorem :: JORDAN8:3

for k being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) )
for D being ( ( ) ( ) set )
for f being ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( ) ( ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( ) ( ) set ) )
for G being ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) st 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= len f : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( ) ( ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of b₂ : ( ( ) ( ) set ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & f : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( ) ( ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of b₂ : ( ( ) ( ) set ) ) is_sequence_on G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) holds
ex i1, j1, i2, j2 being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) st
( [i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) & f : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( ) ( ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of b₂ : ( ( ) ( ) set ) ) /. k : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( ) ( ) set ) ) = G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) * (i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of b₂ : ( ( ) ( ) set ) ) & [i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) & f : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(b₂ : ( ( ) ( ) set ) ) Function-like V28() FinSequence-like FinSubsequence-like ) FinSequence of b₂ : ( ( ) ( ) set ) ) /. (k : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( ) ( ) set ) ) = G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274(b₂ : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ( ( ) ( functional non empty FinSequence-membered ) M11(b₂ : ( ( ) ( ) set ) )) ) * (i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of b₂ : ( ( ) ( ) set ) ) & ( ( i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) or ( i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) or ( i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) or ( i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) ) ) ;

theorem :: JORDAN8:4

theorem :: JORDAN8:5

theorem :: JORDAN8:6

for G being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board)
for p being ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( non empty ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like non empty V28() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st f : ( ( non empty ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like non empty V28() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is_sequence_on G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) & ex i, j being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) st
( [i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & p : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Point of ( ( ) ( non empty ) set ) ) = G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) ) & ( for i1, j1, i2, j2 being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) st [i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & [i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & f : ( ( non empty ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like non empty V28() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. (len f : ( ( non empty ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like non empty V28() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) = G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) & p : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Point of ( ( ) ( non empty ) set ) ) = G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) holds
(abs (i2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) - i1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() ext-real ) set ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) + (abs (j2 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) - j1 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() ext-real ) set ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) = 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) holds
f : ( ( non empty ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like non empty V28() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ^ <*p : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Point of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like non empty V28() V35(1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like non empty V28() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) is_sequence_on G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ;

theorem :: JORDAN8:7

for i, k, j being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) )
for G being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + k : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) < len G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) < width G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & cell (G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ,i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) meets cell (G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ,(i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) + k : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
k : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN8:8

for C being ( ( non empty compact ) ( non empty compact ) Subset of ) holds
( C : ( ( non empty compact ) ( non empty compact ) Subset of ) is vertical iff E-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) <= W-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) ;

theorem :: JORDAN8:9

for C being ( ( non empty compact ) ( non empty compact ) Subset of ) holds
( C : ( ( non empty compact ) ( non empty compact ) Subset of ) is horizontal iff N-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) <= S-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) ;

definition

let C be ( ( ) ( ) Subset of ) ;
let n be ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ;

func Gauge (C,n) -> ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ) means :: JORDAN8:def 1
( len it : ( ( ) ( ) Element of C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = (2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( ) ( ) Element of bool (bool C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) + 3 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & len it : ( ( ) ( ) Element of C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) = width it : ( ( ) ( ) Element of C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & ( for i, j being ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) st [i : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ,j : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ] : ( ( ) ( ) set ) in Indices it : ( ( ) ( ) Element of C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) Element of C : ( ( ) ( ) TopStruct ) ) * (i : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ,j : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) = |[((W-bound C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) + ((((E-bound C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) - (W-bound C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) / (2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( ) ( ) Element of bool (bool C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of COMPLEX : ( ( ) ( V86() V92() ) set ) ) * (i : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) - 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ,((S-bound C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) + ((((N-bound C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) - (S-bound C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) / (2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) |^ n : ( ( ) ( ) Element of bool (bool C : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of COMPLEX : ( ( ) ( V86() V92() ) set ) ) * (j : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) - 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ]| : ( ( ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) Function-like non empty V28() V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V75() V76() V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) ) );

end;

registration

let C be ( ( non empty ) ( non empty ) Subset of ) ;
let n be ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ;

cluster Gauge (C : ( ( non empty ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) set ) ) : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular ) Matrix of ) -> V3() tabular X_equal-in-line Y_equal-in-column ;

end;

registration

let C be ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ;
let n be ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ;

cluster Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) set ) ) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) -> tabular Y_increasing-in-line X_increasing-in-column ;

end;

theorem :: JORDAN8:10

for T being ( ( non empty ) ( non empty ) Subset of )
for n being ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) holds len (Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) >= 4 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN8:11

for j, n being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) )
for T being ( ( non empty ) ( non empty ) Subset of ) st 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= len (Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
((Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) * (2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) = W-bound T : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ;

theorem :: JORDAN8:12

for j, n being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) )
for T being ( ( non empty ) ( non empty ) Subset of ) st 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= len (Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
((Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) * (((len (Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) -' 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) = E-bound T : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ;

theorem :: JORDAN8:13

for i, n being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) )
for T being ( ( non empty ) ( non empty ) Subset of ) st 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= len (Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
((Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) * (i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) = S-bound T : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ;

theorem :: JORDAN8:14

for i, n being ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) )
for T being ( ( non empty ) ( non empty ) Subset of ) st 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) <= len (Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
((Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) * (i : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,((len (Gauge (T : ( ( non empty ) ( non empty ) Subset of ) ,n : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) -' 1 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V35(2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V77() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) = N-bound T : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( V21() V22() ext-real ) Element of REAL : ( ( ) ( V86() V87() V88() V92() ) set ) ) ;

theorem :: JORDAN8:15

for C being ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of )
for i, n being ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) st i : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) <= len (Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
cell ((Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,i : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ,(len (Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) misses C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ;

theorem :: JORDAN8:16

for C being ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of )
for j, n being ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) st j : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) <= len (Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
cell ((Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,(len (Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) misses C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ;

theorem :: JORDAN8:17

for C being ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of )
for i, n being ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) st i : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) <= len (Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
cell ((Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,i : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ,0 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) misses C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ;

theorem :: JORDAN8:18

for C being ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of )
for j, n being ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) st j : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) <= len (Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) holds
cell ((Gauge (C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ,n : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) )) : ( ( tabular ) ( V1() V3() V4( NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) V5(K274( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) )) ) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,0 : ( ( ) ( V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ,j : ( ( V20() ) ( V16() V20() V21() V22() ext-real non negative ) Nat) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() ) Element of NAT : ( ( ) ( V86() V87() V88() V89() V90() V91() V92() ) Element of bool REAL : ( ( ) ( V86() V87() V88() V92() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V161() ) ( non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() ) L15()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) misses C : ( ( non empty compact non horizontal non vertical ) ( non empty compact non horizontal non vertical ) Subset of ) ;