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