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