let G be Graph; :: thesis: for sc' being oriented Simple Chain of G holds sc' is oriented simple Chain of G
let sc' be oriented Simple Chain of G; :: thesis: sc' is oriented simple Chain of G
consider vs being FinSequence of the carrier of G such that
A1: vs is_oriented_vertex_seq_of sc' and
A2: for n, m being Element of 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 sc' by A1, Th5;
hence sc' is oriented simple Chain of G by A2, GRAPH_2:def 10; :: thesis: verum