theorem :: AFF_3:1

for AP being AffinPlane st AP is satisfying_DES1 holds
AP is satisfying_DES1_1