:: deftheorem defines trivial GLIB_001:def 26 :
for G being _Graph
for W being Walk of G holds
( W is trivial iff W .length() = 0 );