for T being _Tree
for P being Path of T st P is V5() holds
P is open by GLIB_001:def 31, GLIB_002:def 2;