set G9 = AddNewEdge (v1,v2);
now 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));
( 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
;
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;
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;
( not c9 is empty & vs9 is_vertex_seq_of c9 & vs9 . 1 = v19 & vs9 . (len vs9) = v29 )thus
not
c9 is
empty
by A1;
( vs9 is_vertex_seq_of c9 & vs9 . 1 = v19 & vs9 . (len vs9) = v29 )thus
vs9 is_vertex_seq_of c9
by A2, Th36;
( vs9 . 1 = v19 & vs9 . (len vs9) = v29 )thus
(
vs9 . 1
= v19 &
vs9 . (len vs9) = v29 )
by A3;
verum end;
hence
AddNewEdge (v1,v2) is connected
by Th18; verum