let G be _Graph; :: thesis: ( G is trivial & G is loopless implies G is Tree-like )

assume that

A1: G is trivial and

A2: G is loopless ; :: thesis: G is Tree-like

reconsider G9 = G as trivial _Graph by A1;

G9 is connected ;

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

assume that

A1: G is trivial and

A2: G is loopless ; :: thesis: G is Tree-like

now :: thesis: for W being Walk of G holds not W is Cycle-like

then A4:
G is acyclic
;given W being Walk of G such that A3:
W is Cycle-like
; :: thesis: contradiction

W .edges() <> {} by A3, GLIB_001:136;

then ex e being object st e in W .edges() by XBOOLE_0:def 1;

hence contradiction by A1, A2, GLIB_000:23; :: thesis: verum

end;W .edges() <> {} by A3, GLIB_001:136;

then ex e being object st e in W .edges() by XBOOLE_0:def 1;

hence contradiction by A1, A2, GLIB_000:23; :: thesis: verum

reconsider G9 = G as trivial _Graph by A1;

G9 is connected ;

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