theorem :: EUCLID_8:7

<e1> , <e2> are_orthogonal