theorem Th25: :: HELLY:25
for T being _Tree
for P being Path of T st P is trivial holds
P is open by GLIB_001:def 31, GLIB_002:def 2;