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