:: deftheorem defines <e3> EUCLID_8:def 3 :
<e3> = |[0,0,1]|;