not ].(1 / 2),((1 / 2) + p1).[ is empty ;
hence not ].(1 / 2),(3 / 2).[ is empty ; :: thesis: verum