let F be Graph-yielding Function; :: thesis: ( F is _trivial & F is edgeless implies F is Path-like )
assume A1: ( F is _trivial & F is edgeless ) ; :: thesis: F is Path-like
let x be object ; :: according to GLPACY00:def 2 :: thesis: ( x in dom F implies ex G being _Graph st
( F . x = G & G is Path-like ) )
assume A2: x in dom F ; :: thesis: ex G being _Graph st
( F . x = G & G is Path-like )
then consider G1 being _Graph such that
A3: ( G1 = F . x & G1 is _trivial ) by A1, GLIB_000:def 60;
consider G2 being _Graph such that
A4: ( G2 = F . x & G2 is edgeless ) by A1, A2, GLIB_008:def 2;
take G1 ; :: thesis: ( F . x = G1 & G1 is Path-like )
thus ( F . x = G1 & G1 is Path-like ) by A3, A4; :: thesis: verum