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:33;
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;
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, Th36; :: thesis: verum