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