:: deftheorem Def2 defines Path-like GLPACY00:def 2 :
for F being Graph-yielding Function holds
( F is Path-like iff for x being object st x in dom F holds
ex G being _Graph st
( F . x = G & G is Path-like ) );