:: deftheorem defines Dir010 ANPROJ_9:def 6 :
Dir010 = Dir |[0,1,0]|;