:: deftheorem defines Dir001 ANPROJ_9:def 7 :
Dir001 = Dir |[0,0,1]|;