theorem :: AFF_3:5
for AP being AffinPlane st AP is satisfying_DES1_2 holds
AP is satisfying_DES1_3