the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2;
hence x `1 is Element of L1 by MCART_1:10; :: thesis: verum