theorem Th1: :: BORSUK_6:1

the carrier of [:I[01],I[01]:] = [:[.0,1.],[.0,1.]:] by BORSUK_1:40, BORSUK_1:def 2;