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