set G9 = AddNewEdge (v1,v2);

now :: thesis: for v19, v29 being Vertex of (AddNewEdge (v1,v2)) st v19 <> v29 holds
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 )

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 Th18;
reconsider vs9 = vs as FinSequence of the carrier of (AddNewEdge (v1,v2)) by Def7;
reconsider c9 = c as Chain of AddNewEdge (v1,v2) by Th37;
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, Th36; :: 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 Th18; :: thesis: verum