thus R | Y = R null Y ; :: thesis: verum