dom (Intervals ({},r)) = dom {} by Def3;
hence Intervals ({},r) is empty ; :: thesis: verum