:: deftheorem Def3 defines Desarguesian PAPDESAF:def 3 :
for IT being OAffinSpace holds
( IT is Desarguesian iff Lambda IT is Desarguesian );