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 G9 = AddNewEdge v1,v2;
consider p being FinSequence of the carrier of G such that
A1: p is_vertex_seq_of c by GRAPH_2:36;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then A2: rng c c= the carrier' of G by FINSEQ_1:def 4;
the carrier' of (AddNewEdge v1,v2) = the carrier' of G \/ {the carrier' of G} by Def7;
then the carrier' of G c= the carrier' of (AddNewEdge v1,v2) by XBOOLE_1:7;
then rng c c= the carrier' of (AddNewEdge v1,v2) by A2, 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
reconsider p9 = p as FinSequence of the carrier of (AddNewEdge v1,v2) by Def7;
take p9 ; :: thesis: p9 is_vertex_seq_of c
thus p9 is_vertex_seq_of c by A1, Th41; :: thesis: verum