:: GOBOARD9 semantic presentation

begin

theorem :: GOBOARD9:1
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A1, A2, B being ( ( ) ( ) Subset of ) st A1 : ( ( ) ( ) Subset of ) is_a_component_of B : ( ( ) ( ) Subset of ) & A2 : ( ( ) ( ) Subset of ) is_a_component_of B : ( ( ) ( ) Subset of ) & not A1 : ( ( ) ( ) Subset of ) = A2 : ( ( ) ( ) Subset of ) holds
A1 : ( ( ) ( ) Subset of ) misses A2 : ( ( ) ( ) Subset of ) ;

theorem :: GOBOARD9:2
for GX being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of )
for AA being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = AA : ( ( ) ( ) Subset of ) holds
GX : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | A : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) = (GX : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | B : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) | AA : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ) ;

theorem :: GOBOARD9:3
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B being ( ( non empty ) ( non empty ) Subset of ) st A : ( ( non empty ) ( non empty ) Subset of ) c= B : ( ( non empty ) ( non empty ) Subset of ) & A : ( ( non empty ) ( non empty ) Subset of ) is connected holds
ex C being ( ( ) ( ) Subset of ) st
( C : ( ( ) ( ) Subset of ) is_a_component_of B : ( ( non empty ) ( non empty ) Subset of ) & A : ( ( non empty ) ( non empty ) Subset of ) c= C : ( ( ) ( ) Subset of ) ) ;

theorem :: GOBOARD9:4
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B, C, D being ( ( ) ( ) Subset of ) st B : ( ( ) ( ) Subset of ) is connected & C : ( ( ) ( ) Subset of ) is_a_component_of D : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) c= C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) meets B : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) c= D : ( ( ) ( ) Subset of ) holds
B : ( ( ) ( ) Subset of ) c= C : ( ( ) ( ) Subset of ) ;

registration
cluster non empty convex for ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: GOBOARD9:5
canceled;

theorem :: GOBOARD9:6
for P, Q being ( ( convex ) ( connected convex ) Subset of ) holds P : ( ( convex ) ( connected convex ) Subset of ) /\ Q : ( ( convex ) ( connected convex ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: GOBOARD9:7
for f being ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) holds Rev (X_axis f : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) = X_axis (Rev f : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) ;

theorem :: GOBOARD9:8
for f being ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) holds Rev (Y_axis f : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) = Y_axis (Rev f : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) ;

registration
cluster V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like for ( ( ) ( ) set ) ;
end;

registration
let f be ( ( V13() Function-like non constant FinSequence-like ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like ) FinSequence) ;
cluster Rev f : ( ( V13() Function-like non constant FinSequence-like ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like ) set ) : ( ( V13() Function-like FinSequence-like ) ( V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V26() FinSequence-like FinSubsequence-like ) set ) -> V13() Function-like non constant FinSequence-like ;
end;

definition
let f be ( ( non empty V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ;
:: original: Rev
redefine func Rev f -> ( ( non empty V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ;
end;

theorem :: GOBOARD9:9
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for i, j being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) = len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
left_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = right_cell ((Rev f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( non empty V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: GOBOARD9:10
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for i, j being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) = len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
left_cell ((Rev f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( non empty V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = right_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: GOBOARD9:11
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for k being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex i, j being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st
( i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len (GoB f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( tabular ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) FinSequence of K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= width (GoB f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( tabular ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) FinSequence of K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & cell ((GoB f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( tabular ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) FinSequence of K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ,i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = left_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: GOBOARD9:12
for j being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) 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 ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= width G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (h_strip (G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ,j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: GOBOARD9:13
for i being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) 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 ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() 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 : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (v_strip (G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ,i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: GOBOARD9:14
for i, j being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) 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 ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() 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 : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= width G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (cell (G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ,i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) ;

theorem :: GOBOARD9:15
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for k being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (left_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) ;

theorem :: GOBOARD9:16
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for k being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (right_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) ;

theorem :: GOBOARD9:17
for i, j being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) 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 ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() 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 : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= width G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (cell (G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ,i : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: GOBOARD9:18
canceled;

theorem :: GOBOARD9:19
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for k being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (left_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: GOBOARD9:20
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for k being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (right_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is convex ;

definition
let f be ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ;
func LeftComp f -> ( ( ) ( ) Subset of ) means :: GOBOARD9:def 1
( it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) is_a_component_of (L~ f : ( ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) RLTopStruct ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Int (left_cell (f : ( ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) RLTopStruct ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) );
func RightComp f -> ( ( ) ( ) Subset of ) means :: GOBOARD9:def 2
( it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) is_a_component_of (L~ f : ( ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) RLTopStruct ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Int (right_cell (f : ( ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() add-continuous Mult-continuous ) RLTopStruct ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) );
end;

theorem :: GOBOARD9:21
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for k being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (left_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= LeftComp f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( ) Subset of ) ;

theorem :: GOBOARD9:22
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) holds GoB (Rev f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( non empty V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( tabular ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) FinSequence of K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) = GoB f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( tabular ) ( V13() non empty-yielding V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17(K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) FinSequence of K247( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ;

theorem :: GOBOARD9:23
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) holds RightComp f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( ) Subset of ) = LeftComp (Rev f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( non empty V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( ) Subset of ) ;

theorem :: GOBOARD9:24
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) holds RightComp (Rev f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ) : ( ( non empty V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( ) Subset of ) = LeftComp f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( ) Subset of ) ;

theorem :: GOBOARD9:25
for f being ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence)
for k being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) <= len f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Int (right_cell (f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) ,k : ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= RightComp f : ( ( non empty non constant V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) ( non empty V13() V16( NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() ) Element of K6(REAL : ( ( ) ( non empty V26() V92() V93() V94() V98() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard ) special_circular_sequence) : ( ( ) ( ) Subset of ) ;