let G be Graph; :: thesis: for sc9 being oriented Simple Chain of G holds sc9 is oriented simple Chain of G
let sc9 be oriented Simple Chain of G; :: thesis: sc9 is oriented simple Chain of G
consider vs being FinSequence of the carrier of G such that
A1: vs is_oriented_vertex_seq_of sc9 and
A2: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by Def7;
vs is_vertex_seq_of sc9 by A1, Th4;
hence sc9 is oriented simple Chain of G by A2, GRAPH_2:def 9; :: thesis: verum