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