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