theorem :: GLIB_002:47

for G being finite _Graph holds
( G is Tree-like iff ( G is connected & G .order() = (G .size()) + 1 ) )