thus <e2> <X> <e3> = <e1> ; :: thesis: verum