:: deftheorem Def2 defines Pappian EUCLMETR:def 2 :
for IT being OrtAfSp holds
( IT is Pappian iff AffinStruct(# the carrier of IT, the CONGR of IT #) is Pappian );