:: deftheorem Def3 defines Desarguesian EUCLMETR:def 3 :
for IT being OrtAfSp holds
( IT is Desarguesian iff AffinStruct(# the carrier of IT, the CONGR of IT #) is Desarguesian );