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