set G9 = AddNewEdge v1,v2;

now

let v19, v29 be Vertex of (AddNewEdge v1,v2); :: thesis: ( v19 <> v29 implies ex c9 being Chain of AddNewEdge v1,v2 ex vs9 being FinSequence of the carrier of (AddNewEdge v1,v2) st
( not c9 is empty & vs9 is_vertex_seq_of c9 & vs9 . 1 = v19 & vs9 . (len vs9) = v29 ) )
reconsider v1 = v19, v2 = v29 as Vertex of G by Def7;
assume v19 <> v29 ; :: thesis: ex c9 being Chain of AddNewEdge v1,v2 ex vs9 being FinSequence of the carrier of (AddNewEdge v1,v2) st
( not c9 is empty & vs9 is_vertex_seq_of c9 & vs9 . 1 = v19 & vs9 . (len vs9) = v29 )
then consider c being Chain of G, vs being FinSequence of the carrier of G such that
A1: not c is empty and
A2: vs is_vertex_seq_of c and
A3: ( vs . 1 = v1 & vs . (len vs) = v2 ) by Th23;
reconsider vs9 = vs as FinSequence of the carrier of (AddNewEdge v1,v2) by Def7;
reconsider c9 = c as Chain of AddNewEdge v1,v2 by Th42;
take c9 = c9; :: thesis: ex vs9 being FinSequence of the carrier of (AddNewEdge v1,v2) st
( not c9 is empty & vs9 is_vertex_seq_of c9 & vs9 . 1 = v19 & vs9 . (len vs9) = v29 )
take vs9 = vs9; :: thesis: ( not c9 is empty & vs9 is_vertex_seq_of c9 & vs9 . 1 = v19 & vs9 . (len vs9) = v29 )
thus not c9 is empty by A1; :: thesis: ( vs9 is_vertex_seq_of c9 & vs9 . 1 = v19 & vs9 . (len vs9) = v29 )
thus vs9 is_vertex_seq_of c9 by A2, Th41; :: thesis: ( vs9 . 1 = v19 & vs9 . (len vs9) = v29 )
thus ( vs9 . 1 = v19 & vs9 . (len vs9) = v29 ) by A3; :: thesis: verum

end;

hence AddNewEdge v1,v2 is connected by Th23; :: thesis: verum