let G be _finite _Graph; ( 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; ( 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
; G is Tree-like
now G is acyclic assume
not
G is
acyclic
;
contradictionthen 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;
verum end;
hence
G is Tree-like
by A1; verum