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 )

proof

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;

hence GF is acyclic ; :: thesis: GF is connected
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is connected )

proof

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;

hence GF is connected ; :: thesis: verum