let GF be Graph-yielding Function; :: thesis: ( GF is trivial implies GF is connected )

assume A1: GF is trivial ; :: thesis: GF is connected

let x be object ; :: according to GLIB_002:def 12 :: 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 trivial ) by A1, GLIB_000:def 60;

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

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

assume A1: GF is trivial ; :: thesis: GF is connected

let x be object ; :: according to GLIB_002:def 12 :: 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 trivial ) by A1, GLIB_000:def 60;

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

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