let G be finite _Graph; :: thesis: ( G is Tree-like iff ( G is connected & G .order() = (G .size() ) + 1 ) )
thus ( G is Tree-like implies ( G is connected & G .order() = (G .size() ) + 1 ) ) by Th46; :: thesis: ( G is connected & G .order() = (G .size() ) + 1 implies G is Tree-like )
assume A1: ( G is connected & G .order() = (G .size() ) + 1 ) ; :: thesis: G is Tree-like

now

assume not G is acyclic ; :: thesis: contradiction
then consider W being Walk of G such that
A2: W is Cycle-like by Def2;
set e = choose (W .edges() );
consider G2 being removeEdge of G,(choose (W .edges() ));
not W is trivial by A2;
then A3: W .edges() <> {} by GLIB_001:137;
then A4: choose (W .edges() ) in W .edges() ;
A5: G2 is connected by A1, A2, A3, Th5;
( G2 .order() = G .order() & (G2 .size() ) + 1 = G .size() ) by A4, GLIB_000:55;
then ((G2 .size() ) + 1) + 1 <= ((G2 .size() ) + 1) + 0 by A1, A5, Th40;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

hence G is Tree-like by A1; :: thesis: verum