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