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' & ( 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 A1, GRAPH_2:def 10; :: thesis: verum