:: deftheorem defines Dir111 ANPROJ_9:def 8 :
Dir111 = Dir |[1,1,1]|;