theorem Th13: :: AFF_2:13
for AP being AffinPlane st AP is satisfying_TDES_1 holds
AP is satisfying_des_1