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() by Def23; :: thesis: ex es being Subset of (W .edgeSeq() ) st W .edgeSeq() = Seq es
reconsider es = W .edgeSeq() as Subset of (W .edgeSeq() ) by GRAPH_2:28;
take es ; :: thesis: W .edgeSeq() = Seq es
thus W .edgeSeq() = Seq es by FINSEQ_3:125; :: thesis: verum