:: deftheorem defines Dir100 ANPROJ_9:def 5 :
Dir100 = Dir |[1,0,0]|;