theorem :: EUCLID_8:4

|.<e1>.| = 1