theorem :: EUCLID_8:17

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