:: deftheorem Def2 defines Pappian PAPDESAF:def 2 :
for IT being OAffinSpace holds
( IT is Pappian iff Lambda IT is Pappian );