:: deftheorem defines non-trivial GLIB_000:def 61 :
for GF being Graph-yielding Function holds
( GF is non-trivial iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & not G is _trivial ) );