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

assume A1: ( GF is _trivial & GF is loopless ) ; :: thesis: GF is Tree-like

let x be object ; :: according to GLIB_002:def 14 :: thesis: ( x in dom GF implies ex G being _Graph st

( GF . x = G & G is Tree-like ) )

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

( GF . x = G & G is Tree-like )

then consider G being _Graph such that

A3: ( GF . x = G & G is _trivial ) by A1, GLIB_000:def 60;

consider G0 being _Graph such that

A4: ( GF . x = G0 & G0 is loopless ) by A1, A2, GLIB_000:def 59;

take G ; :: thesis: ( GF . x = G & G is Tree-like )

thus ( GF . x = G & G is Tree-like ) by A3, A4; :: thesis: verum

assume A1: ( GF is _trivial & GF is loopless ) ; :: thesis: GF is Tree-like

let x be object ; :: according to GLIB_002:def 14 :: thesis: ( x in dom GF implies ex G being _Graph st

( GF . x = G & G is Tree-like ) )

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

( GF . x = G & G is Tree-like )

then consider G being _Graph such that

A3: ( GF . x = G & G is _trivial ) by A1, GLIB_000:def 60;

consider G0 being _Graph such that

A4: ( GF . x = G0 & G0 is loopless ) by A1, A2, GLIB_000:def 59;

take G ; :: thesis: ( GF . x = G & G is Tree-like )

thus ( GF . x = G & G is Tree-like ) by A3, A4; :: thesis: verum