:: deftheorem Def4 defines Moufangian PAPDESAF:def 4 :
for IT being OAffinSpace holds
( IT is Moufangian iff Lambda IT is Moufangian );