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