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