reconsider es = W .edgeSeq() as Subset of (W .edgeSeq()) by FINSEQ_6:152;
take W ; :: thesis: ( W is_Walk_from W .first() ,W .last() & ex es being Subset of (W .edgeSeq()) st W .edgeSeq() = Seq es )
thus W is_Walk_from W .first() ,W .last() ; :: thesis: ex es being Subset of (W .edgeSeq()) st W .edgeSeq() = Seq es
take es ; :: thesis: W .edgeSeq() = Seq es
thus W .edgeSeq() = Seq es by FINSEQ_3:116; :: thesis: verum