the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence not the carrier of [:X,Y:] is empty ; :: according to STRUCT_0:def 1 :: thesis: verum