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