theorem Th18: :: GLIB_003:18

for G being real-weighted WGraph
for W1 being Walk of G
for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws