theorem :: EUCLID_8:16

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