defpred S₁[ Nat] means ex G being _Graph ex v being Vertex of G st
( G is n + 1 -vertex & G is n -edge & G is Path-like & ( not G is _trivial implies v is endvertex ) );
A1: S₁[ 0 ]

proof

take G = the _trivial edgeless _Graph; :: thesis: ex v being Vertex of G st
( G is 0 + 1 -vertex & G is 0 -edge & G is Path-like & ( not G is _trivial implies v is endvertex ) )
take the Vertex of G ; :: thesis: ( G is 0 + 1 -vertex & G is 0 -edge & G is Path-like & ( not G is _trivial implies the Vertex of G is endvertex ) )
thus ( G is 0 + 1 -vertex & G is 0 -edge & G is Path-like & ( not G is _trivial implies the Vertex of G is endvertex ) ) ; :: thesis: verum

end;

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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
then consider G2 being _Graph, v2 being Vertex of G2 such that
A3: ( G2 is m + 1 -vertex & G2 is m -edge & G2 is Path-like ) and
A4: ( not G2 is _trivial implies v2 is endvertex ) ;
take G1 = the addAdjVertex of G2,v2, the_Edges_of G2, the_Vertices_of G2; :: thesis: ex v being Vertex of G1 st
( G1 is (m + 1) + 1 -vertex & G1 is m + 1 -edge & G1 is Path-like & ( not G1 is _trivial implies v is endvertex ) )
A5: ( not the_Edges_of G2 in the_Edges_of G2 & not the_Vertices_of G2 in the_Vertices_of G2 ) ;
reconsider v1 = the_Vertices_of G2 as Vertex of G1 by A5, GLIB_006:129;
take v1 ; :: thesis: ( G1 is (m + 1) + 1 -vertex & G1 is m + 1 -edge & G1 is Path-like & ( not G1 is _trivial implies v1 is endvertex ) )
G1 .order() = (G2 .order()) +` 1 by A5, GLIB_006:150
.= (m + 1) +` 1 by A3, GLIB_013:def 3
.= (m + 1) + 1 ;
hence G1 is (m + 1) + 1 -vertex by GLIB_013:def 3; :: thesis: ( G1 is m + 1 -edge & G1 is Path-like & ( not G1 is _trivial implies v1 is endvertex ) )
G1 .size() = (G2 .size()) +` 1 by A5, GLIB_006:150
.= m +` 1 by A3, GLIB_013:def 4
.= m + 1 ;
hence G1 is m + 1 -edge by GLIB_013:def 4; :: thesis: ( G1 is Path-like & ( not G1 is _trivial implies v1 is endvertex ) )
thus G1 is Path-like by A3, A4, Th18; :: thesis: ( not G1 is _trivial implies v1 is endvertex )
assume not G1 is _trivial ; :: thesis: v1 is endvertex
thus v1 is endvertex by A5, GLIB_006:141; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
then consider G being _Graph, v being Vertex of G such that
A8: ( G is n + 1 -vertex & G is n -edge & G is Path-like ) and
( not G is _trivial implies v is endvertex ) ;
take G ; :: thesis: ( G is n + 1 -vertex & G is n -edge & G is Path-like )
thus ( G is n + 1 -vertex & G is n -edge & G is Path-like ) by A8; :: thesis: verum