thus O1 * O2 is Relation of X ; :: thesis: verum