:: JORDAN13 semantic presentation

begin

definition
let C be ( ( non empty non horizontal non vertical being_simple_closed_curve ) ( non empty connected bounded V189( TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) ) non horizontal non vertical being_simple_closed_curve ) Subset of ) ;
let n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;
assume n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) is_sufficiently_large_for C : ( ( non empty non horizontal non vertical being_simple_closed_curve ) ( non empty connected bounded V189( TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) ) non horizontal non vertical being_simple_closed_curve ) Subset of ) ;
func Span (C,n) -> ( ( non empty non constant V179( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard clockwise_oriented ) ( non empty V2() Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non constant V26() FinSequence-like FinSubsequence-like V179( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) special unfolded s.c.c. standard clockwise_oriented ) special_circular_sequence) means :: JORDAN13:def 1
( it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) is_sequence_on Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) & it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) /. 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like V136() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = (Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) * ((X-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(Y-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like V136() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) & it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) /. 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like V136() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = (Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) * (((X-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(Y-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) -element FinSequence-like V136() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) & ( for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= len it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ( front_right_cell (it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) misses C : ( ( ) ( ) RLTopStruct ) & front_left_cell (it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) misses C : ( ( ) ( ) RLTopStruct ) implies it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) turns_left k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) , Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) & ( front_right_cell (it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) misses C : ( ( ) ( ) RLTopStruct ) & front_left_cell (it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) meets C : ( ( ) ( ) RLTopStruct ) implies it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) goes_straight k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) , Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) & ( front_right_cell (it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ,k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) meets C : ( ( ) ( ) RLTopStruct ) implies it : ( ( Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like Function-like V40(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) turns_right k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) , Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V26() FinSequence-like FinSubsequence-like tabular ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M11( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) ) ) ) ) );
end;