theorem :: AFF_3:8
for AP being AffinPlane holds
( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 )