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 Th45; :: 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 :: thesis: G is acyclic

assume not G is acyclic ; :: thesis: contradiction
then consider W being Walk of G such that
A3: W is Cycle-like ;
set e = the Element of W .edges() ;
set G2 = the removeEdge of G, the Element of W .edges() ;
A4: W .edges() <> {} by A3, GLIB_001:136;
then the Element of W .edges() in W .edges() ;
then A5: ( the removeEdge of G, the Element of W .edges() .order() = G .order() & ( the removeEdge of G, the Element of W .edges() .size()) + 1 = G .size() ) by GLIB_000:52;
the removeEdge of G, the Element of W .edges() is connected by A1, A3, A4, Th4;
then (( the removeEdge of G, the Element of W .edges() .size()) + 1) + 1 <= (( the removeEdge of G, the Element of W .edges() .size()) + 1) + 0 by A2, A5, Th39;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

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