set G' = AddNewEdge v1,v2;
now let v1',
v2' be
Vertex of
(AddNewEdge v1,v2);
( v1' <> v2' implies ex c' being Chain of AddNewEdge v1,v2 ex vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st
( not c' is empty & vs' is_vertex_seq_of c' & vs' . 1 = v1' & vs' . (len vs') = v2' ) )reconsider v1 =
v1',
v2 =
v2' as
Vertex of
G by Def7;
assume
v1' <> v2'
;
ex c' being Chain of AddNewEdge v1,v2 ex vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st
( not c' is empty & vs' is_vertex_seq_of c' & vs' . 1 = v1' & vs' . (len vs') = v2' )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 vs' =
vs as
FinSequence of the
carrier of
(AddNewEdge v1,v2) by Def7;
reconsider c' =
c as
Chain of
AddNewEdge v1,
v2 by Th42;
take c' =
c';
ex vs' being FinSequence of the carrier of (AddNewEdge v1,v2) st
( not c' is empty & vs' is_vertex_seq_of c' & vs' . 1 = v1' & vs' . (len vs') = v2' )take vs' =
vs';
( not c' is empty & vs' is_vertex_seq_of c' & vs' . 1 = v1' & vs' . (len vs') = v2' )thus
not
c' is
empty
by A1;
( vs' is_vertex_seq_of c' & vs' . 1 = v1' & vs' . (len vs') = v2' )thus
vs' is_vertex_seq_of c'
by A2, Th41;
( vs' . 1 = v1' & vs' . (len vs') = v2' )thus
(
vs' . 1
= v1' &
vs' . (len vs') = v2' )
by A3;
verum end;
hence
AddNewEdge v1,v2 is connected
by Th23; verum