:: deftheorem defines Fanoian VECTSP_1:def 17 :
for IT being non empty addLoopStr holds
( IT is Fanoian iff for a being Element of IT st a + a = 0. IT holds
a = 0. IT );