let GF be Graph-yielding Function; :: thesis: ( GF is acyclic implies GF is simple )

assume A1: GF is acyclic ; :: thesis: GF is simple

assume A1: GF is acyclic ; :: thesis: GF is simple

now :: thesis: for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is simple )

hence
GF is simple
by GLIB_000:def 64; :: thesis: verumex G being _Graph st

( GF . x = G & G is simple )

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

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

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

( GF . x = G & G is simple )

then consider G being _Graph such that

A2: ( GF . x = G & G is acyclic ) by A1;

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

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

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

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

( GF . x = G & G is simple )

then consider G being _Graph such that

A2: ( GF . x = G & G is acyclic ) by A1;

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

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