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