theorem :: EUCLID_8:4
|.<e1>.| = 1