theorem Th8: :: BORSUK_6:8

id I[01] is Path of 0[01] , 1[01]