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