theorem :: TREAL_1:5

( 0[01] = (#) (0,1) & 1[01] = (0,1) (#) ) by Def1, Def2, BORSUK_1:def 14, BORSUK_1:def 15;