T .pathBetween (a,a) is_Walk_from a,a by Def2;
hence T .pathBetween (a,a) is closed by GLIB_001:119; :: thesis: verum