let G be Graph; :: thesis: {} is oriented Simple Chain of G
consider v being Element of the carrier of G;
set vs = <*v*>;
A1: <*v*> is_oriented_vertex_seq_of {} by GRAPH_4:9;

now

let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len <*v*> & <*v*> . n = <*v*> . m implies ( n = 1 & m = len <*v*> ) )
assume A2: ( 1 <= n & n < m & m <= len <*v*> & <*v*> . n = <*v*> . m ) ; :: thesis: ( n = 1 & m = len <*v*> )
assume ( not n = 1 or not m = len <*v*> ) ; :: thesis: contradiction
len <*v*> = 1 by FINSEQ_1:56;
hence contradiction by A2, XXREAL_0:2; :: thesis: verum

end;

hence {} is oriented Simple Chain of G by A1, GRAPH_1:14, GRAPH_4:def 7; :: thesis: verum