let T be _Tree; :: thesis: for P being Path of T st not P is trivial holds
not P is closed
let P be Path of T; :: thesis: ( not P is trivial implies not P is closed )
assume ( not P is trivial & P is closed ) ; :: thesis: contradiction
then P is Cycle-like by GLIB_001:def 31;
hence contradiction by GLIB_002:def 2; :: thesis: verum