the carrier of [:T2,T1:] = [: the carrier of T2, the carrier of T1:] by BORSUK_1:def 2;
hence [:T2,T1:] is empty ; :: thesis: verum