let G be Graph; :: thesis: for v1, v2 being Vertex of G
for c being Chain of G holds c is Chain of AddNewEdge v1,v2
let v1, v2 be Vertex of G; :: thesis: for c being Chain of G holds c is Chain of AddNewEdge v1,v2
let c be Chain of G; :: thesis: c is Chain of AddNewEdge v1,v2
set G' = AddNewEdge v1,v2;
A1: the carrier' of (AddNewEdge v1,v2) = the carrier' of G \/ {the carrier' of G} by Def7;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then ( rng c c= the carrier' of G & the carrier' of G c= the carrier' of (AddNewEdge v1,v2) ) by A1, FINSEQ_1:def 4, XBOOLE_1:7;
then rng c c= the carrier' of (AddNewEdge v1,v2) by XBOOLE_1:1;
hence c is FinSequence of the carrier' of (AddNewEdge v1,v2) by FINSEQ_1:def 4; :: according to MSSCYC_1:def 1 :: thesis: ex b₁ being FinSequence of the carrier of (AddNewEdge v1,v2) st b₁ is_vertex_seq_of c
consider p being FinSequence of the carrier of G such that
A2: p is_vertex_seq_of c by GRAPH_2:36;
reconsider p' = p as FinSequence of the carrier of (AddNewEdge v1,v2) by Def7;
take p' ; :: thesis: p' is_vertex_seq_of c
thus p' is_vertex_seq_of c by A2, Th41; :: thesis: verum