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 that
A1: G is connected and
A2: 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
A3: W is Cycle-like by Def2;
set e = choose (W .edges());
set G2 = the removeEdge of G,(choose (W .edges()));
A4: W .edges() <> {} by A3, GLIB_001:136;
then choose (W .edges()) in W .edges() ;
then A5: ( the removeEdge of G,(choose (W .edges())) .order() = G .order() & ( the removeEdge of G,(choose (W .edges())) .size()) + 1 = G .size() ) by GLIB_000:52;
the removeEdge of G,(choose (W .edges())) is connected by A1, A3, A4, Th5;
then (( the removeEdge of G,(choose (W .edges())) .size()) + 1) + 1 <= (( the removeEdge of G,(choose (W .edges())) .size()) + 1) + 0 by A2, A5, Th40;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

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