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

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 set 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 by Def2;
reconsider G9 = G as trivial _Graph by A1;
G9 is connected ;
hence G is Tree-like by A4, Def3; :: thesis: verum