let G be _finite edgeless _Graph; :: thesis: P₁[G]
consider p being non empty Graph-yielding _finite edgeless 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 Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) by Th62;
defpred S₁[ Nat] means ( $1 + 1 <= len p implies ex k being Element of dom p st
( k = $1 + 1 & P₁[p . k] ) );
A5: S₁[ 0 ]

proof

assume 0 + 1 <= len p ; :: thesis: ex k being Element of dom p st
( k = 0 + 1 & P₁[p . k] )
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k ; :: thesis: ( k = 0 + 1 & P₁[p . k] )
thus k = 0 + 1 ; :: thesis: P₁[p . k]
thus P₁[p . k] by A1, A3; :: thesis: verum

end;

A6: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A7: S₁[m] ; :: thesis: S₁[m + 1]
assume A8: (m + 1) + 1 <= len p ; :: thesis: ex k being Element of dom p st
( k = (m + 1) + 1 & P₁[p . k] )
then ((m + 1) + 1) - 1 <= (len p) - 0 by XREAL_1:13;
then consider k0 being Element of dom p such that
A9: ( k0 = m + 1 & P₁[p . k0] ) by A7;
set k = k0 + 1;
0 + 1 <= k0 + 1 by XREAL_1:6;
then reconsider k = k0 + 1 as Element of dom p by A8, A9, FINSEQ_3:25;
take k ; :: thesis: ( k = (m + 1) + 1 & P₁[p . k] )
thus k = (m + 1) + 1 by A9; :: thesis: P₁[p . k]
(k0 + 1) - 1 <= (len p) - 1 by A8, A9, XREAL_1:9;
then consider v being Vertex of G such that
A10: ( p . k is addVertex of p . k0,v & not v in the_Vertices_of (p . k0) ) by A4;
thus P₁[p . k] by A2, A9, A10; :: thesis: verum

end;

A11: for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A6);
( (len p) - 1 is Nat & ((len p) - 1) + 1 <= len p ) by INT_1:74;
then ex k being Element of dom p st
( k = ((len p) - 1) + 1 & P₁[p . k] ) by A11;
hence P₁[G] by A3; :: thesis: verum