let G be _finite connected _Graph; P1[G]
consider p being non empty Graph-yielding _finite connected FinSequence such that
A4:
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = (G .size()) + 1 )
and
A5:
for n being Element of dom p holds
( not n <= (len p) - 1 or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) )
by Th74;
defpred S1[ Nat] means ( $1 <= len p implies ex k being Element of dom p st
( $1 = k & P1[p . k] ) );
A6:
S1[1]
A7:
for m being non zero Nat st S1[m] holds
S1[m + 1]
proof
let m be non
zero Nat;
( S1[m] implies S1[m + 1] )
assume A8:
S1[
m]
;
S1[m + 1]
assume A9:
m + 1
<= len p
;
ex k being Element of dom p st
( m + 1 = k & P1[p . k] )
0 + 1
<= m + 1
by XREAL_1:6;
then reconsider k =
m + 1 as
Element of
dom p by A9, FINSEQ_3:25;
take
k
;
( m + 1 = k & P1[p . k] )
thus
m + 1
= k
;
P1[p . k]
(m + 1) - 1
<= (len p) - 0
by A9, XREAL_1:13;
then consider k0 being
Element of
dom p such that A10:
(
m = k0 &
P1[
p . k0] )
by A8;
(m + 1) - 1
<= (len p) - 1
by A9, XREAL_1:9;
per cases then
( ex v1, v2 being Vertex of G ex e being object st
( p . (k0 + 1) is addAdjVertex of p . k0,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . k0)) & ( ( v1 in the_Vertices_of (p . k0) & not v2 in the_Vertices_of (p . k0) ) or ( not v1 in the_Vertices_of (p . k0) & v2 in the_Vertices_of (p . k0) ) ) ) or ex v1, v2 being Vertex of G ex e being object st
( p . (k0 + 1) is addEdge of p . k0,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . k0)) & v1 in the_Vertices_of (p . k0) & v2 in the_Vertices_of (p . k0) ) )
by A5, A10;
suppose
ex
v1,
v2 being
Vertex of
G ex
e being
object st
(
p . (k0 + 1) is
addEdge of
p . k0,
v1,
e,
v2 &
e in (the_Edges_of G) \ (the_Edges_of (p . k0)) &
v1 in the_Vertices_of (p . k0) &
v2 in the_Vertices_of (p . k0) )
;
P1[p . k]then consider v1,
v2 being
Vertex of
G,
e being
object such that A15:
p . (k0 + 1) is
addEdge of
p . k0,
v1,
e,
v2
and A16:
(
e in (the_Edges_of G) \ (the_Edges_of (p . k0)) &
v1 in the_Vertices_of (p . k0) &
v2 in the_Vertices_of (p . k0) )
;
reconsider v1 =
v1,
v2 =
v2 as
Vertex of
(p . k0) by A16;
A17:
not
e in the_Edges_of (p . k0)
by A16, XBOOLE_0:def 5;
p . k is
addEdge of
p . k0,
v1,
e,
v2
by A10, A15;
hence
P1[
p . k]
by A3, A10, A17;
verum end;
end;
for m being non zero Nat holds S1[m]
from NAT_1:sch 10(A6, A7);
then
ex k being Element of dom p st
( len p = k & P1[p . k] )
;
hence
P1[G]
by A4; verum