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