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