let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A2: ( GF . x = G & G is Tree-like ) by A1;
take G ; :: thesis:
thus ( GF . x = G & G is acyclic ) by A2; :: thesis:

end;

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

let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A2: ( GF . x = G & G is Tree-like ) by A1;
take G ; :: thesis:
thus ( GF . x = G & G is connected ) by A2; :: thesis:

end;