theorem :: AFF_3:7
for AP being AffinPlane st AP is satisfying_DES2_1 holds
AP is satisfying_DES2