take O_el Y ; :: thesis: O_el Y is constant
thus O_el Y is constant ; :: thesis: verum