let G be _finite simple connected _Graph; P1[G]
consider p being non empty Graph-yielding _finite simple connected FinSequence such that
A3:
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() )
and
A4:
for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V )
by Th82;
defpred S1[ Nat] means ( $1 <= len p implies ex k being Element of dom p st
( $1 = k & P1[p . k] ) );
A5:
S1[1]
A6:
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 A7:
S1[
m]
;
S1[m + 1]
assume A8:
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 A8, 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 A8, XREAL_1:13;
then consider k0 being
Element of
dom p such that A9:
(
m = k0 &
P1[
p . k0] )
by A7;
(m + 1) - 1
<= (len p) - 1
by A8, XREAL_1:9;
then consider v being
object ,
V being non
empty finite set such that A10:
v in (the_Vertices_of G) \ (the_Vertices_of (p . k0))
and A11:
(
V c= the_Vertices_of (p . k0) &
p . (k0 + 1) is
addAdjVertexAll of
p . k0,
v,
V )
by A4, A9;
not
v in the_Vertices_of (p . k0)
by A10, XBOOLE_0:def 5;
hence
P1[
p . k]
by A2, A9, A11;
verum
end;
for m being non zero Nat holds S1[m]
from NAT_1:sch 10(A5, A6);
then
ex k being Element of dom p st
( len p = k & P1[p . k] )
;
hence
P1[G]
by A3; verum