let G be _Graph; :: thesis: ( G is 2 -vertex & G is simple & G is connected implies G is Path-like )
assume A1: ( G is 2 -vertex & G is simple & G is connected ) ; :: thesis: G is Path-like
then reconsider G9 = G as _finite _Graph ;
(((G9 .order()) ^2) - (G9 .order())) / 2 = (((G9 .order()) ^2) - 2) / 2 by A1, GLIB_013:def 3
.= ((2 ^2) - 2) / 2 by A1, GLIB_013:def 3
.= ((2 * 2) - 2) / 2 by SQUARE_1:def 1
.= 1 ;
then A2: G9 .size() <= 1 by A1, GLIB_013:12;

now :: thesis: for W being Walk of G9 holds not W is Cycle-like

given W being Walk of G9 such that A3: W is Cycle-like ; :: thesis: contradiction
card (W .length()) <= card (G9 .size()) by A3, GLIBPRE1:27, NAT_1:43;
then W .length() <= 1 by A2, XXREAL_0:2;
then W .length() = 1 by A3, NAT_1:25, GLIB_001:def 26;
then consider e being object such that
A4: e Joins W .first() ,W .last() ,G9 and
W = G9 .walkOf ((W .first()),e,(W .last())) by GLIBPRE1:28;
W .first() = W .last() by A3, GLIB_001:def 24;
hence contradiction by A1, A4, GLIB_000:18; :: thesis: verum

end;

then A5: G9 is acyclic by GLIB_002:def 2;

now :: thesis: for v being Vertex of G9 holds v .degree() <= 2

let v be Vertex of G9; :: thesis: v .degree() <= 2
card (v .edgesInOut()) <= G9 .size() by NAT_1:43;
then v .degree() <= G9 .size() by A1, GLIB_000:19;
then v .degree() <= 1 by A2, XXREAL_0:2;
hence v .degree() <= 2 by XXREAL_0:2; :: thesis: verum

end;

hence G is Path-like by A1, A5, Th17; :: thesis: verum