theorem :: EUCLID_8:20

<e1> <X> <e3> = - <e2>