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());
consider G2 being removeEdge of G,(choose (W .edges()));
A4: W .edges() <> {} by A3, GLIB_001:137;
then choose (W .edges()) in W .edges() ;
then A5: ( G2 .order() = G .order() & (G2 .size()) + 1 = G .size() ) by GLIB_000:55;
G2 is connected by A1, A3, A4, Th5;
then ((G2 .size()) + 1) + 1 <= ((G2 .size()) + 1) + 0 by A2, A5, Th40;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

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