let G be Graph; :: thesis: for e being set st e in the carrier' of G holds
<*e*> is Path of G
let e be set ; :: thesis: ( e in the carrier' of G implies <*e*> is Path of G )
assume e in the carrier' of G ; :: thesis: <*e*> is Path of G
then reconsider c = <*e*> as Chain of G by MSSCYC_1:5;
now :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len c holds
c . n <> c . m
let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len c implies c . n <> c . m )
A1: len c = 1 by FINSEQ_1:39;
assume ( 1 <= n & n < m & m <= len c ) ; :: thesis: c . n <> c . m
hence c . n <> c . m by A1, XXREAL_0:2; :: thesis: verum
end;
hence <*e*> is Path of G by GRAPH_1:def 16; :: thesis: verum