:: deftheorem Def12 defines - MOD_2:def 12 :
for a being Element of {0,1,2} holds
( ( a = 0 implies - a = 0 ) & ( a = 1 implies - a = 2 ) & ( a = 2 implies - a = 1 ) );