:: deftheorem Def53 defines Graph-yielding GLIB_000:def 54 :
for F being ManySortedSet of NAT holds
( F is Graph-yielding iff for n being Nat holds F . n is _Graph );