theorem :: EUCLID_8:9

<e2> , <e3> are_orthogonal