theorem :: EUCLID_8:8

<e1> , <e3> are_orthogonal