thus x `11 is Element of D1 ; :: thesis: verum