let G be _Graph; :: thesis: ( not G is _trivial & G is edgeless implies ( not G is connected & not G is Tree-like & not G is complete ) )
assume A2: ( not G is _trivial & G is edgeless ) ; :: thesis: ( not G is connected & not G is Tree-like & not G is complete )
then consider v1, v2 being Vertex of G such that
A3: v1 <> v2 by GLIB_000:21;
for W being Walk of G holds not W is_Walk_from v1,v2
proof
given W being Walk of G such that A4: W is_Walk_from v1,v2 ; :: thesis: contradiction
( W .first() = v1 & W .last() = v2 ) by A4, GLIB_001:def 23;
hence contradiction by A2, A3, GLIB_001:127; :: thesis: verum
end;
hence ( not G is connected & not G is Tree-like & not G is complete ) by GLIB_002:def 1; :: thesis: verum