let F be Graph-yielding Function; :: thesis: ( F is _trivial & F is non-Dmulti & F is loopfull implies F is Cycle-like )
assume A1: ( F is _trivial & F is non-Dmulti & F is loopfull ) ; :: thesis: F is Cycle-like
let x be object ; :: according to GLPACY00:def 7 :: thesis: ( x in dom F implies ex G being _Graph st
( F . x = G & G is Cycle-like ) )
assume A2: x in dom F ; :: thesis: ex G being _Graph st
( F . x = G & G is Cycle-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 non-Dmulti ) by A1, A2, GLIB_000:def 63;
consider G3 being _Graph such that
A5: ( G3 = F . x & G3 is loopfull ) by A1, A2, GLIB_012:def 2;
take G1 ; :: thesis: ( F . x = G1 & G1 is Cycle-like )
thus ( F . x = G1 & G1 is Cycle-like ) by A3, A4, A5; :: thesis: verum