let GF be Graph-yielding Function; :: thesis: ( GF is Tree-like implies ( GF is acyclic & GF is connected ) )

assume A1: GF is Tree-like ; :: thesis: ( GF is acyclic & GF is connected )

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is acyclic )

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is connected )

assume A1: GF is Tree-like ; :: thesis: ( GF is acyclic & GF is connected )

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is acyclic )

proof

hence
GF is acyclic
; :: thesis: GF is connected
let x be object ; :: thesis: ( x in dom GF implies ex G being _Graph st

( GF . x = G & G is acyclic ) )

assume x in dom GF ; :: thesis: ex G being _Graph st

( GF . x = G & G is acyclic )

then consider G being _Graph such that

A2: ( GF . x = G & G is Tree-like ) by A1;

take G ; :: thesis: ( GF . x = G & G is acyclic )

thus ( GF . x = G & G is acyclic ) by A2; :: thesis: verum

end;( GF . x = G & G is acyclic ) )

assume x in dom GF ; :: thesis: ex G being _Graph st

( GF . x = G & G is acyclic )

then consider G being _Graph such that

A2: ( GF . x = G & G is Tree-like ) by A1;

take G ; :: thesis: ( GF . x = G & G is acyclic )

thus ( GF . x = G & G is acyclic ) by A2; :: thesis: verum

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is connected )

proof

hence
GF is connected
; :: thesis: verum
let x be object ; :: thesis: ( x in dom GF implies ex G being _Graph st

( GF . x = G & G is connected ) )

assume x in dom GF ; :: thesis: ex G being _Graph st

( GF . x = G & G is connected )

then consider G being _Graph such that

A2: ( GF . x = G & G is Tree-like ) by A1;

take G ; :: thesis: ( GF . x = G & G is connected )

thus ( GF . x = G & G is connected ) by A2; :: thesis: verum

end;( GF . x = G & G is connected ) )

assume x in dom GF ; :: thesis: ex G being _Graph st

( GF . x = G & G is connected )

then consider G being _Graph such that

A2: ( GF . x = G & G is Tree-like ) by A1;

take G ; :: thesis: ( GF . x = G & G is connected )

thus ( GF . x = G & G is connected ) by A2; :: thesis: verum