thus x `12 is Element of D2 ; :: thesis: verum