let G be Graph; :: thesis: for sc being oriented simple Chain of G
for sc' being oriented Chain of G st sc' = sc holds
sc' is Simple
let sc be oriented simple Chain of G; :: thesis: for sc' being oriented Chain of G st sc' = sc holds
sc' is Simple
let sc' be oriented Chain of G; :: thesis: ( sc' = sc implies sc' is Simple )
assume A1: sc' = sc ; :: thesis: sc' is Simple
consider vs being FinSequence of the carrier of G such that
A2: vs is_oriented_vertex_seq_of sc' by Th10;
vs is_vertex_seq_of sc by A1, A2, Th5;
then 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 GRAPH_2:51;
hence sc' is Simple by A2, Def7; :: thesis: verum