x `22 = (x `2) `2 by MCART_1:def 17;
hence x `22 is Element of D3 ; :: thesis: verum