x `12 = (x `1) `2 by MCART_1:def 15;
hence x `12 is Element of D2 ; :: thesis: verum