:: deftheorem Def4 defines Fanoian EUCLMETR:def 4 :
for IT being OrtAfSp holds
( IT is Fanoian iff AffinStruct(# the carrier of IT, the CONGR of IT #) is Fanoian );