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