theorem :: AFF_2:2

for AP being AffinPlane holds
( AP is Desarguesian iff AP is satisfying_DES_1 )