:: deftheorem defines is_split_at GRAPH_2:def 13 :
for F being FinSequence of INT
for n being Nat holds
( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds
F . i <= F . j );