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
now :: thesis: for W being Walk of G holds not W is Cycle-like
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;
then A4: G is acyclic ;
reconsider G9 = G as _trivial _Graph by A1;
G9 is connected ;
hence G is Tree-like by A4; :: thesis: verum