theorem :: EUCLID_8:18

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