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

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

hence
G is Tree-like
by A1; :: thesis: verumassume
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;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