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